Commit 2025-12-10 15:34 460512ef

View on Github →

feat(CategoryTheory/Sites/Hypercover): pre-1-hypercover obtained by taking coproducts of the components (#32578) We show that satisfying the sheaf condition for a pre-1-hypercover E is the same as satisfying the sheaf condition for E collapsed to a single object covering by taking coproducts.

Estimated changes

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

added def CategoryTheory.Limits.Fork.equivOfIsos

added theorem CategoryTheory.Limits.Fork.equivOfIsos_functor_obj_ι

added theorem CategoryTheory.Limits.Fork.equivOfIsos_inverse_obj_ι

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

added def CategoryTheory.Limits.Multicofork.isoOfπ

added def CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork

added theorem CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork_functor_obj_ι

added theorem CategoryTheory.Limits.MulticospanIndex.multiforkOfParallelHomsEquivFork_inverse_obj_ι

added def CategoryTheory.Limits.MulticospanIndex.ofParallelHoms

added def CategoryTheory.Limits.Multifork.ext

added def CategoryTheory.Limits.Multifork.isLimitEquivOfIsos

added def CategoryTheory.Limits.Multifork.isoOfι

added theorem CategoryTheory.Limits.Multifork.ι_ofι

added def CategoryTheory.Limits.WalkingMulticospan.functorExt

added def CategoryTheory.Limits.WalkingMultispan.functorExt

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

added def CategoryTheory.Limits.Cofan.isColimitMkOfUnique

added def CategoryTheory.Limits.Fan.isLimitMkOfUnique

Modified Mathlib/CategoryTheory/Sites/Hypercover/One.lean

added def CategoryTheory.PreOneHypercover.Y'

added theorem CategoryTheory.PreOneHypercover.Y'_apply

added def CategoryTheory.PreOneHypercover.forkOfIsColimit

added theorem CategoryTheory.PreOneHypercover.forkOfIsColimit_ι_map_inj

added def CategoryTheory.PreOneHypercover.isLimitSigmaOfIsColimitEquiv

added theorem CategoryTheory.PreOneHypercover.multifork_ι

added theorem CategoryTheory.PreOneHypercover.p₁_sigmaOfIsColimit

added theorem CategoryTheory.PreOneHypercover.p₂_sigmaOfIsColimit

added def CategoryTheory.PreOneHypercover.sigmaOfIsColimit

Modified Mathlib/CategoryTheory/Sites/Hypercover/Zero.lean

added theorem CategoryTheory.PreZeroHypercover.inj_sigmaOfIsColimit_f

added def CategoryTheory.PreZeroHypercover.sigmaOfIsColimit

Modified Mathlib/CategoryTheory/Sites/Limits.lean