Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-27 09:46 b8af4914

View on Github →

feat(category_theory/sites/whiskering): Functors between sheaf categories induced by compositiion (#10496) We construct the functor Sheaf J A to Sheaf J B induced by a functor A to B which preserves the appropriate limits.

Estimated changes

Created src/category_theory/sites/whiskering.lean

added def category_theory.Sheaf_compose

added def category_theory.Sheaf_compose_map

added theorem category_theory.Sheaf_compose_map_app

added theorem category_theory.Sheaf_compose_map_app_app

added theorem category_theory.Sheaf_compose_map_comp

added theorem category_theory.Sheaf_compose_map_id

added theorem category_theory.Sheaf_compose_map_to_presheaf

added theorem category_theory.Sheaf_compose_obj_to_presheaf

added def category_theory.grothendieck_topology.cover.map_multifork

added def category_theory.grothendieck_topology.cover.multicospan_comp

added theorem category_theory.grothendieck_topology.cover.multicospan_comp_app_left

added theorem category_theory.grothendieck_topology.cover.multicospan_comp_app_right

added theorem category_theory.grothendieck_topology.cover.multicospan_comp_hom_app_left

added theorem category_theory.grothendieck_topology.cover.multicospan_comp_hom_app_right

added theorem category_theory.presheaf.is_sheaf.comp