Equivalence of categories of sheaves with a dense subsite that is 1-hypercover dense

Let F : C₀ ⥤ C be a functor equipped with Grothendieck topologies J₀ and J. Assume that F is a dense subsite. We introduce a typeclass IsOneHypercoverDense.{w} F J₀ J which roughly says that objects in C admit a 1-hypercover consisting of objects in C₀.

structure CategoryTheory.Functor.PreOneHypercoverDenseData {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] (F : Functor C₀ C) (S : C) : Type (max (max (max u₀ v) v₀) (w + 1))

Given a functor F : C₀ ⥤ C and an object S : C, this structure roughly contains the data of a pre-1-hypercover of S consisting of objects in C₀.

• I₀ : Type w

  the index type of the covering of S

• X (i : self.I₀) : C₀

  the objects in the covering of S

• f (i : self.I₀) : F.obj (self.X i) ⟶ S

  the morphisms in the covering of S

• I₁ (i₁ i₂ : self.I₀) : Type w

  the index type of the coverings of the fibre products

• Y ⦃i₁ i₂ : self.I₀⦄ (j : self.I₁ i₁ i₂) : C₀

  the objects in the coverings of the fibre products

• p₁ ⦃i₁ i₂ : self.I₀⦄ (j : self.I₁ i₁ i₂) : self.Y j ⟶ self.X i₁

  the first projection Y j ⟶ X i₁

• p₂ ⦃i₁ i₂ : self.I₀⦄ (j : self.I₁ i₁ i₂) : self.Y j ⟶ self.X i₂

  the second projection Y j ⟶ X i₂

• w ⦃i₁ i₂ : self.I₀⦄ (j : self.I₁ i₁ i₂) : CategoryStruct.comp (F.map (self.p₁ j)) (self.f i₁) = CategoryStruct.comp (F.map (self.p₂ j)) (self.f i₂)

theorem CategoryTheory.Functor.PreOneHypercoverDenseData.w_assoc {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {S : C} (self : F.PreOneHypercoverDenseData S) ⦃i₁ i₂ : self.I₀⦄ (j : self.I₁ i₁ i₂) {Z : C} (h : S ⟶ Z) : CategoryStruct.comp (F.map (self.p₁ j)) (CategoryStruct.comp (self.f i₁) h) = CategoryStruct.comp (F.map (self.p₂ j)) (CategoryStruct.comp (self.f i₂) h)

def CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {X : C} (data : F.PreOneHypercoverDenseData X) : PreOneHypercover X

The pre-1-hypercover induced by a PreOneHypercoverDenseData structure.

@[simp]

theorem CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover_I₁ {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {X : C} (data : F.PreOneHypercoverDenseData X) (i₁ i₂ : data.I₀) : data.toPreOneHypercover.I₁ i₁ i₂ = data.I₁ i₁ i₂

@[simp]

theorem CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover_I₀ {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {X : C} (data : F.PreOneHypercoverDenseData X) : data.toPreOneHypercover.I₀ = data.I₀

@[simp]

theorem CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover_p₁ {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {X : C} (data : F.PreOneHypercoverDenseData X) (x✝ x✝¹ : data.I₀) (j : data.I₁ x✝ x✝¹) : data.toPreOneHypercover.p₁ j = F.map (data.p₁ j)

@[simp]

theorem CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover_p₂ {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {X : C} (data : F.PreOneHypercoverDenseData X) (x✝ x✝¹ : data.I₀) (j : data.I₁ x✝ x✝¹) : data.toPreOneHypercover.p₂ j = F.map (data.p₂ j)

@[simp]

theorem CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover_Y {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {X : C} (data : F.PreOneHypercoverDenseData X) (x✝ x✝¹ : data.I₀) (j : data.I₁ x✝ x✝¹) : data.toPreOneHypercover.Y j = F.obj (data.Y j)

@[simp]

theorem CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover_X {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {X : C} (data : F.PreOneHypercoverDenseData X) (i : data.I₀) : data.toPreOneHypercover.X i = F.obj (data.X i)

@[simp]

theorem CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover_f {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {X : C} (data : F.PreOneHypercoverDenseData X) (i : data.I₀) : data.toPreOneHypercover.f i = data.f i

@[reducible, inline]

abbrev CategoryTheory.Functor.PreOneHypercoverDenseData.I₁' {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {X : C} (data : F.PreOneHypercoverDenseData X) : Type w

The sigma type of all data.I₁ i₁ i₂ for ⟨i₁, i₂⟩ : data.I₀ × data.I₀.

def CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanShape {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {X : C} (data : F.PreOneHypercoverDenseData X) : Limits.MulticospanShape

The shape of the multiforks attached to data : F.PreOneHypercoverDenseData X.

@[simp]

theorem CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanShape_L {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {X : C} (data : F.PreOneHypercoverDenseData X) : data.multicospanShape.L = data.I₀

@[simp]

theorem CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanShape_snd {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {X : C} (data : F.PreOneHypercoverDenseData X) (j : data.I₁') : data.multicospanShape.snd j = j.fst.2

@[simp]

theorem CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanShape_fst {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {X : C} (data : F.PreOneHypercoverDenseData X) (j : data.I₁') : data.multicospanShape.fst j = j.fst.1

@[simp]

theorem CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanShape_R {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {X : C} (data : F.PreOneHypercoverDenseData X) : data.multicospanShape.R = data.I₁'

def CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanIndex {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {A : Type u'} [Category.{v', u'} A] {X : C} (data : F.PreOneHypercoverDenseData X) (P : Functor C₀ᵒᵖ A) : Limits.MulticospanIndex data.multicospanShape A

The diagram of the multiforks attached to data : F.PreOneHypercoverDenseData X.

@[simp]

theorem CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanIndex_left {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {A : Type u'} [Category.{v', u'} A] {X : C} (data : F.PreOneHypercoverDenseData X) (P : Functor C₀ᵒᵖ A) (i : data.multicospanShape.L) : (data.multicospanIndex P).left i = P.obj (Opposite.op (data.X i))

@[simp]

theorem CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanIndex_snd {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {A : Type u'} [Category.{v', u'} A] {X : C} (data : F.PreOneHypercoverDenseData X) (P : Functor C₀ᵒᵖ A) (j : data.multicospanShape.R) : (data.multicospanIndex P).snd j = P.map (data.p₂ j.snd).op

@[simp]

theorem CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanIndex_fst {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {A : Type u'} [Category.{v', u'} A] {X : C} (data : F.PreOneHypercoverDenseData X) (P : Functor C₀ᵒᵖ A) (j : data.multicospanShape.R) : (data.multicospanIndex P).fst j = P.map (data.p₁ j.snd).op

@[simp]

theorem CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanIndex_right {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {A : Type u'} [Category.{v', u'} A] {X : C} (data : F.PreOneHypercoverDenseData X) (P : Functor C₀ᵒᵖ A) (j : data.multicospanShape.R) : (data.multicospanIndex P).right j = P.obj (Opposite.op (data.Y j.snd))

def CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanMap {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {A : Type u'} [Category.{v', u'} A] {X : C} (data : F.PreOneHypercoverDenseData X) {P Q : Functor C₀ᵒᵖ A} (f : P ⟶ Q) : (data.multicospanIndex P).multicospan ⟶ (data.multicospanIndex Q).multicospan

The functoriality of the diagrams attached to data : F.PreOneHypercoverDenseData X with respect to morphisms in C₀ᵒᵖ ⥤ A.

@[simp]

theorem CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanMap_app {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {A : Type u'} [Category.{v', u'} A] {X : C} (data : F.PreOneHypercoverDenseData X) {P Q : Functor C₀ᵒᵖ A} (f : P ⟶ Q) (x : Limits.WalkingMulticospan data.multicospanShape) : (data.multicospanMap f).app x = match x with | Limits.WalkingMulticospan.left i => f.app (Opposite.op (data.X i)) | Limits.WalkingMulticospan.right j => f.app (Opposite.op (data.Y j.snd))

def CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanMapIso {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {A : Type u'} [Category.{v', u'} A] {X : C} (data : F.PreOneHypercoverDenseData X) {P Q : Functor C₀ᵒᵖ A} (e : P ≅ Q) : (data.multicospanIndex P).multicospan ≅ (data.multicospanIndex Q).multicospan

The natural isomorphism between the diagrams attached to data : F.PreOneHypercoverDenseData X that are induced by isomorphisms in C₀ᵒᵖ ⥤ A.

@[simp]

theorem CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanMapIso_hom {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {A : Type u'} [Category.{v', u'} A] {X : C} (data : F.PreOneHypercoverDenseData X) {P Q : Functor C₀ᵒᵖ A} (e : P ≅ Q) : (data.multicospanMapIso e).hom = data.multicospanMap e.hom

@[simp]

theorem CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanMapIso_inv {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {A : Type u'} [Category.{v', u'} A] {X : C} (data : F.PreOneHypercoverDenseData X) {P Q : Functor C₀ᵒᵖ A} (e : P ≅ Q) : (data.multicospanMapIso e).inv = data.multicospanMap e.inv

def CategoryTheory.Functor.PreOneHypercoverDenseData.sieve₁₀ {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {X : C} (data : F.PreOneHypercoverDenseData X) {i₁ i₂ : data.I₀} {W₀ : C₀} (p₁ : W₀ ⟶ data.X i₁) (p₂ : W₀ ⟶ data.X i₂) : Sieve W₀

Given data : F.PreOneHypercoverDenseData X, an object W₀ : C₀ and two morphisms p₁ : W₀ ⟶ data.X i₁ and p₂ : W₀ ⟶ data.X i₂, this is the sieve of W₀ consisting of morphisms g : Z₀ ⟶ W₀ such that there exists a morphism Z₀ ⟶ data.Y j such that g ≫ p₁ = h ≫ data.p₁ j and g ≫ p₂ = h ≫ data.p₂ j.

@[simp]

theorem CategoryTheory.Functor.PreOneHypercoverDenseData.sieve₁₀_apply {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {X : C} (data : F.PreOneHypercoverDenseData X) {i₁ i₂ : data.I₀} {W₀ : C₀} (p₁ : W₀ ⟶ data.X i₁) (p₂ : W₀ ⟶ data.X i₂) (Z₀ : C₀) (g : Z₀ ⟶ W₀) : (data.sieve₁₀ p₁ p₂).arrows g = ∃ (j : data.I₁ i₁ i₂) (h : Z₀ ⟶ data.Y j), CategoryStruct.comp g p₁ = CategoryStruct.comp h (data.p₁ j) ∧ CategoryStruct.comp g p₂ = CategoryStruct.comp h (data.p₂ j)

structure CategoryTheory.Functor.OneHypercoverDenseData {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] (F : Functor C₀ C) (J₀ : GrothendieckTopology C₀) (J : GrothendieckTopology C) (S : C) extends F.PreOneHypercoverDenseData S : Type (max (max (max u₀ v) v₀) (w + 1))

Given a functor F : C₀ ⥤ C, Grothendieck topologies J₀ on C₀ and J on C, an object S. : C, this structure roughly contains the data of a 1-hypercover of S consisting of objects in C₀.

• I₀ : Type w
• X (i : self.I₀) : C₀
• f (i : self.I₀) : F.obj (self.X i) ⟶ S
• I₁ (i₁ i₂ : self.I₀) : Type w
• Y ⦃i₁ i₂ : self.I₀⦄ (j : self.I₁ i₁ i₂) : C₀
• p₁ ⦃i₁ i₂ : self.I₀⦄ (j : self.I₁ i₁ i₂) : self.Y j ⟶ self.X i₁
• p₂ ⦃i₁ i₂ : self.I₀⦄ (j : self.I₁ i₁ i₂) : self.Y j ⟶ self.X i₂
• w ⦃i₁ i₂ : self.I₀⦄ (j : self.I₁ i₁ i₂) : CategoryStruct.comp (F.map (self.p₁ j)) (self.f i₁) = CategoryStruct.comp (F.map (self.p₂ j)) (self.f i₂)
• mem₀ : self.toPreOneHypercover.sieve₀ ∈ J S
• mem₁₀ (i₁ i₂ : self.I₀) ⦃W₀ : C₀⦄ (p₁ : W₀ ⟶ self.X i₁) (p₂ : W₀ ⟶ self.X i₂) (w : CategoryStruct.comp (F.map p₁) (self.f i₁) = CategoryStruct.comp (F.map p₂) (self.f i₂)) : self.sieve₁₀ p₁ p₂ ∈ J₀ W₀

class CategoryTheory.Functor.IsOneHypercoverDense {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] (F : Functor C₀ C) (J₀ : GrothendieckTopology C₀) (J : GrothendieckTopology C) : Prop

Given a functor F : C₀ ⥤ C, Grothendieck topologies J₀ on C₀, this is the property that any object in C has a 1-hypercover consisting of objects in C₀.

• nonempty_oneHypercoverDenseData (X : C) : Nonempty (F.OneHypercoverDenseData J₀ J X)

noncomputable def CategoryTheory.Functor.oneHypercoverDenseData {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] (F : Functor C₀ C) (J₀ : GrothendieckTopology C₀) (J : GrothendieckTopology C) [F.IsOneHypercoverDense J₀ J] (X : C) : F.OneHypercoverDenseData J₀ J X

A choice of a OneHypercoverDenseData structure when F is 1-hypercover dense.

theorem CategoryTheory.Functor.isDenseSubsite_of_isOneHypercoverDense {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] (F : Functor C₀ C) (J₀ : GrothendieckTopology C₀) (J : GrothendieckTopology C) [F.IsOneHypercoverDense J₀ J] [F.IsLocallyFull J] [F.IsLocallyFaithful J] (h : ∀ {X₀ : C₀} {S₀ : Sieve X₀}, Sieve.functorPushforward F S₀ ∈ J.sieves (F.obj X₀) ↔ S₀ ∈ J₀.sieves X₀) : IsDenseSubsite J₀ J F

theorem CategoryTheory.Functor.IsOneHypercoverDense.of_hasPullbacks {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} [IsDenseSubsite J₀ J F] [Limits.HasPullbacks C] [F.Full] [F.Faithful] (hF : ∀ (S : C), ∃ (ι : Type w) (U : ι → C₀) (f : (i : ι) → F.obj (U i) ⟶ S), Sieve.ofArrows (fun (i : ι) => F.obj (U i)) f ∈ J S) : F.IsOneHypercoverDense J₀ J

Constructor for IsOneHypercoverDense.{w} F J₀ J for a dense subsite when the functor F : C₀ ⥤ C is fully faithful, C has pullbacks, and any object in C admits a w-small covering family consisting of objects in C₀.

theorem CategoryTheory.Functor.OneHypercoverDenseData.mem₁ {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} [IsDenseSubsite J₀ J F] {X : C} (data : F.OneHypercoverDenseData J₀ J X) (i₁ i₂ : data.I₀) {W : C} (p₁ : W ⟶ F.obj (data.X i₁)) (p₂ : W ⟶ F.obj (data.X i₂)) (w : CategoryStruct.comp p₁ (data.f i₁) = CategoryStruct.comp p₂ (data.f i₂)) : data.toPreOneHypercover.sieve₁ p₁ p₂ ∈ J W

def CategoryTheory.Functor.OneHypercoverDenseData.toOneHypercover {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} [IsDenseSubsite J₀ J F] {X : C} (data : F.OneHypercoverDenseData J₀ J X) : J.OneHypercover X

The 1-hypercover associated to a OneHypercoverDenseData structure.

@[simp]

theorem CategoryTheory.Functor.OneHypercoverDenseData.toOneHypercover_toPreOneHypercover {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} [IsDenseSubsite J₀ J F] {X : C} (data : F.OneHypercoverDenseData J₀ J X) : data.toOneHypercover.toPreOneHypercover = data.toPreOneHypercover

structure CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {X : C} (data : F.OneHypercoverDenseData J₀ J X) {X₀ : C₀} (f : F.obj X₀ ⟶ X) {Y₀ : C₀} (g : Y₀ ⟶ X₀) : Type (max v w)

Auxiliary structure for the definition OneHypercoverDenseData.sieve.

• i₀ : data.I₀

  the index of the intermediate object

• q : F.obj Y₀ ⟶ F.obj (data.X self.i₀)

  the morphism that is part of the factorization fac.

• fac : CategoryStruct.comp self.q (data.f self.i₀) = CategoryStruct.comp (F.map g) f

@[simp]

theorem CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.fac_assoc {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {X : C} {data : F.OneHypercoverDenseData J₀ J X} {X₀ : C₀} {f : F.obj X₀ ⟶ X} {Y₀ : C₀} {g : Y₀ ⟶ X₀} (self : data.SieveStruct f g) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp self.q (CategoryStruct.comp (data.f self.i₀) h) = CategoryStruct.comp (F.map g) (CategoryStruct.comp f h)

def CategoryTheory.Functor.OneHypercoverDenseData.sieve {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {X : C} (data : F.OneHypercoverDenseData J₀ J X) {X₀ : C₀} (f : F.obj X₀ ⟶ X) : Sieve X₀

Given data : OneHypercoverDenseData F J₀ J X and a morphism f : F.obj X₀ ⟶ X, this is the sieve of X₀ consisting of morphisms g : Y₀ ⟶ X₀ such that there exists i₀ : data.I₀, q : F.obj Y₀ ⟶ F.obj (data.X i₀) such that we have a factorization q ≫ data.f i₀ = F.map g ≫ f.

@[simp]

theorem CategoryTheory.Functor.OneHypercoverDenseData.sieve_apply {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {X : C} (data : F.OneHypercoverDenseData J₀ J X) {X₀ : C₀} (f : F.obj X₀ ⟶ X) (Y₀ : C₀) (g : Y₀ ⟶ X₀) : (data.sieve f).arrows g = Nonempty (data.SieveStruct f g)

theorem CategoryTheory.Functor.OneHypercoverDenseData.sieve_mem {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} [IsDenseSubsite J₀ J F] {X : C} (data : F.OneHypercoverDenseData J₀ J X) {X₀ : C₀} (f : F.obj X₀ ⟶ X) : data.sieve f ∈ J₀ X₀

noncomputable def CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.liftAux {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [IsDenseSubsite J₀ J F] {data : (X : C) → F.OneHypercoverDenseData J₀ J X} {G : Functor Cᵒᵖ A} (hG₀ : Presheaf.IsSheaf J₀ (F.op.comp G)) {X : C} {S : J.Cover X} (s : Limits.Multifork (S.index G)) (i : (data X).I₀) : s.pt ⟶ G.obj (Opposite.op (F.obj ((data X).X i)))

Auxiliary definition for lift.

theorem CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.liftAux_fac {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [IsDenseSubsite J₀ J F] {data : (X : C) → F.OneHypercoverDenseData J₀ J X} {G : Functor Cᵒᵖ A} (hG₀ : Presheaf.IsSheaf J₀ (F.op.comp G)) {X : C} {S : J.Cover X} (s : Limits.Multifork (S.index G)) {i : (data X).I₀} {W₀ : C₀} (a : W₀ ⟶ (data X).X i) (ha : (↑S).arrows (CategoryStruct.comp (F.map a) ((data X).f i))) : CategoryStruct.comp (liftAux hG₀ s i) (G.map (F.map a).op) = s.ι { Y := F.obj W₀, f := CategoryStruct.comp (F.map a) ((data X).f i), hf := ha }

noncomputable def CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.lift {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [IsDenseSubsite J₀ J F] {data : (X : C) → F.OneHypercoverDenseData J₀ J X} {G : Functor Cᵒᵖ A} (hG₀ : Presheaf.IsSheaf J₀ (F.op.comp G)) (hG : (X : C) → Limits.IsLimit ((data X).toOneHypercover.multifork G)) {X : C} {S : J.Cover X} (s : Limits.Multifork (S.index G)) : s.pt ⟶ G.obj (Opposite.op X)

Auxiliary definition for the lemma OneHypercoverDenseData.isSheaf_iff.

theorem CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.lift_map {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [IsDenseSubsite J₀ J F] {data : (X : C) → F.OneHypercoverDenseData J₀ J X} {G : Functor Cᵒᵖ A} (hG₀ : Presheaf.IsSheaf J₀ (F.op.comp G)) (hG : (X : C) → Limits.IsLimit ((data X).toOneHypercover.multifork G)) {X : C} {S : J.Cover X} (s : Limits.Multifork (S.index G)) (i : (data X).I₀) : CategoryStruct.comp (lift hG₀ hG s) (G.map ((data X).f i).op) = liftAux hG₀ s i

theorem CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.lift_map_assoc {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [IsDenseSubsite J₀ J F] {data : (X : C) → F.OneHypercoverDenseData J₀ J X} {G : Functor Cᵒᵖ A} (hG₀ : Presheaf.IsSheaf J₀ (F.op.comp G)) (hG : (X : C) → Limits.IsLimit ((data X).toOneHypercover.multifork G)) {X : C} {S : J.Cover X} (s : Limits.Multifork (S.index G)) (i : (data X).I₀) {Z : A} (h : G.obj (Opposite.op (F.obj ((data X).X i))) ⟶ Z) : CategoryStruct.comp (lift hG₀ hG s) (CategoryStruct.comp (G.map ((data X).f i).op) h) = CategoryStruct.comp (liftAux hG₀ s i) h

theorem CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.fac {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [IsDenseSubsite J₀ J F] {data : (X : C) → F.OneHypercoverDenseData J₀ J X} {G : Functor Cᵒᵖ A} (hG₀ : Presheaf.IsSheaf J₀ (F.op.comp G)) (hG : (X : C) → Limits.IsLimit ((data X).toOneHypercover.multifork G)) {X : C} {S : J.Cover X} (s : Limits.Multifork (S.index G)) (a : S.Arrow) : CategoryStruct.comp (lift hG₀ hG s) (G.map a.f.op) = s.ι a

theorem CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.fac_assoc {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [IsDenseSubsite J₀ J F] {data : (X : C) → F.OneHypercoverDenseData J₀ J X} {G : Functor Cᵒᵖ A} (hG₀ : Presheaf.IsSheaf J₀ (F.op.comp G)) (hG : (X : C) → Limits.IsLimit ((data X).toOneHypercover.multifork G)) {X : C} {S : J.Cover X} (s : Limits.Multifork (S.index G)) (a : S.Arrow) {Z : A} (h : G.obj (Opposite.op a.Y) ⟶ Z) : CategoryStruct.comp (lift hG₀ hG s) (CategoryStruct.comp (G.map a.f.op) h) = CategoryStruct.comp (s.ι a) h

theorem CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.hom_ext {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [IsDenseSubsite J₀ J F] {data : (X : C) → F.OneHypercoverDenseData J₀ J X} {G : Functor Cᵒᵖ A} (hG₀ : Presheaf.IsSheaf J₀ (F.op.comp G)) (hG : (X : C) → Limits.IsLimit ((data X).toOneHypercover.multifork G)) {X : C} {S : J.Cover X} {s : Limits.Multifork (S.index G)} {f₁ f₂ : s.pt ⟶ G.obj (Opposite.op X)} (h : ∀ (a : S.Arrow), CategoryStruct.comp f₁ (G.map a.f.op) = CategoryStruct.comp f₂ (G.map a.f.op)) : f₁ = f₂

noncomputable def CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.isLimit {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [IsDenseSubsite J₀ J F] {data : (X : C) → F.OneHypercoverDenseData J₀ J X} {G : Functor Cᵒᵖ A} (hG₀ : Presheaf.IsSheaf J₀ (F.op.comp G)) (hG : (X : C) → Limits.IsLimit ((data X).toOneHypercover.multifork G)) {X : C} (S : J.Cover X) : Limits.IsLimit (S.multifork G)

Auxiliary definition for the lemma OneHypercoverDenseData.isSheaf_iff.

theorem CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X) (G : Functor Cᵒᵖ A) : Presheaf.IsSheaf J G ↔ Presheaf.IsSheaf J₀ (F.op.comp G) ∧ ∀ (X : C), Nonempty (Limits.IsLimit ((data X).toOneHypercover.multifork G))

Let F : C₀ ⥤ C be a dense subsite, and assume we have a family data : ∀ X, F.OneHypercoverDenseData J₀ J X. This lemma shows that G : Cᵒᵖ ⥤ A is a sheaf iff F.op F.op ⋙ G : C₀ᵒᵖ ⥤ A is a sheaf and for any X : C, the multifork for G and the 1-hypercover given by data X is a limit.

noncomputable def CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] (data : (X : C) → F.OneHypercoverDenseData J₀ J X) [Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : Sheaf J₀ A) (X : C) : A

Given a dense subsite F : C₀ ⥤ C and a family data : ∀ X, OneHypercoverDenseData F J₀ J X and a sheaf G₀ on J₀, this is the value on an object X : C of the "extension" of G₀ as a sheaf on J (see OneHypercoverDenseData.essSurj.presheaf for the construction of this extension as a presheaf): it is defined as a multiequalizer using data X.

noncomputable def CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] (data : (X : C) → F.OneHypercoverDenseData J₀ J X) [Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : Sheaf J₀ A) (X : C) (i : (data X).I₀) : presheafObj data G₀ X ⟶ G₀.val.obj (Opposite.op ((data X).X i))

The projection presheafObj data G₀ X ⟶ G₀.val.obj (op ((data X).X i)).

theorem CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_hom_ext {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] {data : (X : C) → F.OneHypercoverDenseData J₀ J X} [Limits.HasLimitsOfSize.{w, w, v', u'} A] {G₀ : Sheaf J₀ A} {X : C} {Z : A} {f g : Z ⟶ presheafObj data G₀ X} (h : ∀ (i : (data X).I₀), CategoryStruct.comp f (presheafObjπ data G₀ X i) = CategoryStruct.comp g (presheafObjπ data G₀ X i)) : f = g

theorem CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_hom_ext_iff {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] {data : (X : C) → F.OneHypercoverDenseData J₀ J X} [Limits.HasLimitsOfSize.{w, w, v', u'} A] {G₀ : Sheaf J₀ A} {X : C} {Z : A} {f g : Z ⟶ presheafObj data G₀ X} : f = g ↔ ∀ (i : (data X).I₀), CategoryStruct.comp f (presheafObjπ data G₀ X i) = CategoryStruct.comp g (presheafObjπ data G₀ X i)

theorem CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_condition {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] (data : (X : C) → F.OneHypercoverDenseData J₀ J X) [Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : Sheaf J₀ A) (X : C) (i i' : (data X).I₀) (j : (data X).I₁ i i') : CategoryStruct.comp (presheafObjπ data G₀ X i) (G₀.val.map ((data X).p₁ j).op) = CategoryStruct.comp (presheafObjπ data G₀ X i') (G₀.val.map ((data X).p₂ j).op)

theorem CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_condition_assoc {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] (data : (X : C) → F.OneHypercoverDenseData J₀ J X) [Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : Sheaf J₀ A) (X : C) (i i' : (data X).I₀) (j : (data X).I₁ i i') {Z : A} (h : G₀.val.obj (Opposite.op ((data X).Y j)) ⟶ Z) : CategoryStruct.comp (presheafObjπ data G₀ X i) (CategoryStruct.comp (G₀.val.map ((data X).p₁ j).op) h) = CategoryStruct.comp (presheafObjπ data G₀ X i') (CategoryStruct.comp (G₀.val.map ((data X).p₂ j).op) h)

theorem CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj_mapPreimage_condition {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X) [Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : Sheaf J₀ A) (X : C) (i₁ i₂ : (data X).I₀) {Y₀ : C₀} (p₁ : F.obj Y₀ ⟶ F.obj ((data X).X i₁)) (p₂ : F.obj Y₀ ⟶ F.obj ((data X).X i₂)) (fac : CategoryStruct.comp p₁ ((data X).f i₁) = CategoryStruct.comp p₂ ((data X).f i₂)) : CategoryStruct.comp (presheafObjπ data G₀ X i₁) (IsDenseSubsite.mapPreimage J F G₀ p₁) = CategoryStruct.comp (presheafObjπ data G₀ X i₂) (IsDenseSubsite.mapPreimage J F G₀ p₂)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjMultifork {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] (data : (X : C) → F.OneHypercoverDenseData J₀ J X) [Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : Sheaf J₀ A) (X : C) : Limits.Multifork ((data X).multicospanIndex G₀.val)

The (limit) multifork with point presheafObjπ data G₀ X for the diagram given by G₀ and data X.

noncomputable def CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjIsLimit {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] (data : (X : C) → F.OneHypercoverDenseData J₀ J X) [Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : Sheaf J₀ A) (X : C) : Limits.IsLimit (presheafObjMultifork data G₀ X)

The multifork presheafObjMultifork is a limit.

noncomputable def CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction.res {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X) [Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : Sheaf J₀ A) {X : C} {X₀ Y₀ : C₀} {f : F.obj X₀ ⟶ X} {g : Y₀ ⟶ X₀} (h : (data X).SieveStruct f g) : presheafObj data G₀ X ⟶ G₀.val.obj (Opposite.op Y₀)

Auxiliary definition for OneHypercoverDenseData.essSurj.restriction.

theorem CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction.res_eq_res {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X) [Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : Sheaf J₀ A) {X : C} {X₀ Y₀ : C₀} {f : F.obj X₀ ⟶ X} {g : Y₀ ⟶ X₀} (h₁ h₂ : (data X).SieveStruct f g) : res data G₀ h₁ = res data G₀ h₂

noncomputable def CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X) [Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : Sheaf J₀ A) {X : C} {X₀ : C₀} (f : F.obj X₀ ⟶ X) : presheafObj data G₀ X ⟶ G₀.val.obj (Opposite.op X₀)

Let F : C₀ ⥤ C be a dense subsite and data : ∀ X, F.OneHypercoverDenseData J₀ J X be a family. Let G₀ be a sheaf on C₀. Let f : F.obj X₀ ⟶ X. This is the canonical morphism presheafObj data G₀ X ⟶ G₀.val.obj (op X₀) (where presheafObj data G₀ X is the value on X of the extension to C of the sheaf G₀, see OneHypercoverDenseData.essSurj.presheaf and OneHypercoverDenseData.essSurj.isSheaf).

theorem CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction_map {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X) [Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : Sheaf J₀ A) {X : C} {X₀ : C₀} (f : F.obj X₀ ⟶ X) {Y₀ : C₀} (g : Y₀ ⟶ X₀) {i : (data X).I₀} (p : F.obj Y₀ ⟶ F.obj ((data X).X i)) (fac : CategoryStruct.comp p ((data X).f i) = CategoryStruct.comp (F.map g) f) : CategoryStruct.comp (restriction data G₀ f) (G₀.val.map g.op) = CategoryStruct.comp (presheafObjπ data G₀ X i) (IsDenseSubsite.mapPreimage J F G₀ p)

theorem CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction_eq_of_fac {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X) [Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : Sheaf J₀ A) {X : C} {X₀ : C₀} (f : F.obj X₀ ⟶ X) {i : (data X).I₀} (p : F.obj X₀ ⟶ F.obj ((data X).X i)) (fac : CategoryStruct.comp p ((data X).f i) = f) : restriction data G₀ f = CategoryStruct.comp (presheafObjπ data G₀ X i) (IsDenseSubsite.mapPreimage J F G₀ p)

noncomputable def CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X) [Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : Sheaf J₀ A) {X Y : C} (f : X ⟶ Y) : presheafObj data G₀ Y ⟶ presheafObj data G₀ X

Auxiliary definition for OneHypercoverDenseData.essSurj.presheaf.

@[simp]

theorem CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_π {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X) [Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : Sheaf J₀ A) {X Y : C} (f : X ⟶ Y) (i : (data X).I₀) : CategoryStruct.comp (presheafMap data G₀ f) (presheafObjπ data G₀ X i) = restriction data G₀ (CategoryStruct.comp ((data X).f i) f)

@[simp]

theorem CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_π_assoc {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X) [Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : Sheaf J₀ A) {X Y : C} (f : X ⟶ Y) (i : (data X).I₀) {Z : A} (h : G₀.val.obj (Opposite.op ((data X).X i)) ⟶ Z) : CategoryStruct.comp (presheafMap data G₀ f) (CategoryStruct.comp (presheafObjπ data G₀ X i) h) = CategoryStruct.comp (restriction data G₀ (CategoryStruct.comp ((data X).f i) f)) h

@[simp]

theorem CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_restriction {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X) [Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : Sheaf J₀ A) {X Y : C} {X₀ : C₀} (f : F.obj X₀ ⟶ X) (g : X ⟶ Y) : CategoryStruct.comp (presheafMap data G₀ g) (restriction data G₀ f) = restriction data G₀ (CategoryStruct.comp f g)

@[simp]

theorem CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_restriction_assoc {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X) [Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : Sheaf J₀ A) {X Y : C} {X₀ : C₀} (f : F.obj X₀ ⟶ X) (g : X ⟶ Y) {Z : A} (h : G₀.val.obj (Opposite.op X₀) ⟶ Z) : CategoryStruct.comp (presheafMap data G₀ g) (CategoryStruct.comp (restriction data G₀ f) h) = CategoryStruct.comp (restriction data G₀ (CategoryStruct.comp f g)) h

theorem CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_id {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X) [Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : Sheaf J₀ A) (X : C) : presheafMap data G₀ (CategoryStruct.id X) = CategoryStruct.id (presheafObj data G₀ X)

theorem CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_comp {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X) [Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : Sheaf J₀ A) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : presheafMap data G₀ (CategoryStruct.comp f g) = CategoryStruct.comp (presheafMap data G₀ g) (presheafMap data G₀ f)

theorem CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafMap_comp_assoc {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X) [Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : Sheaf J₀ A) {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : A} (h : presheafObj data G₀ X ⟶ Z✝) : CategoryStruct.comp (presheafMap data G₀ (CategoryStruct.comp f g)) h = CategoryStruct.comp (presheafMap data G₀ g) (CategoryStruct.comp (presheafMap data G₀ f) h)

noncomputable def CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheaf {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X) [Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : Sheaf J₀ A) : Functor Cᵒᵖ A

Let F : C₀ ⥤ C be a dense subsite and data : ∀ X, F.OneHypercoverDenseData J₀ J X be a family. Let G₀ be a sheaf on C₀. This is a presheaf on C which extends G₀, and we shall also show that it is a sheaf (TODO).

@[simp]

theorem CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheaf_map {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X) [Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : Sheaf J₀ A) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) : (presheaf data G₀).map f = presheafMap data G₀ f.unop

@[simp]

theorem CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheaf_obj {C₀ : Type u₀} {C : Type u} [Category.{v₀, u₀} C₀] [Category.{v, u} C] {F : Functor C₀ C} {J₀ : GrothendieckTopology C₀} {J : GrothendieckTopology C} {A : Type u'} [Category.{v', u'} A] [IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X) [Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : Sheaf J₀ A) (X : Cᵒᵖ) : (presheaf data G₀).obj X = presheafObj data G₀ (Opposite.unop X)