Commit 2023-04-17 08:52 7392084b

View on Github →

feat: port CategoryTheory.Sites.Whiskering (#3461)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Sites/Whiskering.lean

added def CategoryTheory.GrothendieckTopology.Cover.mapMultifork

added def CategoryTheory.GrothendieckTopology.Cover.multicospanComp

added theorem CategoryTheory.GrothendieckTopology.Cover.multicospanComp_app_left

added theorem CategoryTheory.GrothendieckTopology.Cover.multicospanComp_app_right

added theorem CategoryTheory.GrothendieckTopology.Cover.multicospanComp_hom_app_left

added theorem CategoryTheory.GrothendieckTopology.Cover.multicospanComp_hom_app_right

added theorem CategoryTheory.GrothendieckTopology.Cover.multicospanComp_hom_inv_left

added theorem CategoryTheory.GrothendieckTopology.Cover.multicospanComp_hom_inv_right

added theorem CategoryTheory.Presheaf.IsSheaf.comp

added def CategoryTheory.sheafCompose