Documentation

Mathlib.CategoryTheory.Sites.IsSheafOneHypercover

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 #

@[reducible, inline]

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 XProp)
Instances For

    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}, SJ.sieves X, ∃ (E : J.OneHypercover X) (_ : H E), E.sieve₀ S
    Instances
      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 ENonempty (CategoryTheory.Limits.IsLimit (E.multifork P))) {X : C} (S : CategoryTheory.Sieve X) (hS : S J.sieves X) {T : A} {x : T P.obj (Opposite.op X)} {y : T P.obj (Opposite.op X)} (h : ∀ ⦃Y : C⦄ (f : Y X), S.arrows fCategoryTheory.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 ENonempty (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 (Opposite.op X)

      Auxiliary definition for isLimit.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        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 ENonempty (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 (Opposite.op (E.X i)) Z) :
        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 ENonempty (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 ENonempty (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) :
        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 ENonempty (CategoryTheory.Limits.IsLimit (E.multifork P))) {X : C} {S : CategoryTheory.Sieve X} {E : J.OneHypercover X} (hE : H E) (le : E.sieve₀ S) :

        Auxiliary definition for OneHypercoverFamily.isSheaf_iff.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[reducible, inline]

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

          Equations
          • J.IsGeneratedByOneHypercovers = .IsGenerating
          Instances For