1-hypercovers

Given a Grothendieck topology J on a category C, we define the type of 1-hypercovers of an object S : C. They consists of a covering family of morphisms X i ⟶ S indexed by a type I₀ and, for each tuple (i₁, i₂) of elements of I₀, a "covering Y j of the fibre product of X i₁ and X i₂ over S", a condition which is phrased here without assuming that the fibre product actually exist.

The definition OneHypercover.isLimitMultifork shows that if E is a 1-hypercover of S, and F is a sheaf, then F.obj (op S) identifies to the multiequalizer of suitable maps F.obj (op (E.X i)) ⟶ F.obj (op (E.Y j)).

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

The categorical data that is involved in a 1-hypercover of an object S. This consists of a family of morphisms f i : X i ⟶ S for i : I₀, and for each tuple (i₁, i₂) of elements in I₀, a family of objects Y j indexed by a type I₁ i₁ i₂, which are equipped with a map to the fibre product of X i₁ and X i₂, which is phrased here as the data of the two projections p₁ : Y j ⟶ X i₁, p₂ : Y j ⟶ X i₂ and the relation p₁ j ≫ f i₁ = p₂ j ≫ f i₂. (See GrothendieckTopology.OneHypercover for the topological conditions.)

• 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₀) : 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 (self.p₁ j) (self.f i₁) = CategoryStruct.comp (self.p₂ j) (self.f i₂)

@[reducible, inline]

abbrev CategoryTheory.PreOneHypercover.HasPullbacks {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) : Prop

The assumption that the pullback of X i₁ and X i₂ over S exists for any i₁ and i₂.

Equations

• E.HasPullbacks = ∀ (i₁ i₂ : E.I₀), CategoryTheory.Limits.HasPullback (E.f i₁) (E.f i₂)

@[reducible, inline]

abbrev CategoryTheory.PreOneHypercover.sieve₀ {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) : Sieve S

The sieve of S that is generated by the morphisms f i : X i ⟶ S.

Equations

• E.sieve₀ = CategoryTheory.Sieve.ofArrows E.X E.f

def CategoryTheory.PreOneHypercover.sieve₁ {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) {i₁ i₂ : E.I₀} {W : C} (p₁ : W ⟶ E.X i₁) (p₂ : W ⟶ E.X i₂) : Sieve W

Given an object W equipped with morphisms p₁ : W ⟶ E.X i₁, p₂ : W ⟶ E.X i₂, this is the sieve of W which consists of morphisms g : Z ⟶ W such that there exists j and h : Z ⟶ E.Y j such that g ≫ p₁ = h ≫ E.p₁ j and g ≫ p₂ = h ≫ E.p₂ j. See lemmas sieve₁_eq_pullback_sieve₁' and sieve₁'_eq_sieve₁ for equational lemmas regarding this sieve.

Equations

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

@[simp]

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.PreOneHypercover.toPullback {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) {i₁ i₂ : E.I₀} (j : E.I₁ i₁ i₂) [Limits.HasPullback (E.f i₁) (E.f i₂)] : E.Y j ⟶ Limits.pullback (E.f i₁) (E.f i₂)

The obvious morphism E.Y j ⟶ pullback (E.f i₁) (E.f i₂) given by E : PreOneHypercover S.

Equations

• E.toPullback j = CategoryTheory.Limits.pullback.lift (E.p₁ j) (E.p₂ j) ⋯

noncomputable def CategoryTheory.PreOneHypercover.sieve₁' {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (i₁ i₂ : E.I₀) [Limits.HasPullback (E.f i₁) (E.f i₂)] : Sieve (Limits.pullback (E.f i₁) (E.f i₂))

The sieve of pullback (E.f i₁) (E.f i₂) given by E : PreOneHypercover S.

Equations

• E.sieve₁' i₁ i₂ = CategoryTheory.Sieve.ofArrows E.Y fun (j : E.I₁ i₁ i₂) => E.toPullback j

theorem CategoryTheory.PreOneHypercover.sieve₁_eq_pullback_sieve₁' {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) {i₁ i₂ : E.I₀} [Limits.HasPullback (E.f i₁) (E.f i₂)] {W : C} (p₁ : W ⟶ E.X i₁) (p₂ : W ⟶ E.X i₂) (w : CategoryStruct.comp p₁ (E.f i₁) = CategoryStruct.comp p₂ (E.f i₂)) : E.sieve₁ p₁ p₂ = Sieve.pullback (Limits.pullback.lift p₁ p₂ w) (E.sieve₁' i₁ i₂)

theorem CategoryTheory.PreOneHypercover.sieve₁'_eq_sieve₁ {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (i₁ i₂ : E.I₀) [Limits.HasPullback (E.f i₁) (E.f i₂)] : E.sieve₁' i₁ i₂ = E.sieve₁ (Limits.pullback.fst (E.f i₁) (E.f i₂)) (Limits.pullback.snd (E.f i₁) (E.f i₂))

@[reducible, inline]

abbrev CategoryTheory.PreOneHypercover.I₁' {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) : Type w

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

Equations

• E.I₁' = ((i : E.I₀ × E.I₀) × E.I₁ i.1 i.2)

def CategoryTheory.PreOneHypercover.multicospanShape {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) : Limits.MulticospanShape

The shape of the multiforks attached to E : PreOneHypercover S.

Equations

• E.multicospanShape = { L := E.I₀, R := E.I₁', fst := fun (j : E.I₁') => j.fst.1, snd := fun (j : E.I₁') => j.fst.2 }

@[simp]

theorem CategoryTheory.PreOneHypercover.multicospanShape_R {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) : E.multicospanShape.R = E.I₁'

@[simp]

theorem CategoryTheory.PreOneHypercover.multicospanShape_snd {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (j : E.I₁') : E.multicospanShape.snd j = j.fst.2

@[simp]

theorem CategoryTheory.PreOneHypercover.multicospanShape_L {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) : E.multicospanShape.L = E.I₀

@[simp]

theorem CategoryTheory.PreOneHypercover.multicospanShape_fst {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (j : E.I₁') : E.multicospanShape.fst j = j.fst.1

def CategoryTheory.PreOneHypercover.multicospanIndex {C : Type u} [Category.{v, u} C] {A : Type u_1} [Category.{u_2, u_1} A] {S : C} (E : PreOneHypercover S) (F : Functor Cᵒᵖ A) : Limits.MulticospanIndex E.multicospanShape A

The diagram of the multifork attached to a presheaf F : Cᵒᵖ ⥤ A, S : C and E : PreOneHypercover S.

Equations

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

@[simp]

theorem CategoryTheory.PreOneHypercover.multicospanIndex_fst {C : Type u} [Category.{v, u} C] {A : Type u_1} [Category.{u_2, u_1} A] {S : C} (E : PreOneHypercover S) (F : Functor Cᵒᵖ A) (j : E.multicospanShape.R) : (E.multicospanIndex F).fst j = F.map (E.p₁ j.snd).op

@[simp]

theorem CategoryTheory.PreOneHypercover.multicospanIndex_right {C : Type u} [Category.{v, u} C] {A : Type u_1} [Category.{u_2, u_1} A] {S : C} (E : PreOneHypercover S) (F : Functor Cᵒᵖ A) (j : E.multicospanShape.R) : (E.multicospanIndex F).right j = F.obj (Opposite.op (E.Y j.snd))

@[simp]

theorem CategoryTheory.PreOneHypercover.multicospanIndex_left {C : Type u} [Category.{v, u} C] {A : Type u_1} [Category.{u_2, u_1} A] {S : C} (E : PreOneHypercover S) (F : Functor Cᵒᵖ A) (i : E.multicospanShape.L) : (E.multicospanIndex F).left i = F.obj (Opposite.op (E.X i))

@[simp]

theorem CategoryTheory.PreOneHypercover.multicospanIndex_snd {C : Type u} [Category.{v, u} C] {A : Type u_1} [Category.{u_2, u_1} A] {S : C} (E : PreOneHypercover S) (F : Functor Cᵒᵖ A) (j : E.multicospanShape.R) : (E.multicospanIndex F).snd j = F.map (E.p₂ j.snd).op

def CategoryTheory.PreOneHypercover.multifork {C : Type u} [Category.{v, u} C] {A : Type u_1} [Category.{u_2, u_1} A] {S : C} (E : PreOneHypercover S) (F : Functor Cᵒᵖ A) : Limits.Multifork (E.multicospanIndex F)

The multifork attached to a presheaf F : Cᵒᵖ ⥤ A, S : C and E : PreOneHypercover S.

Equations

• E.multifork F = CategoryTheory.Limits.Multifork.ofι (E.multicospanIndex F) (F.obj (Opposite.op S)) (fun (i₀ : E.multicospanShape.L) => F.map (E.f i₀).op) ⋯

structure CategoryTheory.PreOneHypercover.Hom {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (F : PreOneHypercover S) : Type (max (max u_2 u_3) v)

A morphism of pre-1-hypercovers of S is a family of refinement morphisms commuting with the structure morphisms of E and F.

• s₀ (i : E.I₀) : F.I₀

  The map between indexing types of the coverings of S

• s₁ {i j : E.I₀} (k : E.I₁ i j) : F.I₁ (self.s₀ i) (self.s₀ j)

  The map between indexing types of the coverings of the fibre products over S.

• h₀ (i : E.I₀) : E.X i ⟶ F.X (self.s₀ i)

  The refinement morphisms between objects in the coverings of S.

• h₁ {i j : E.I₀} (k : E.I₁ i j) : E.Y k ⟶ F.Y (self.s₁ k)

  The refinement morphisms between objects in the coverings of the fibre products over S.

• w₀ (i : E.I₀) : CategoryStruct.comp (self.h₀ i) (F.f (self.s₀ i)) = E.f i
• w₁₁ {i j : E.I₀} (k : E.I₁ i j) : CategoryStruct.comp (self.h₁ k) (F.p₁ (self.s₁ k)) = CategoryStruct.comp (E.p₁ k) (self.h₀ i)
• w₁₂ {i j : E.I₀} (k : E.I₁ i j) : CategoryStruct.comp (self.h₁ k) (F.p₂ (self.s₁ k)) = CategoryStruct.comp (E.p₂ k) (self.h₀ j)

theorem CategoryTheory.PreOneHypercover.Hom.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} {x y : E.Hom F} : x = y ↔ x.s₀ = y.s₀ ∧ @s₁ C inst✝ S E F x ≍ @s₁ C inst✝ S E F y ∧ x.h₀ ≍ y.h₀ ∧ @h₁ C inst✝ S E F x ≍ @h₁ C inst✝ S E F y

theorem CategoryTheory.PreOneHypercover.Hom.ext {C : Type u} {inst✝ : Category.{v, u} C} {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} {x y : E.Hom F} (s₀ : x.s₀ = y.s₀) (s₁ : @s₁ C inst✝ S E F x ≍ @s₁ C inst✝ S E F y) (h₀ : x.h₀ ≍ y.h₀) (h₁ : @h₁ C inst✝ S E F x ≍ @h₁ C inst✝ S E F y) : x = y

@[simp]

theorem CategoryTheory.PreOneHypercover.Hom.w₀_assoc {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} (self : E.Hom F) (i : E.I₀) {Z : C} (h : S ⟶ Z) : CategoryStruct.comp (self.h₀ i) (CategoryStruct.comp (F.f (self.s₀ i)) h) = CategoryStruct.comp (E.f i) h

theorem CategoryTheory.PreOneHypercover.Hom.w₁₂_assoc {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} (self : E.Hom F) {i j : E.I₀} (k : E.I₁ i j) {Z : C} (h : F.X (self.s₀ j) ⟶ Z) : CategoryStruct.comp (self.h₁ k) (CategoryStruct.comp (F.p₂ (self.s₁ k)) h) = CategoryStruct.comp (E.p₂ k) (CategoryStruct.comp (self.h₀ j) h)

theorem CategoryTheory.PreOneHypercover.Hom.w₁₁_assoc {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} (self : E.Hom F) {i j : E.I₀} (k : E.I₁ i j) {Z : C} (h : F.X (self.s₀ i) ⟶ Z) : CategoryStruct.comp (self.h₁ k) (CategoryStruct.comp (F.p₁ (self.s₁ k)) h) = CategoryStruct.comp (E.p₁ k) (CategoryStruct.comp (self.h₀ i) h)

def CategoryTheory.PreOneHypercover.Hom.id {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) : E.Hom E

The identity refinement of a pre-1-hypercover.

Equations

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

@[simp]

theorem CategoryTheory.PreOneHypercover.Hom.id_h₁ {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) {i✝ j✝ : E.I₀} (x✝ : E.I₁ i✝ j✝) : (id E).h₁ x✝ = CategoryStruct.id (E.Y x✝)

@[simp]

theorem CategoryTheory.PreOneHypercover.Hom.id_s₁ {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) {i✝ j✝ : E.I₀} (a : E.I₁ i✝ j✝) : (id E).s₁ a = _root_.id a

@[simp]

theorem CategoryTheory.PreOneHypercover.Hom.id_s₀ {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (a : E.I₀) : (id E).s₀ a = _root_.id a

@[simp]

theorem CategoryTheory.PreOneHypercover.Hom.id_h₀ {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (x✝ : E.I₀) : (id E).h₀ x✝ = CategoryStruct.id (E.X x✝)

def CategoryTheory.PreOneHypercover.Hom.comp {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} {G : PreOneHypercover S} (f : E.Hom F) (g : F.Hom G) : E.Hom G

Composition of refinement morphisms of pre-1-hypercovers.

Equations

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

@[simp]

theorem CategoryTheory.PreOneHypercover.Hom.comp_h₁ {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} {G : PreOneHypercover S} (f : E.Hom F) (g : F.Hom G) {i✝ j✝ : E.I₀} (i : E.I₁ i✝ j✝) : (f.comp g).h₁ i = CategoryStruct.comp (f.h₁ i) (g.h₁ (f.s₁ i))

@[simp]

theorem CategoryTheory.PreOneHypercover.Hom.comp_h₀ {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} {G : PreOneHypercover S} (f : E.Hom F) (g : F.Hom G) (i : E.I₀) : (f.comp g).h₀ i = CategoryStruct.comp (f.h₀ i) (g.h₀ (f.s₀ i))

@[simp]

theorem CategoryTheory.PreOneHypercover.Hom.comp_s₁ {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} {G : PreOneHypercover S} (f : E.Hom F) (g : F.Hom G) {i✝ j✝ : E.I₀} (a✝ : E.I₁ i✝ j✝) : (f.comp g).s₁ a✝ = (g.s₁ ∘ f.s₁) a✝

@[simp]

theorem CategoryTheory.PreOneHypercover.Hom.comp_s₀ {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} {G : PreOneHypercover S} (f : E.Hom F) (g : F.Hom G) (a✝ : E.I₀) : (f.comp g).s₀ a✝ = (g.s₀ ∘ f.s₀) a✝

def CategoryTheory.PreOneHypercover.Hom.s₁' {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} (f : E.Hom F) (k : E.I₁') : F.I₁'

The induced index map E.I₁' → F.I₁' from a refinement morphism E ⟶ F.

Equations

• f.s₁' k = ⟨(f.s₀ k.fst.1, f.s₀ k.fst.2), f.s₁ k.snd⟩

instance CategoryTheory.PreOneHypercover.instCategory {C : Type u} [Category.{v, u} C] {S : C} : Category.{max v u_2, max (max u v) (u_2 + 1)} (PreOneHypercover S)

Equations

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

@[simp]

theorem CategoryTheory.PreOneHypercover.id_s₁ {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) {i✝ j✝ : E.I₀} (a : E.I₁ i✝ j✝) : (CategoryStruct.id E).s₁ a = a

@[simp]

theorem CategoryTheory.PreOneHypercover.id_h₀ {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (x✝ : E.I₀) : (CategoryStruct.id E).h₀ x✝ = CategoryStruct.id (E.X x✝)

@[simp]

theorem CategoryTheory.PreOneHypercover.id_s₀ {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (a : E.I₀) : (CategoryStruct.id E).s₀ a = a

@[simp]

theorem CategoryTheory.PreOneHypercover.comp_h₁ {C : Type u} [Category.{v, u} C] {S : C} {X✝ Y✝ Z✝ : PreOneHypercover S} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) {i✝ j✝ : X✝.I₀} (i : X✝.I₁ i✝ j✝) : (CategoryStruct.comp f g).h₁ i = CategoryStruct.comp (f.h₁ i) (g.h₁ (f.s₁ i))

@[simp]

theorem CategoryTheory.PreOneHypercover.id_h₁ {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) {i✝ j✝ : E.I₀} (x✝ : E.I₁ i✝ j✝) : (CategoryStruct.id E).h₁ x✝ = CategoryStruct.id (E.Y x✝)

@[simp]

theorem CategoryTheory.PreOneHypercover.comp_s₁ {C : Type u} [Category.{v, u} C] {S : C} {X✝ Y✝ Z✝ : PreOneHypercover S} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) {i✝ j✝ : X✝.I₀} (a✝ : X✝.I₁ i✝ j✝) : (CategoryStruct.comp f g).s₁ a✝ = g.s₁ (f.s₁ a✝)

@[simp]

theorem CategoryTheory.PreOneHypercover.comp_s₀ {C : Type u} [Category.{v, u} C] {S : C} {X✝ Y✝ Z✝ : PreOneHypercover S} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) (a✝ : X✝.I₀) : (CategoryStruct.comp f g).s₀ a✝ = g.s₀ (f.s₀ a✝)

@[simp]

theorem CategoryTheory.PreOneHypercover.comp_h₀ {C : Type u} [Category.{v, u} C] {S : C} {X✝ Y✝ Z✝ : PreOneHypercover S} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) (i : X✝.I₀) : (CategoryStruct.comp f g).h₀ i = CategoryStruct.comp (f.h₀ i) (g.h₀ (f.s₀ i))

structure CategoryTheory.PreOneHypercover.Homotopy {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} (f g : E.Hom F) : Type (max (max v w) w')

A homotopy of refinements E ⟶ F is a family of morphisms Xᵢ ⟶ Yₐ where Yₐ is a component of the cover of X_{f(i)} ×[S] X_{g(i)}.

• H (i : E.I₀) : F.I₁ (f.s₀ i) (g.s₀ i)

  The index map sending i : E.I₀ to a above (f(i), g(i)).

• a (i : E.I₀) : E.X i ⟶ F.Y (self.H i)

  The morphism Xᵢ ⟶ Yₐ.

• wl (i : E.I₀) : CategoryStruct.comp (self.a i) (F.p₁ (self.H i)) = f.h₀ i
• wr (i : E.I₀) : CategoryStruct.comp (self.a i) (F.p₂ (self.H i)) = g.h₀ i

@[simp]

theorem CategoryTheory.PreOneHypercover.Homotopy.wr_assoc {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} {f g : E.Hom F} (self : Homotopy f g) (i : E.I₀) {Z : C} (h : F.X (g.s₀ i) ⟶ Z) : CategoryStruct.comp (self.a i) (CategoryStruct.comp (F.p₂ (self.H i)) h) = CategoryStruct.comp (g.h₀ i) h

@[simp]

theorem CategoryTheory.PreOneHypercover.Homotopy.wl_assoc {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} {f g : E.Hom F} (self : Homotopy f g) (i : E.I₀) {Z : C} (h : F.X (f.s₀ i) ⟶ Z) : CategoryStruct.comp (self.a i) (CategoryStruct.comp (F.p₁ (self.H i)) h) = CategoryStruct.comp (f.h₀ i) h

def CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit {C : Type u} [Category.{v, u} C] {A : Type u_1} [Category.{u_2, u_1} A] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} (f : E.Hom F) (P : Functor Cᵒᵖ A) {c : Limits.Multifork (E.multicospanIndex P)} (hc : Limits.IsLimit c) (d : Limits.Multifork (F.multicospanIndex P)) : d.pt ⟶ c.pt

A refinement morphism E ⟶ F induces a morphism on associated multiequalizers.

Equations

• f.mapMultiforkOfIsLimit P hc d = CategoryTheory.Limits.Multifork.IsLimit.lift hc (fun (a : E.multicospanShape.L) => CategoryTheory.CategoryStruct.comp (d.ι (f.s₀ a)) (P.map (f.h₀ a).op)) ⋯

@[simp]

theorem CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit_ι {C : Type u} [Category.{v, u} C] {A : Type u_1} [Category.{u_2, u_1} A] {S : C} {E F : PreOneHypercover S} (f : E.Hom F) (P : Functor Cᵒᵖ A) {c : Limits.Multifork (E.multicospanIndex P)} (hc : Limits.IsLimit c) (d : Limits.Multifork (F.multicospanIndex P)) (a : E.I₀) : CategoryStruct.comp (f.mapMultiforkOfIsLimit P hc d) (c.ι a) = CategoryStruct.comp (d.ι (f.s₀ a)) (P.map (f.h₀ a).op)

@[simp]

theorem CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit_ι_assoc {C : Type u} [Category.{v, u} C] {A : Type u_1} [Category.{u_2, u_1} A] {S : C} {E F : PreOneHypercover S} (f : E.Hom F) (P : Functor Cᵒᵖ A) {c : Limits.Multifork (E.multicospanIndex P)} (hc : Limits.IsLimit c) (d : Limits.Multifork (F.multicospanIndex P)) (a : E.I₀) {Z : A} (h : (E.multicospanIndex P).left a ⟶ Z) : CategoryStruct.comp (f.mapMultiforkOfIsLimit P hc d) (CategoryStruct.comp (c.ι a) h) = CategoryStruct.comp (d.ι (f.s₀ a)) (CategoryStruct.comp (P.map (f.h₀ a).op) h)

theorem CategoryTheory.PreOneHypercover.Homotopy.mapMultiforkOfIsLimit_eq {C : Type u} [Category.{v, u} C] {A : Type u_1} [Category.{u_2, u_1} A] {S : C} {E F : PreOneHypercover S} {f g : E.Hom F} (H : Homotopy f g) (P : Functor Cᵒᵖ A) {c : Limits.Multifork (E.multicospanIndex P)} (hc : Limits.IsLimit c) (d : Limits.Multifork (F.multicospanIndex P)) : f.mapMultiforkOfIsLimit P hc d = g.mapMultiforkOfIsLimit P hc d

Homotopic refinements induce the same map on multiequalizers.

@[reducible, inline]

noncomputable abbrev CategoryTheory.PreOneHypercover.cylinderX {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) {i : E.I₀} (k : F.I₁ (f.s₀ i) (g.s₀ i)) : C

(Implementation): The covering object of cylinder f g.

Equations

• CategoryTheory.PreOneHypercover.cylinderX f g k = CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.lift (f.h₀ i) (g.h₀ i) ⋯) (F.toPullback k)

@[reducible, inline]

noncomputable abbrev CategoryTheory.PreOneHypercover.cylinderf {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) {i : E.I₀} (k : F.I₁ (f.s₀ i) (g.s₀ i)) : cylinderX f g k ⟶ S

(Implementation): The structure morphisms of the covering objects of cylinder f g.

Equations

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

noncomputable def CategoryTheory.PreOneHypercover.cylinder {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) : PreOneHypercover S

Given two refinement morphisms f, g : E ⟶ F, this is a (pre-)1-hypercover W that admits a morphism h : W ⟶ E such that h ≫ f and h ≫ g are homotopic. Hence they become equal after quotienting out by homotopy. This is a 1-hypercover, if E and F are (see OneHpyercover.cylinder).

Equations

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

@[simp]

theorem CategoryTheory.PreOneHypercover.cylinder_p₁ {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) {p q : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)} (k : ULift.{max w w', w} (E.I₁ p.fst q.fst)) : (cylinder f g).p₁ k = CategoryStruct.comp (Limits.pullback.fst (Limits.pullback.map (cylinderf f g p.snd) (cylinderf f g q.snd) (E.f p.fst) (E.f q.fst) (Limits.pullback.fst (Limits.pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd)) (Limits.pullback.fst (Limits.pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)) (CategoryStruct.id S) ⋯ ⋯) (Limits.pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯)) (Limits.pullback.fst (cylinderf f g p.snd) (cylinderf f g q.snd))

@[simp]

theorem CategoryTheory.PreOneHypercover.cylinder_I₁ {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) (p q : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)) : (cylinder f g).I₁ p q = ULift.{max w w', w} (E.I₁ p.fst q.fst)

@[simp]

theorem CategoryTheory.PreOneHypercover.cylinder_Y {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) {p q : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)} (k : ULift.{max w w', w} (E.I₁ p.fst q.fst)) : (cylinder f g).Y k = Limits.pullback (Limits.pullback.map (cylinderf f g p.snd) (cylinderf f g q.snd) (E.f p.fst) (E.f q.fst) (Limits.pullback.fst (Limits.pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd)) (Limits.pullback.fst (Limits.pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)) (CategoryStruct.id S) ⋯ ⋯) (Limits.pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯)

@[simp]

theorem CategoryTheory.PreOneHypercover.cylinder_p₂ {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) {p q : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)} (k : ULift.{max w w', w} (E.I₁ p.fst q.fst)) : (cylinder f g).p₂ k = CategoryStruct.comp (Limits.pullback.fst (Limits.pullback.map (cylinderf f g p.snd) (cylinderf f g q.snd) (E.f p.fst) (E.f q.fst) (Limits.pullback.fst (Limits.pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd)) (Limits.pullback.fst (Limits.pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)) (CategoryStruct.id S) ⋯ ⋯) (Limits.pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯)) (Limits.pullback.snd (cylinderf f g p.snd) (cylinderf f g q.snd))

@[simp]

theorem CategoryTheory.PreOneHypercover.cylinder_f {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) (p : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)) : (cylinder f g).f p = cylinderf f g p.snd

@[simp]

theorem CategoryTheory.PreOneHypercover.cylinder_I₀ {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) : (cylinder f g).I₀ = ((i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i))

@[simp]

theorem CategoryTheory.PreOneHypercover.cylinder_X {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) (p : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)) : (cylinder f g).X p = cylinderX f g p.snd

theorem CategoryTheory.PreOneHypercover.toPullback_cylinder {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) {i j : (cylinder f g).I₀} (k : (cylinder f g).I₁ i j) : (cylinder f g).toPullback k = Limits.pullback.fst (Limits.pullback.map (cylinderf f g i.snd) (cylinderf f g j.snd) (E.f i.fst) (E.f j.fst) (Limits.pullback.fst (Limits.pullback.lift (f.h₀ i.fst) (g.h₀ i.fst) ⋯) (F.toPullback i.snd)) (Limits.pullback.fst (Limits.pullback.lift (f.h₀ j.fst) (g.h₀ j.fst) ⋯) (F.toPullback j.snd)) (CategoryStruct.id S) ⋯ ⋯) (Limits.pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯)

theorem CategoryTheory.PreOneHypercover.sieve₀_cylinder {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) : (cylinder f g).sieve₀ = Sieve.generate (Presieve.bindOfArrows E.X E.f fun (i : E.I₀) => (Sieve.pullback (Limits.pullback.lift (f.h₀ i) (g.h₀ i) ⋯) (F.sieve₁' (f.s₀ i) (g.s₀ i))).arrows)

theorem CategoryTheory.PreOneHypercover.sieve₁'_cylinder {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) (i j : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)) : (cylinder f g).sieve₁' i j = Sieve.pullback (Limits.pullback.map ((cylinder f g).f i) ((cylinder f g).f j) (E.f i.fst) (E.f j.fst) (Limits.pullback.fst (Limits.pullback.lift (f.h₀ i.fst) (g.h₀ i.fst) ⋯) (F.toPullback i.snd)) (Limits.pullback.fst (Limits.pullback.lift (f.h₀ j.fst) (g.h₀ j.fst) ⋯) (F.toPullback j.snd)) (CategoryStruct.id S) ⋯ ⋯) (E.sieve₁' i.fst j.fst)

noncomputable def CategoryTheory.PreOneHypercover.cylinderHom {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) : (cylinder f g).Hom E

(Implementation): The refinement morphism cylinder f g ⟶ E.

Equations

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

@[simp]

theorem CategoryTheory.PreOneHypercover.cylinderHom_s₀ {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) (p : (cylinder f g).I₀) : (cylinderHom f g).s₀ p = p.fst

@[simp]

theorem CategoryTheory.PreOneHypercover.cylinderHom_s₁ {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) {i✝ j✝ : (cylinder f g).I₀} (k : (cylinder f g).I₁ i✝ j✝) : (cylinderHom f g).s₁ k = k.down

@[simp]

theorem CategoryTheory.PreOneHypercover.cylinderHom_h₀ {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) (p : (cylinder f g).I₀) : (cylinderHom f g).h₀ p = Limits.pullback.fst (Limits.pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd)

@[simp]

theorem CategoryTheory.PreOneHypercover.cylinderHom_h₁ {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) {p q : (cylinder f g).I₀} (k : (cylinder f g).I₁ p q) : (cylinderHom f g).h₁ k = Limits.pullback.snd (Limits.pullback.map (cylinderf f g p.snd) (cylinderf f g q.snd) (E.f p.fst) (E.f q.fst) (Limits.pullback.fst (Limits.pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd)) (Limits.pullback.fst (Limits.pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)) (CategoryStruct.id S) ⋯ ⋯) (Limits.pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯)

noncomputable def CategoryTheory.PreOneHypercover.cylinderHomotopy {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) : Homotopy ((cylinderHom f g).comp f) ((cylinderHom f g).comp g)

(Implementation): The homotopy of the morphisms cylinder f g ⟶ E ⟶ F.

Equations

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

theorem CategoryTheory.PreOneHypercover.exists_nonempty_homotopy {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) : ∃ (W : PreOneHypercover S) (h : W.Hom E), Nonempty (Homotopy (h.comp f) (h.comp g))

Up to homotopy, the category of (pre-)1-hypercovers is cofiltered.

structure CategoryTheory.GrothendieckTopology.OneHypercover {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (S : C) extends CategoryTheory.PreOneHypercover S : Type (max (max u v) (w + 1))

The type of 1-hypercovers of an object S : C in a category equipped with a Grothendieck topology J. This can be constructed from a covering of S and a covering of the fibre products of the objects in this covering (see OneHypercover.mk').

• I₀ : Type w
• X (i : self.I₀) : C
• f (i : self.I₀) : 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 (self.p₁ j) (self.f i₁) = CategoryStruct.comp (self.p₂ j) (self.f i₂)
• mem₀ : self.sieve₀ ∈ J S
• mem₁ (i₁ i₂ : self.I₀) ⦃W : C⦄ (p₁ : W ⟶ self.X i₁) (p₂ : W ⟶ self.X i₂) (w : CategoryStruct.comp p₁ (self.f i₁) = CategoryStruct.comp p₂ (self.f i₂)) : self.sieve₁ p₁ p₂ ∈ J W

theorem CategoryTheory.GrothendieckTopology.OneHypercover.mem_sieve₁' {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} (E : J.OneHypercover S) (i₁ i₂ : E.I₀) [Limits.HasPullback (E.f i₁) (E.f i₂)] : E.sieve₁' i₁ i₂ ∈ J (Limits.pullback (E.f i₁) (E.f i₂))

def CategoryTheory.GrothendieckTopology.OneHypercover.mk' {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} (E : PreOneHypercover S) [E.HasPullbacks] (mem₀ : E.sieve₀ ∈ J S) (mem₁' : ∀ (i₁ i₂ : E.I₀), E.sieve₁' i₁ i₂ ∈ J (Limits.pullback (E.f i₁) (E.f i₂))) : J.OneHypercover S

In order to check that a certain data is a 1-hypercover of S, it suffices to check that the data provides a covering of S and of the fibre products.

Equations

• CategoryTheory.GrothendieckTopology.OneHypercover.mk' E mem₀ mem₁' = { toPreOneHypercover := E, mem₀ := mem₀, mem₁ := ⋯ }

@[simp]

theorem CategoryTheory.GrothendieckTopology.OneHypercover.mk'_toPreOneHypercover {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} (E : PreOneHypercover S) [E.HasPullbacks] (mem₀ : E.sieve₀ ∈ J S) (mem₁' : ∀ (i₁ i₂ : E.I₀), E.sieve₁' i₁ i₂ ∈ J (Limits.pullback (E.f i₁) (E.f i₂))) : (mk' E mem₀ mem₁').toPreOneHypercover = E

noncomputable def CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift {C : Type u} [Category.{v, u} C] {A : Type u_1} [Category.{u_2, u_1} A] {J : GrothendieckTopology C} {S : C} {E : J.OneHypercover S} {F : Sheaf J A} (c : Limits.Multifork (E.multicospanIndex F.val)) : c.pt ⟶ F.val.obj (Opposite.op S)

Auxiliary definition of isLimitMultifork.

Equations

• CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift c = ⋯.amalgamateOfArrows E.f ⋯ c.ι ⋯

theorem CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift_map {C : Type u} [Category.{v, u} C] {A : Type u_1} [Category.{u_3, u_1} A] {J : GrothendieckTopology C} {S : C} {E : J.OneHypercover S} {F : Sheaf J A} (c : Limits.Multifork (E.multicospanIndex F.val)) (i₀ : E.I₀) : CategoryStruct.comp (multiforkLift c) (F.val.map (E.f i₀).op) = c.ι i₀

theorem CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift_map_assoc {C : Type u} [Category.{v, u} C] {A : Type u_1} [Category.{u_3, u_1} A] {J : GrothendieckTopology C} {S : C} {E : J.OneHypercover S} {F : Sheaf J A} (c : Limits.Multifork (E.multicospanIndex F.val)) (i₀ : E.I₀) {Z : A} (h : F.val.obj (Opposite.op (E.X i₀)) ⟶ Z) : CategoryStruct.comp (multiforkLift c) (CategoryStruct.comp (F.val.map (E.f i₀).op) h) = CategoryStruct.comp (c.ι i₀) h

noncomputable def CategoryTheory.GrothendieckTopology.OneHypercover.isLimitMultifork {C : Type u} [Category.{v, u} C] {A : Type u_1} [Category.{u_2, u_1} A] {J : GrothendieckTopology C} {S : C} (E : J.OneHypercover S) (F : Sheaf J A) : Limits.IsLimit (E.multifork F.val)

If E : J.OneHypercover S and F : Sheaf J A, then F.obj (op S) is a multiequalizer of suitable maps F.obj (op (E.X i)) ⟶ F.obj (op (E.Y j)) induced by E.p₁ j and E.p₂ j.

Equations

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

@[reducible, inline]

abbrev CategoryTheory.GrothendieckTopology.OneHypercover.Hom {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} (E : J.OneHypercover S) (F : J.OneHypercover S) : Type (max (max w w') v)

A morphism of 1-hypercovers is a morphism of the underlying pre-1-hypercovers.

Equations

• E.Hom F = E.Hom F.toPreOneHypercover

noncomputable def CategoryTheory.GrothendieckTopology.OneHypercover.cylinder {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} {E : J.OneHypercover S} {F : J.OneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) : J.OneHypercover S

Given two refinement morphism f, g : E ⟶ F, this is a 1-hypercover W that admits a morphism h : W ⟶ E such that h ≫ f and h ≫ g are homotopic. Hence they become equal after quotienting out by homotopy.

Equations

• CategoryTheory.GrothendieckTopology.OneHypercover.cylinder f g = CategoryTheory.GrothendieckTopology.OneHypercover.mk' (CategoryTheory.PreOneHypercover.cylinder f g) ⋯ ⋯

@[simp]

theorem CategoryTheory.GrothendieckTopology.OneHypercover.cylinder_toPreOneHypercover {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} {E : J.OneHypercover S} {F : J.OneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) : (cylinder f g).toPreOneHypercover = PreOneHypercover.cylinder f g

theorem CategoryTheory.GrothendieckTopology.OneHypercover.exists_nonempty_homotopy {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} {E : J.OneHypercover S} {F : J.OneHypercover S} [Limits.HasPullbacks C] (f g : E.Hom F) : ∃ (W : J.OneHypercover S) (h : W.Hom E), Nonempty (PreOneHypercover.Homotopy (PreOneHypercover.Hom.comp h f) (PreOneHypercover.Hom.comp h g))

Up to homotopy, the category of 1-hypercovers is cofiltered.

def CategoryTheory.GrothendieckTopology.Cover.preOneHypercover {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} (S : J.Cover X) : PreOneHypercover X

The tautological 1-pre-hypercover induced by S : J.Cover X. Its index type I₀ is given by S.Arrow (i.e. all the morphisms in the sieve S), while I₁ is given by all possible pullback cones.

Equations

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

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_p₂ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} (S : J.Cover X) (x✝ x✝¹ : S.Arrow) (r : x✝.Relation x✝¹) : S.preOneHypercover.p₂ r = r.g₂

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_Y {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} (S : J.Cover X) (x✝ x✝¹ : S.Arrow) (r : x✝.Relation x✝¹) : S.preOneHypercover.Y r = r.Z

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_p₁ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} (S : J.Cover X) (x✝ x✝¹ : S.Arrow) (r : x✝.Relation x✝¹) : S.preOneHypercover.p₁ r = r.g₁

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_f {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} (S : J.Cover X) (f : S.Arrow) : S.preOneHypercover.f f = f.f

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_I₀ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} (S : J.Cover X) : S.preOneHypercover.I₀ = S.Arrow

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_I₁ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} (S : J.Cover X) (f₁ f₂ : S.Arrow) : S.preOneHypercover.I₁ f₁ f₂ = f₁.Relation f₂

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_X {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} (S : J.Cover X) (f : S.Arrow) : S.preOneHypercover.X f = f.Y

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_sieve₀ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} (S : J.Cover X) : S.preOneHypercover.sieve₀ = ↑S

theorem CategoryTheory.GrothendieckTopology.Cover.preOneHypercover_sieve₁ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} (S : J.Cover X) (f₁ f₂ : S.Arrow) {W : C} (p₁ : W ⟶ f₁.Y) (p₂ : W ⟶ f₂.Y) (w : CategoryStruct.comp p₁ f₁.f = CategoryStruct.comp p₂ f₂.f) : S.preOneHypercover.sieve₁ p₁ p₂ = ⊤

def CategoryTheory.GrothendieckTopology.Cover.oneHypercover {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} (S : J.Cover X) : J.OneHypercover X

The tautological 1-hypercover induced by S : J.Cover X. Its index type I₀ is given by S.Arrow (i.e. all the morphisms in the sieve S), while I₁ is given by all possible pullback cones.

Equations

• S.oneHypercover = { toPreOneHypercover := S.preOneHypercover, mem₀ := ⋯, mem₁ := ⋯ }

@[simp]

theorem CategoryTheory.GrothendieckTopology.Cover.oneHypercover_toPreOneHypercover {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {X : C} (S : J.Cover X) : S.oneHypercover.toPreOneHypercover = S.preOneHypercover