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} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.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 ∈ J.sieves X, ∃ (E : J.OneHypercover X) (_ : H E), E.sieve₀ ≤ S

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

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

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

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

Auxiliary definition for isLimit.

Equations

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

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

theorem CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac' {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] {H : J.OneHypercoverFamily} {P : CategoryTheory.Functor Cᵒᵖ A} (hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (CategoryTheory.Limits.IsLimit (E.multifork P))) {X : C} {S : CategoryTheory.Sieve X} {E : J.OneHypercover X} (hE : H E) (le : E.sieve₀ ≤ S) (F : CategoryTheory.Limits.Multifork (CategoryTheory.GrothendieckTopology.Cover.index ⟨S, ⋯⟩ P)) (i : E.I₀) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.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 {C : Type u} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] {H : J.OneHypercoverFamily} [H.IsGenerating] {P : CategoryTheory.Functor Cᵒᵖ A} (hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (CategoryTheory.Limits.IsLimit (E.multifork P))) {X : C} {S : CategoryTheory.Sieve X} {E : J.OneHypercover X} (hE : H E) (le : E.sieve₀ ≤ S) (F : CategoryTheory.Limits.Multifork (CategoryTheory.GrothendieckTopology.Cover.index ⟨S, ⋯⟩ P)) {Y : C} (f : Y ⟶ X) (hf : S.arrows f) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.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} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] {H : J.OneHypercoverFamily} [H.IsGenerating] {P : CategoryTheory.Functor Cᵒᵖ A} (hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (CategoryTheory.Limits.IsLimit (E.multifork P))) {X : C} {S : CategoryTheory.Sieve X} {E : J.OneHypercover X} (hE : H E) (le : E.sieve₀ ≤ S) : CategoryTheory.Limits.IsLimit (CategoryTheory.GrothendieckTopology.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} [CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [CategoryTheory.Category.{v', u'} A] (H : J.OneHypercoverFamily) [H.IsGenerating] (P : CategoryTheory.Functor Cᵒᵖ A) : CategoryTheory.Presheaf.IsSheaf J P ↔ ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (CategoryTheory.Limits.IsLimit (E.multifork P))

@[reducible, inline]

abbrev CategoryTheory.GrothendieckTopology.IsGeneratedByOneHypercovers {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.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} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) : J.IsGeneratedByOneHypercovers

Equations

• ⋯ = ⋯

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