Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-12 23:21 8bb0b6f7

View on Github →

feat(category_theory/sites/plus): If P is a sheaf, then the map from P to P^+ is an isomorphism. (#10297) Also adds some simple results about (co)limits where the morphisms in the diagram are isomorphisms.

Estimated changes

Modified src/category_theory/category/preorder.lean

Modified src/category_theory/limits/shapes/terminal.lean

added def category_theory.limits.cocone_of_diagram_initial

added def category_theory.limits.colimit_of_diagram_initial

added def category_theory.limits.colimit_of_initial

added def category_theory.limits.cone_of_diagram_terminal

added def category_theory.limits.is_initial_bot

added theorem category_theory.limits.is_iso_ι_of_is_initial

added theorem category_theory.limits.is_iso_π_of_is_terminal

added def category_theory.limits.is_terminal_top

added def category_theory.limits.limit_of_diagram_terminal

added def category_theory.limits.limit_of_terminal

Modified src/category_theory/sites/plus.lean

added theorem category_theory.grothendieck_topology.is_iso_to_plus_of_is_sheaf