1-hypercovers and (pre)sheaves of types

In this file we provide some API for working with 1-hypercovers for sheaves of types.

Main declarations

• CategoryTheory.PreOneHypercover.IsStronglySheafFor: A pre-1-hypercover E satisfies the strong sheaf condition for a presheaf of types F if F is a sheaf for the 0-covering and separated for the 1-coverings.
• CategoryTheory.PreOneHypercover.IsStronglySheafFor.amalgamate: Glue a family of compatible sections along E if E satisfies the strong sheaf condition.
• CategoryTheory.PreOneHypercover.IsStronglySheafFor.isLimitMultifork: If E satisfies the strong sheaf condition for F, then the multiequalizer diagram for E is limiting.

def CategoryTheory.PreZeroHypercover.sectionsEquivOfHasPullbacks {C : Type u_1} [Category.{v_1, u_1} C] {S : C} (E : PreZeroHypercover S) [E.HasPullbacks] (F : Functor Cᵒᵖ (Type u_2)) : (E.toPreOneHypercover.multicospanIndex F).sections ≃ Subtype (Presieve.Arrows.Compatible F E.f)

If the pre-0-hypercover E has pairwise pullbacks, the sections over the multifork associated to a presheaf of types are equivalent to the compatible families on E.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.PreZeroHypercover.sectionsEquivOfHasPullbacks_symm_apply_val {C : Type u_1} [Category.{v_1, u_1} C] {S : C} (E : PreZeroHypercover S) [E.HasPullbacks] (F : Functor Cᵒᵖ (Type u_2)) (s : Subtype (Presieve.Arrows.Compatible F E.f)) (i : E.I₀) : ((E.sectionsEquivOfHasPullbacks F).symm s).val i = ↑s i

@[simp]

theorem CategoryTheory.PreZeroHypercover.sectionsEquivOfHasPullbacks_apply_coe {C : Type u_1} [Category.{v_1, u_1} C] {S : C} (E : PreZeroHypercover S) [E.HasPullbacks] (F : Functor Cᵒᵖ (Type u_2)) (s : (E.toPreOneHypercover.multicospanIndex F).sections) (i : E.toPreOneHypercover.multicospanShape.L) : ↑((E.sectionsEquivOfHasPullbacks F) s) i = s.val i

theorem CategoryTheory.PreZeroHypercover.isLimit_toPreOneHypercover_type_iff {C : Type u_1} [Category.{v_1, u_1} C] {S : C} (E : PreZeroHypercover S) [E.HasPullbacks] (F : Functor Cᵒᵖ (Type u_2)) : Nonempty (Limits.IsLimit (E.toPreOneHypercover.multifork F)) ↔ Presieve.IsSheafFor F E.presieve₀

theorem CategoryTheory.Precoverage.ZeroHypercover.Hom.isSheafFor_iff {C : Type u_1} [Category.{v_1, u_1} C] [Limits.HasPullbacks C] {K : Precoverage C} [K.IsStableUnderBaseChange] {S : C} {F : Functor Cᵒᵖ (Type u_2)} {𝒰 : K.ZeroHypercover S} {𝒱 : K.ZeroHypercover S} (f : Hom K 𝒰 𝒱) (H₁ : Presieve.IsSheafFor F (Presieve.ofArrows 𝒰.X 𝒰.f)) (H₂ : ∀ {X : C} (f : X ⟶ S), Presieve.IsSeparatedFor F (Presieve.ofArrows (pullback₂ f 𝒰).X (pullback₂ f 𝒰).f)) : Presieve.IsSheafFor F (Presieve.ofArrows 𝒱.X 𝒱.f)

structure CategoryTheory.PreOneHypercover.IsStronglySeparatedFor {C : Type u_1} [Category.{v_1, u_1} C] {X : C} (E : PreOneHypercover X) (F : Functor Cᵒᵖ (Type u_3)) : Prop

A presheaf F of types is (strongly) separated for a pre-1-hypercover if F is separated for both the 0 and the 1-components.

• isSeparatedFor_presieve₀ : Presieve.IsSeparatedFor F E.presieve₀
• isSeparatedFor_sieve₁ ⦃i j : E.I₀⦄ ⦃W : C⦄ (p₁ : W ⟶ E.X i) (p₂ : W ⟶ E.X j) (h : CategoryStruct.comp p₁ (E.f i) = CategoryStruct.comp p₂ (E.f j)) : Presieve.IsSeparatedFor F (E.sieve₁ p₁ p₂).arrows

structure CategoryTheory.PreOneHypercover.IsStronglySheafFor {C : Type u_1} [Category.{v_1, u_1} C] {X : C} (E : PreOneHypercover X) (F : Functor Cᵒᵖ (Type u_3)) : Prop

A presheaf F of types is (strongly) a sheaf for a pre-1-hypercover if F is a sheaf for both the 0 and the 1-components. This implies that the multiequalizer diagram attached to E is exact (see CategoryTheory.PreOneHypercover.IsStronglySheafFor.isLimitMultifork).

• isSheafFor_presieve₀ : Presieve.IsSheafFor F E.presieve₀
• isSeparatedFor_sieve₁ ⦃i j : E.I₀⦄ ⦃W : C⦄ (p₁ : W ⟶ E.X i) (p₂ : W ⟶ E.X j) (h : CategoryStruct.comp p₁ (E.f i) = CategoryStruct.comp p₂ (E.f j)) : Presieve.IsSeparatedFor F (E.sieve₁ p₁ p₂).arrows

theorem CategoryTheory.PreOneHypercover.IsStronglySheafFor.isStronglySeparatedFor {C : Type u_1} [Category.{v_1, u_1} C] {X : C} {E : PreOneHypercover X} {F : Functor Cᵒᵖ (Type u_2)} (h : E.IsStronglySheafFor F) : E.IsStronglySeparatedFor F

theorem CategoryTheory.PreOneHypercover.IsStronglySeparatedFor.arrowsCompatible {C : Type u_1} [Category.{v_1, u_1} C] {X : C} {E : PreOneHypercover X} {F : Functor Cᵒᵖ (Type u_2)} (h : E.IsStronglySeparatedFor F) (x : (i : E.I₀) → F.obj (Opposite.op (E.X i))) (hc : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (ConcreteCategory.hom (F.map (E.p₁ k).op)) (x i) = (ConcreteCategory.hom (F.map (E.p₂ k).op)) (x j)) : Presieve.Arrows.Compatible F E.f x

noncomputable def CategoryTheory.PreOneHypercover.IsStronglySheafFor.amalgamate {C : Type u_1} [Category.{v_1, u_1} C] {X : C} {E : PreOneHypercover X} {F : Functor Cᵒᵖ (Type u_2)} (h : E.IsStronglySheafFor F) (x : (i : E.I₀) → F.obj (Opposite.op (E.X i))) (hc : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (ConcreteCategory.hom (F.map (E.p₁ k).op)) (x i) = (ConcreteCategory.hom (F.map (E.p₂ k).op)) (x j)) : F.obj (Opposite.op X)

Glue sections of a Type-valued sheaf over a 1-hypercover.

Equations

• h.amalgamate x hc = ⋯.amalgamate ⋯.familyOfElements ⋯

@[simp]

theorem CategoryTheory.PreOneHypercover.IsStronglySheafFor.map_amalgamate {C : Type u_1} [Category.{v_1, u_1} C] {X : C} {E : PreOneHypercover X} {F : Functor Cᵒᵖ (Type u_2)} (h : E.IsStronglySheafFor F) (x : (i : E.I₀) → F.obj (Opposite.op (E.X i))) (hc : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), (ConcreteCategory.hom (F.map (E.p₁ k).op)) (x i) = (ConcreteCategory.hom (F.map (E.p₂ k).op)) (x j)) (i : E.I₀) : (ConcreteCategory.hom (F.map (E.f i).op)) (h.amalgamate x hc) = x i

noncomputable def CategoryTheory.PreOneHypercover.IsStronglySheafFor.isLimitMultifork {C : Type u_1} [Category.{v_1, u_1} C] {X : C} {E : PreOneHypercover X} {F : Functor Cᵒᵖ (Type u_2)} (h : E.IsStronglySheafFor F) : Limits.IsLimit (E.multifork F)

F satisfies the (strong) sheaf condition for the pre-1-hypercover E, then the multiequalizer diagram attached to E is limiting.

Equations

• h.isLimitMultifork = ⋯.some

theorem CategoryTheory.PreOneHypercover.IsStronglySheafFor.isSheafFor_sieve_of_pullback {C : Type u_1} [Category.{v_1, u_1} C] {X : C} {E : PreOneHypercover X} {F : Functor Cᵒᵖ (Type u_2)} (h₁ : E.IsStronglySheafFor F) (h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor F (Sieve.pullback f E.sieve₀).arrows) {S : Sieve X} (H : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows) (H' : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (CategoryStruct.comp (E.p₁ k) (E.f i)) S).arrows) : Presieve.IsSheafFor F S.arrows

theorem CategoryTheory.PreOneHypercover.IsStronglySheafFor.isSheafFor_of_pullback {C : Type u_1} [Category.{v_1, u_1} C] {X : C} {E : PreOneHypercover X} {F : Functor Cᵒᵖ (Type u_2)} (h₁ : E.IsStronglySheafFor F) (h₂ : ∀ ⦃Y : C⦄ (f : Y ⟶ X), Presieve.IsSeparatedFor F (Sieve.pullback f E.sieve₀).arrows) {R : Presieve X} (H : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) (Sieve.generate R)).arrows) (H' : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (Sieve.generate R)).arrows) : Presieve.IsSheafFor F R

Being a sheaf for a presieve R is local on the target in the following sense: If E is a pre-1-hypercover for which F is separated and a sheaf for the 0-components, then to check that F is a sheaf for R it suffices to check:

• F is a sheaf for the pullbacks of R along the maps from the 0-components.
• F is separated for the pullbacks of R along the maps from the 1-components.

theorem CategoryTheory.GrothendieckTopology.OneHypercover.isStronglySeparatedFor {C : Type u_1} [Category.{v_1, u_1} C] {J : GrothendieckTopology C} {X : C} {E : J.OneHypercover X} {F : Functor Cᵒᵖ (Type u_2)} (hf : Presieve.IsSeparated J F) : E.IsStronglySeparatedFor F

theorem CategoryTheory.GrothendieckTopology.OneHypercover.isStronglySheafFor {C : Type u_1} [Category.{v_1, u_1} C] {J : GrothendieckTopology C} {X : C} {E : J.OneHypercover X} {F : Functor Cᵒᵖ (Type u_2)} (hf : Presieve.IsSheaf J F) : E.IsStronglySheafFor F

theorem CategoryTheory.GrothendieckTopology.OneHypercover.isSheafFor_sieve_of_pullback {C : Type u_1} [Category.{v_1, u_1} C] {J : GrothendieckTopology C} {X : C} (E : J.OneHypercover X) {F : Functor Cᵒᵖ (Type u_2)} (hF : Presieve.IsSheaf J F) {S : Sieve X} (h₁ : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) S).arrows) (h₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (CategoryStruct.comp (E.p₁ k) (E.f i)) S).arrows) : Presieve.IsSheafFor F S.arrows

theorem CategoryTheory.GrothendieckTopology.OneHypercover.isSheafFor_of_pullback {C : Type u_1} [Category.{v_1, u_1} C] {J : GrothendieckTopology C} {X : C} {E : J.OneHypercover X} {F : Functor Cᵒᵖ (Type u_2)} (hF : Presieve.IsSheaf J F) {R : Presieve X} (h₁ : ∀ (i : E.I₀), Presieve.IsSheafFor F (Sieve.pullback (E.f i) (Sieve.generate R)).arrows) (h₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), Presieve.IsSeparatedFor F (Sieve.pullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (Sieve.generate R)).arrows) : Presieve.IsSheafFor F R

If F is a J-sheaf, then being a sheaf for a presieve R is J-local on the target, i.e. it can be checked on the pullbacks from a 1-hypercover.