Characterization of sheaves using 1-hypercovers

In this file, given a Grothendieck topology J on a category C, we define a type J.OneHypercoverFamily of families of 1-hypercovers. When H : J.OneHypercoverFamily, we define a predicate H.IsGenerating which means that any covering sieve contains the sieve generated by the underlying covering of one of the 1-hypercovers in the family. If this holds, we show in OneHypercoverFamily.isSheaf_iff that a presheaf P : Cᵒᵖ ⥤ A is a sheaf iff for any 1-hypercover E in the family, the multifork E.multifork P is limit.

There is a universe parameter w attached to OneHypercoverFamily and OneHypercover. This universe controls the "size" of the 1-hypercovers: the index types involved in the 1-hypercovers have to be in Type w. Then, we introduce a type class GrothendieckTopology.IsGeneratedByOneHypercovers.{w} J as an abbreviation for OneHypercoverFamily.IsGenerating.{w} (J := J) ⊤. We show that if C : Type u and Category.{v} C, then GrothendieckTopology.IsGeneratedByOneHypercovers.{max u v} J holds.

TODO

• Show that functors which preserve 1-hypercovers are continuous.
• Refactor DenseSubsite using 1-hypercovers.

@[reducible, inline]

abbrev CategoryTheory.GrothendieckTopology.OneHypercoverFamily {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) : Type (max (max u (w + 1)) v)

A family of 1-hypercovers consists of the data of a predicate on OneHypercover.{w} J X for all X.

Equations

• J.OneHypercoverFamily = (⦃X : C⦄ → J.OneHypercover X → Prop)

class CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsGenerating {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (H : J.OneHypercoverFamily) : Prop

A family of 1-hypercovers generates the topology if any covering sieve contains the sieve generated by the underlying covering of one of these 1-hypercovers. See OneHypercoverFamily.isSheaf_iff for the characterization of sheaves.

• le {X : C} (S : Sieve X) (hS : S ∈ J X) : ∃ (E : J.OneHypercover X) (_ : H E), E.sieve₀ ≤ S

theorem CategoryTheory.GrothendieckTopology.OneHypercoverFamily.exists_oneHypercover {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (H : J.OneHypercoverFamily) [H.IsGenerating] {X : C} (S : Sieve X) (hS : S ∈ J X) : ∃ (E : J.OneHypercover X) (_ : H E), E.sieve₀ ≤ S

theorem CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.hom_ext {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] (H : J.OneHypercoverFamily) (P : Functor Cᵒᵖ A) (hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (Limits.IsLimit (E.multifork P))) [H.IsGenerating] {X : C} (S : Sieve X) (hS : S ∈ J X) {T : A} {x y : T ⟶ P.obj (Opposite.op X)} (h : ∀ ⦃Y : C⦄ (f : Y ⟶ X), S.arrows f → CategoryStruct.comp x (P.map f.op) = CategoryStruct.comp y (P.map f.op)) : x = y

noncomputable def CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.lift {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] {H : J.OneHypercoverFamily} {P : Functor Cᵒᵖ A} (hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (Limits.IsLimit (E.multifork P))) {X : C} {S : Sieve X} {E : J.OneHypercover X} (hE : H E) (le : E.sieve₀ ≤ S) (F : Limits.Multifork (Cover.index ⟨S, ⋯⟩ P)) : F.pt ⟶ P.obj (Opposite.op X)

Auxiliary definition for isLimit.

Equations

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

theorem CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac' {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] {H : J.OneHypercoverFamily} {P : Functor Cᵒᵖ A} (hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (Limits.IsLimit (E.multifork P))) {X : C} {S : Sieve X} {E : J.OneHypercover X} (hE : H E) (le : E.sieve₀ ≤ S) (F : Limits.Multifork (Cover.index ⟨S, ⋯⟩ P)) (i : E.I₀) : CategoryStruct.comp (lift hP hE le F) (P.map (E.f i).op) = F.ι { Y := E.X i, f := E.f i, hf := ⋯ }

theorem CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac'_assoc {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] {H : J.OneHypercoverFamily} {P : Functor Cᵒᵖ A} (hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (Limits.IsLimit (E.multifork P))) {X : C} {S : Sieve X} {E : J.OneHypercover X} (hE : H E) (le : E.sieve₀ ≤ S) (F : Limits.Multifork (Cover.index ⟨S, ⋯⟩ P)) (i : E.I₀) {Z : A} (h : P.obj (Opposite.op (E.X i)) ⟶ Z) : CategoryStruct.comp (lift hP hE le F) (CategoryStruct.comp (P.map (E.f i).op) h) = CategoryStruct.comp (F.ι { Y := E.X i, f := E.f i, hf := ⋯ }) h

theorem CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] {H : J.OneHypercoverFamily} {P : Functor Cᵒᵖ A} (hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (Limits.IsLimit (E.multifork P))) {X : C} {S : Sieve X} {E : J.OneHypercover X} (hE : H E) (le : E.sieve₀ ≤ S) (F : Limits.Multifork (Cover.index ⟨S, ⋯⟩ P)) [H.IsGenerating] {Y : C} (f : Y ⟶ X) (hf : S.arrows f) : CategoryStruct.comp (lift hP hE le F) (P.map f.op) = F.ι { Y := Y, f := f, hf := hf }

noncomputable def CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.isLimit {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] {H : J.OneHypercoverFamily} {P : Functor Cᵒᵖ A} (hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (Limits.IsLimit (E.multifork P))) {X : C} {S : Sieve X} {E : J.OneHypercover X} (hE : H E) (le : E.sieve₀ ≤ S) [H.IsGenerating] : Limits.IsLimit (Cover.multifork ⟨S, ⋯⟩ P)

Auxiliary definition for OneHypercoverFamily.isSheaf_iff.

Equations

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

theorem CategoryTheory.GrothendieckTopology.OneHypercoverFamily.isSheaf_iff {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] (H : J.OneHypercoverFamily) (P : Functor Cᵒᵖ A) [H.IsGenerating] : Presheaf.IsSheaf J P ↔ ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (Limits.IsLimit (E.multifork P))

@[reducible, inline]

abbrev CategoryTheory.GrothendieckTopology.IsGeneratedByOneHypercovers {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) : Prop

Condition that a topology is generated by 1-hypercovers of size w.

Equations

• J.IsGeneratedByOneHypercovers = ⊤.IsGenerating

instance CategoryTheory.GrothendieckTopology.instIsGeneratedByOneHypercovers {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) : J.IsGeneratedByOneHypercovers

theorem CategoryTheory.Presheaf.isSheaf_iff_of_isGeneratedByOneHypercovers {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) {A : Type u'} [Category.{v', u'} A] [J.IsGeneratedByOneHypercovers] (P : Functor Cᵒᵖ A) : IsSheaf J P ↔ ∀ ⦃X : C⦄ (E : J.OneHypercover X), Nonempty (Limits.IsLimit (E.multifork P))