Commit 2021-11-30 06:50 f11d505e

View on Github →

feat(category_theory/sites/compatible_*): Compatibility of plus and sheafification with composition. (#10510) Compatibility of sheafification with composition. This will be used later to obtain adjunctions between categories of sheaves.

Estimated changes

Created src/category_theory/sites/compatible_plus.lean

added def category_theory.grothendieck_topology.diagram_comp_iso

added theorem category_theory.grothendieck_topology.diagram_comp_iso_hom_ι

added def category_theory.grothendieck_topology.plus_comp_iso

added theorem category_theory.grothendieck_topology.plus_comp_iso_inv_eq_plus_lift

added theorem category_theory.grothendieck_topology.plus_comp_iso_whisker_left

added theorem category_theory.grothendieck_topology.plus_comp_iso_whisker_right

added def category_theory.grothendieck_topology.plus_functor_whisker_left_iso

added def category_theory.grothendieck_topology.plus_functor_whisker_right_iso

added theorem category_theory.grothendieck_topology.to_plus_comp_plus_comp_iso_inv

added theorem category_theory.grothendieck_topology.whisker_right_to_plus_comp_plus_comp_iso_hom

added theorem category_theory.grothendieck_topology.ι_plus_comp_iso_hom

Created src/category_theory/sites/compatible_sheafification.lean

added def category_theory.grothendieck_topology.sheafification_whisker_left_iso

added theorem category_theory.grothendieck_topology.sheafification_whisker_left_iso_hom_app

added theorem category_theory.grothendieck_topology.sheafification_whisker_left_iso_inv_app

added def category_theory.grothendieck_topology.sheafification_whisker_right_iso

added theorem category_theory.grothendieck_topology.sheafification_whisker_right_iso_hom_app

added theorem category_theory.grothendieck_topology.sheafification_whisker_right_iso_inv_app

added def category_theory.grothendieck_topology.sheafify_comp_iso

added theorem category_theory.grothendieck_topology.sheafify_comp_iso_inv_eq_sheafify_lift

added theorem category_theory.grothendieck_topology.to_sheafify_comp_sheafify_comp_iso_inv

added theorem category_theory.grothendieck_topology.whisker_right_to_sheafify_sheafify_comp_iso_hom

Modified src/category_theory/sites/plus.lean

added def category_theory.grothendieck_topology.diagram_nat_trans

added theorem category_theory.grothendieck_topology.diagram_nat_trans_comp

added theorem category_theory.grothendieck_topology.diagram_nat_trans_id

added theorem category_theory.grothendieck_topology.plus_map_comp

added theorem category_theory.grothendieck_topology.plus_map_id

added theorem category_theory.grothendieck_topology.to_plus_naturality

Modified src/category_theory/sites/sheafification.lean

added theorem category_theory.grothendieck_topology.sheafification_map_sheafify_lift

added theorem category_theory.grothendieck_topology.sheafify_is_sheaf

Modified src/category_theory/sites/whiskering.lean

added theorem category_theory.grothendieck_topology.cover.multicospan_comp_hom_inv_left

added theorem category_theory.grothendieck_topology.cover.multicospan_comp_hom_inv_right