Documentation

Mathlib.CategoryTheory.Sites.CoproductSheafCondition

The sheaf condition and universal coproducts #

In this file we show that if { fᵢ : Yᵢ ⟶ X } is a family of morphisms and ∐ᵢ Yᵢ is a universal coproduct, then any presheaf F that preserves products is a sheaf for the single object covering { ∐ᵢ Yᵢ ⟶ X } if and only if it is a sheaf for { fᵢ : Yᵢ ⟶ X }ᵢ.

We provide both a version for a general coefficient category and one for type values presheafs.

source
noncomputable def CategoryTheory.PreZeroHypercover.isLimitSigmaOfIsColimitEquiv {C : Type u_1} [Category.{v_1, u_1} C] {A : Type u_2} [Category.{v_2, u_2} A] {S : C} (E : PreZeroHypercover S) [E.HasPullbacks] {c : Limits.Cofan E.X} (hc : Limits.IsColimit c) (huniv : IsUniversalColimit c) [(E.sigmaOfIsColimit hc).HasPullbacks] [∀ (i : E.I₀), Limits.HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)] (F : Functor Cᵒᵖ A) [Limits.PreservesLimit (Discrete.functor fun (i : E.toPreOneHypercover.I₀) => Opposite.op (E.toPreOneHypercover.X i)) F] [Limits.PreservesLimit (Discrete.functor fun (i : E.toPreOneHypercover.I₁') => Opposite.op (E.toPreOneHypercover.Y' i)) F] :
Limits.IsLimit ((E.sigmaOfIsColimit hc).toPreOneHypercover.multifork F) ≃ Limits.IsLimit (E.toPreOneHypercover.multifork F)

Let E be a pre-0-hypercover with pairwise pullbacks. If ∐ᵢ Eᵢ is a universal coproduct and the presheaf F preserves products, then the multifork associated to the single object 0-hypercover { ∐ᵢ Eᵢ ⟶ S } is exact if and only if the multifork for E is exact.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem CategoryTheory.Presieve.isSheafFor_sigmaDesc_iff {C : Type u_1} [Category.{v_1, u_1} C] {S : C} {ι : Type u_3} {X : ι → C} (f : (i : ι) → X i ⟶ S) [(ofArrows X f).HasPairwisePullbacks] {c : Limits.Cofan X} (hc : Limits.IsColimit c) (hc' : IsUniversalColimit c) [Limits.HasPullback (Limits.Cofan.IsColimit.desc hc f) (Limits.Cofan.IsColimit.desc hc f)] [∀ (i : ι), Limits.HasPullback (f i) (Limits.Cofan.IsColimit.desc hc f)] (F : Functor Cᵒᵖ (Type u_4)) [Limits.PreservesLimit (Discrete.functor fun (i : ι) => Opposite.op (X i)) F] [Limits.PreservesLimit (Discrete.functor fun (ij : ι × ι) => Opposite.op (Limits.pullback (f ij.1) (f ij.2))) F] :
    IsSheafFor F (singleton (Limits.Cofan.IsColimit.desc hc f)) ↔ IsSheafFor F (ofArrows X f)

    Let { fᵢ : Xᵢ ⟶ S } be a family of morphisms. If ∐ᵢ Xᵢ is a universal coproduct and the presheaf F preserves products, then F is a sheaf for the single object covering { ∐ᵢ Xᵢ ⟶ S } if and only if it is a sheaf for { fᵢ : Xᵢ ⟶ S }ᵢ.