Commit 2026-01-30 07:22 e54dcdb9

View on Github →

feat(CategoryTheory): the yoneda embedding to sheaves preserves disjoint coproducts (#34145) From Proetale.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/Shapes/DisjointCoproduct.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Products.lean

added def CategoryTheory.Limits.Cofan.isColimitMapCoconeEquiv

added def CategoryTheory.Limits.Fan.isLimitMapConeEquiv

Modified Mathlib/CategoryTheory/Sites/Sieves.lean

added def CategoryTheory.Sieve.toFunctor

Modified Mathlib/CategoryTheory/Sites/Subcanonical.lean

added theorem CategoryTheory.GrothendieckTopology.preservesColimitsOfShape_yoneda_of_ofArrows_inj_mem