1-hypercovers

Given a Grothendieck topology J on a category C, we define the type of 1-hypercovers of an object S : C. They consist 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 exists.

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) extends CategoryTheory.PreZeroHypercover S : 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
• X (i : self.I₀) : C
• f (i : self.I₀) : self.X i ⟶ 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₂)

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.Y' {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (i : E.I₁') : C

The 1-components as a function from the sigma type over E.I₁ i₁ i₂.

Equations

• E.Y' i = E.Y i.snd

@[simp]

theorem CategoryTheory.PreOneHypercover.Y'_apply {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (i : E.I₁') : E.Y' i = E.Y i.snd

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_L {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) : E.multicospanShape.L = 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_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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, 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) ⋯

@[simp]

theorem CategoryTheory.PreOneHypercover.multifork_ι {C : Type u} [Category.{v, u} C] {A : Type u_1} [Category.{v_1, u_1} A] {S : C} (E : PreOneHypercover S) (F : Functor Cᵒᵖ A) (i : E.I₀) : (E.multifork F).ι i = F.map (E.f i).op

def CategoryTheory.PreOneHypercover.forkOfIsColimit {C : Type u} [Category.{v, u} C] {A : Type u_1} [Category.{v_1, u_1} A] {S : C} (E : PreOneHypercover S) {c : Limits.Cofan E.X} (hc : Limits.IsColimit c) {d : Limits.Cofan E.Y'} (hd : Limits.IsColimit d) (F : Functor Cᵒᵖ A) : Limits.Fork (F.map (Limits.Cofan.IsColimit.desc hd fun (x : E.I₁') => CategoryStruct.comp (E.p₁ x.snd) (c.inj x.fst.1)).op) (F.map (Limits.Cofan.IsColimit.desc hd fun (x : E.I₁') => CategoryStruct.comp (E.p₂ x.snd) (c.inj x.fst.2)).op)

The fork associated to a pre-0-hypercover induced by taking the coproduct of the components.

Equations

• E.forkOfIsColimit hc hd F = CategoryTheory.Limits.Fork.ofι (F.map (CategoryTheory.Limits.Cofan.IsColimit.desc hc E.f).op) ⋯

@[simp]

theorem CategoryTheory.PreOneHypercover.forkOfIsColimit_pt {C : Type u} [Category.{v, u} C] {A : Type u_1} [Category.{v_1, u_1} A] {S : C} (E : PreOneHypercover S) {c : Limits.Cofan E.X} (hc : Limits.IsColimit c) {d : Limits.Cofan E.Y'} (hd : Limits.IsColimit d) (F : Functor Cᵒᵖ A) : (E.forkOfIsColimit hc hd F).pt = F.obj (Opposite.op S)

@[simp]

theorem CategoryTheory.PreOneHypercover.forkOfIsColimit_ι_map_inj {C : Type u} [Category.{v, u} C] {A : Type u_1} [Category.{v_1, u_1} A] {S : C} (E : PreOneHypercover S) {c : Limits.Cofan E.X} (hc : Limits.IsColimit c) {d : Limits.Cofan E.Y'} (hd : Limits.IsColimit d) (F : Functor Cᵒᵖ A) (i : E.I₀) : CategoryStruct.comp (E.forkOfIsColimit hc hd F).ι (F.map (c.inj i).op) = F.map (E.f i).op

@[simp]

theorem CategoryTheory.PreOneHypercover.forkOfIsColimit_ι_map_inj_assoc {C : Type u} [Category.{v, u} C] {A : Type u_1} [Category.{v_1, u_1} A] {S : C} (E : PreOneHypercover S) {c : Limits.Cofan E.X} (hc : Limits.IsColimit c) {d : Limits.Cofan E.Y'} (hd : Limits.IsColimit d) (F : Functor Cᵒᵖ A) (i : E.I₀) {Z : A} (h : F.obj (Opposite.op (E.X i)) ⟶ Z) : CategoryStruct.comp (E.forkOfIsColimit hc hd F).ι (CategoryStruct.comp (F.map (c.inj i).op) h) = CategoryStruct.comp (F.map (E.f i).op) h

noncomputable def CategoryTheory.PreOneHypercover.isLimitMultiforkEquivIsLimitFork {C : Type u} [Category.{v, u} C] {A : Type u_1} [Category.{v_1, u_1} A] {S : C} (E : PreOneHypercover S) {c : Limits.Cofan E.X} (hc : Limits.IsColimit c) {d : Limits.Cofan E.Y'} (hd : Limits.IsColimit d) (F : Functor Cᵒᵖ A) [Limits.PreservesLimit (Discrete.functor fun (i : E.I₀) => Opposite.op (E.X i)) F] [Limits.PreservesLimit (Discrete.functor fun (i : E.I₁') => Opposite.op (E.Y' i)) F] : Limits.IsLimit (E.multifork F) ≃ Limits.IsLimit (E.forkOfIsColimit hc hd F)

The multifork associated to a pre-1-hypercover is limiting if and only if the fork induced by taking the coproduct of the components is limiting.

Equations

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

def CategoryTheory.PreOneHypercover.sigmaOfIsColimit {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) {c : Limits.Cofan E.X} (hc : Limits.IsColimit c) {d : Limits.Cofan E.Y'} (hd : Limits.IsColimit d) : PreOneHypercover S

The single object pre-1-hypercover obtained from taking coproducts of the components.

Equations

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

@[simp]

theorem CategoryTheory.PreOneHypercover.sigmaOfIsColimit_Y {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) {c : Limits.Cofan E.X} (hc : Limits.IsColimit c) {d : Limits.Cofan E.Y'} (hd : Limits.IsColimit d) (x✝ x✝¹ : (E.sigmaOfIsColimit hc).I₀) (x✝² : PUnit.{w + 1}) : (E.sigmaOfIsColimit hc hd).Y x✝² = d.pt

@[simp]

theorem CategoryTheory.PreOneHypercover.sigmaOfIsColimit_toPreZeroHypercover {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) {c : Limits.Cofan E.X} (hc : Limits.IsColimit c) {d : Limits.Cofan E.Y'} (hd : Limits.IsColimit d) : (E.sigmaOfIsColimit hc hd).toPreZeroHypercover = E.sigmaOfIsColimit hc

@[simp]

theorem CategoryTheory.PreOneHypercover.p₁_sigmaOfIsColimit {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) {c : Limits.Cofan E.X} (hc : Limits.IsColimit c) {d : Limits.Cofan E.Y'} (hd : Limits.IsColimit d) (i : E.I₁') {a b : PUnit.{w + 1}} (r : (E.sigmaOfIsColimit hc hd).I₁ a b) : CategoryStruct.comp (d.inj i) ((E.sigmaOfIsColimit hc hd).p₁ r) = CategoryStruct.comp (E.p₁ i.snd) (c.inj i.fst.1)

@[simp]

theorem CategoryTheory.PreOneHypercover.p₁_sigmaOfIsColimit_assoc {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) {c : Limits.Cofan E.X} (hc : Limits.IsColimit c) {d : Limits.Cofan E.Y'} (hd : Limits.IsColimit d) (i : E.I₁') {a b : PUnit.{w + 1}} (r : (E.sigmaOfIsColimit hc hd).I₁ a b) {Z : C} (h : (E.sigmaOfIsColimit hc hd).X a ⟶ Z) : CategoryStruct.comp (d.inj i) (CategoryStruct.comp ((E.sigmaOfIsColimit hc hd).p₁ r) h) = CategoryStruct.comp (E.p₁ i.snd) (CategoryStruct.comp (c.inj i.fst.1) h)

@[simp]

theorem CategoryTheory.PreOneHypercover.p₂_sigmaOfIsColimit {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) {c : Limits.Cofan E.X} (hc : Limits.IsColimit c) {d : Limits.Cofan E.Y'} (hd : Limits.IsColimit d) (i : E.I₁') {a b : PUnit.{w + 1}} (r : (E.sigmaOfIsColimit hc hd).I₁ a b) : CategoryStruct.comp (d.inj i) ((E.sigmaOfIsColimit hc hd).p₂ r) = CategoryStruct.comp (E.p₂ i.snd) (c.inj i.fst.2)

@[simp]

theorem CategoryTheory.PreOneHypercover.p₂_sigmaOfIsColimit_assoc {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) {c : Limits.Cofan E.X} (hc : Limits.IsColimit c) {d : Limits.Cofan E.Y'} (hd : Limits.IsColimit d) (i : E.I₁') {a b : PUnit.{w + 1}} (r : (E.sigmaOfIsColimit hc hd).I₁ a b) {Z : C} (h : (E.sigmaOfIsColimit hc hd).X b ⟶ Z) : CategoryStruct.comp (d.inj i) (CategoryStruct.comp ((E.sigmaOfIsColimit hc hd).p₂ r) h) = CategoryStruct.comp (E.p₂ i.snd) (CategoryStruct.comp (c.inj i.fst.2) h)

@[implicit_reducible]

instance CategoryTheory.PreOneHypercover.instUniqueLMulticospanShapeSigmaOfIsColimit {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) {c : Limits.Cofan E.X} (hc : Limits.IsColimit c) {d : Limits.Cofan E.Y'} (hd : Limits.IsColimit d) : Unique (E.sigmaOfIsColimit hc hd).multicospanShape.L

Equations

• E.instUniqueLMulticospanShapeSigmaOfIsColimit hc hd = inferInstanceAs (Unique PUnit.{?u.83 + 1})

@[implicit_reducible]

instance CategoryTheory.PreOneHypercover.instUniqueRMulticospanShapeSigmaOfIsColimit {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) {c : Limits.Cofan E.X} (hc : Limits.IsColimit c) {d : Limits.Cofan E.Y'} (hd : Limits.IsColimit d) : Unique (E.sigmaOfIsColimit hc hd).multicospanShape.R

Equations

• E.instUniqueRMulticospanShapeSigmaOfIsColimit hc hd = { default := ⟨(PUnit.unit, PUnit.unit), PUnit.unit⟩, uniq := ⋯ }

noncomputable def CategoryTheory.PreOneHypercover.isLimitSigmaOfIsColimitEquiv {C : Type u} [Category.{v, u} C] {A : Type u_1} [Category.{v_1, u_1} A] {S : C} (E : PreOneHypercover S) {c : Limits.Cofan E.X} (hc : Limits.IsColimit c) {d : Limits.Cofan E.Y'} (hd : Limits.IsColimit d) (F : Functor Cᵒᵖ A) [Limits.PreservesLimit (Discrete.functor fun (i : E.I₀) => Opposite.op (E.X i)) F] [Limits.PreservesLimit (Discrete.functor fun (i : E.I₁') => Opposite.op (E.Y' i)) F] : Limits.IsLimit ((E.sigmaOfIsColimit hc hd).multifork F) ≃ Limits.IsLimit (E.multifork F)

If E is a pre-1-hypercover and F a presheaf, the induced equalizer of the single object covering obtained from E by taking coproducts is limiting if and only if the induced multiequalizer of E is limiting.

Equations

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

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

The trivial pre-1-hypercover of S with a single component S.

Equations

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

@[simp]

theorem CategoryTheory.PreOneHypercover.trivial_I₁ {C : Type u} [Category.{v, u} C] (S : C) (x✝ x✝¹ : (PreZeroHypercover.singleton (CategoryStruct.id S)).I₀) : (trivial S).I₁ x✝ x✝¹ = PUnit.{w + 1}

@[simp]

theorem CategoryTheory.PreOneHypercover.trivial_Y {C : Type u} [Category.{v, u} C] (S : C) (x✝ x✝¹ : (PreZeroHypercover.singleton (CategoryStruct.id S)).I₀) (x✝² : PUnit.{w + 1}) : (trivial S).Y x✝² = S

@[simp]

theorem CategoryTheory.PreOneHypercover.trivial_p₂ {C : Type u} [Category.{v, u} C] (S : C) (x✝ x✝¹ : (PreZeroHypercover.singleton (CategoryStruct.id S)).I₀) (x✝² : PUnit.{w + 1}) : (trivial S).p₂ x✝² = CategoryStruct.id S

@[simp]

theorem CategoryTheory.PreOneHypercover.trivial_toPreZeroHypercover {C : Type u} [Category.{v, u} C] (S : C) : (trivial S).toPreZeroHypercover = PreZeroHypercover.singleton (CategoryStruct.id S)

@[simp]

theorem CategoryTheory.PreOneHypercover.trivial_p₁ {C : Type u} [Category.{v, u} C] (S : C) (x✝ x✝¹ : (PreZeroHypercover.singleton (CategoryStruct.id S)).I₀) (x✝² : PUnit.{w + 1}) : (trivial S).p₁ x✝² = CategoryStruct.id S

theorem CategoryTheory.PreOneHypercover.sieve₀_trivial {C : Type u} [Category.{v, u} C] (S : C) : (trivial S).sieve₀ = ⊤

@[simp]

theorem CategoryTheory.PreOneHypercover.sieve₁_trivial {C : Type u} [Category.{v, u} C] {S W : C} {p : W ⟶ S} : (trivial S).sieve₁ p p = ⊤

instance CategoryTheory.PreOneHypercover.instNonempty {C : Type u} [Category.{v, u} C] {S : C} : Nonempty (PreOneHypercover S)

noncomputable def CategoryTheory.PreOneHypercover.inter {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (F : PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), Limits.HasPullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryStruct.comp (F.p₁ l) (F.f a))] : PreOneHypercover S

Intersection of two pre-1-hypercovers.

Equations

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

@[simp]

theorem CategoryTheory.PreOneHypercover.inter_I₁ {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (F : PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), Limits.HasPullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryStruct.comp (F.p₁ l) (F.f a))] (i j : (E.inter F.toPreZeroHypercover).I₀) : (E.inter F).I₁ i j = (E.I₁ i.1 j.1 × F.I₁ i.2 j.2)

@[simp]

theorem CategoryTheory.PreOneHypercover.inter_toPreZeroHypercover {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (F : PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), Limits.HasPullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryStruct.comp (F.p₁ l) (F.f a))] : (E.inter F).toPreZeroHypercover = E.inter F.toPreZeroHypercover

@[simp]

theorem CategoryTheory.PreOneHypercover.inter_p₂ {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (F : PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), Limits.HasPullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryStruct.comp (F.p₁ l) (F.f a))] (i j : (E.inter F.toPreZeroHypercover).I₀) (k : E.I₁ i.1 j.1 × F.I₁ i.2 j.2) : (E.inter F).p₂ k = Limits.pullback.map (CategoryStruct.comp (E.p₁ k.1) (E.f i.1)) (CategoryStruct.comp (F.p₁ k.2) (F.f i.2)) (E.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm j).fst) (F.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm j).snd) (E.p₂ k.1) (F.p₂ k.2) (CategoryStruct.id S) ⋯ ⋯

@[simp]

theorem CategoryTheory.PreOneHypercover.inter_p₁ {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (F : PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), Limits.HasPullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryStruct.comp (F.p₁ l) (F.f a))] (i j : (E.inter F.toPreZeroHypercover).I₀) (k : E.I₁ i.1 j.1 × F.I₁ i.2 j.2) : (E.inter F).p₁ k = Limits.pullback.map (CategoryStruct.comp (E.p₁ k.1) (E.f i.1)) (CategoryStruct.comp (F.p₁ k.2) (F.f i.2)) (E.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm i).fst) (F.f ((Equiv.sigmaEquivProd E.I₀ F.toPreZeroHypercover.1).symm i).snd) (E.p₁ k.1) (F.p₁ k.2) (CategoryStruct.id S) ⋯ ⋯

@[simp]

theorem CategoryTheory.PreOneHypercover.inter_Y {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (F : PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), Limits.HasPullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryStruct.comp (F.p₁ l) (F.f a))] (i j : (E.inter F.toPreZeroHypercover).I₀) (k : E.I₁ i.1 j.1 × F.I₁ i.2 j.2) : (E.inter F).Y k = Limits.pullback (CategoryStruct.comp (E.p₁ k.1) (E.f i.1)) (CategoryStruct.comp (F.p₁ k.2) (F.f i.2))

theorem CategoryTheory.PreOneHypercover.sieve₁_inter {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [Limits.HasPullbacks C] {i j : E.I₀ × F.I₀} {W : C} {p₁ : W ⟶ Limits.pullback (E.f i.1) (F.f i.2)} {p₂ : W ⟶ Limits.pullback (E.f j.1) (F.f j.2)} (w : CategoryStruct.comp p₁ (CategoryStruct.comp (Limits.pullback.fst (E.f i.1) (F.f i.2)) (E.f i.1)) = CategoryStruct.comp p₂ (CategoryStruct.comp (Limits.pullback.fst (E.f j.1) (F.f j.2)) (E.f j.1))) : (E.inter F).sieve₁ p₁ p₂ = Sieve.bind (E.sieve₁ (CategoryStruct.comp p₁ (Limits.pullback.fst (E.f i.1) (F.f i.2))) (CategoryStruct.comp p₂ (Limits.pullback.fst (E.f j.1) (F.f j.2)))).arrows fun (x : C) (f : x ⟶ W) (x_1 : (E.sieve₁ (CategoryStruct.comp p₁ (Limits.pullback.fst (E.f i.1) (F.f i.2))) (CategoryStruct.comp p₂ (Limits.pullback.fst (E.f j.1) (F.f j.2)))).arrows f) => Sieve.pullback f (F.sieve₁ (CategoryStruct.comp p₁ (Limits.pullback.snd (E.f i.1) (F.f i.2))) (CategoryStruct.comp p₂ (Limits.pullback.snd (E.f j.1) (F.f j.2))))

structure CategoryTheory.PreOneHypercover.Hom {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (F : PreOneHypercover S) extends E.Hom F.toPreZeroHypercover : 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₀
• h₀ (i : E.I₀) : E.X i ⟶ F.X (self.s₀ i)
• w₀ (i : E.I₀) : CategoryStruct.comp (self.h₀ i) (F.f (self.s₀ i)) = E.f i
• 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 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 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₀ ∧ x.h₀ ≍ y.h₀ ∧ @s₁ C inst✝ S E F x ≍ @s₁ C inst✝ S E F y ∧ @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₀) (h₀ : x.h₀ ≍ y.h₀) (s₁ : @s₁ C inst✝ S E F x ≍ @s₁ C inst✝ S E F y) (h₁ : @h₁ C inst✝ S E F x ≍ @h₁ C inst✝ S E F y) : x = y

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)

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)

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 = 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 = 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 : 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) (a✝ : E.I₀) : (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) {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_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))

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⟩

@[implicit_reducible]

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.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_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.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_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))

@[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.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.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))

def CategoryTheory.PreOneHypercover.oneToZero {C : Type u} [Category.{v, u} C] {S : C} : Functor (PreOneHypercover S) (PreZeroHypercover S)

The forgetful functor from pre-1-hypercovers to pre-0-hypercovers.

Equations

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

@[simp]

theorem CategoryTheory.PreOneHypercover.oneToZero_map {C : Type u} [Category.{v, u} C] {S : C} {X✝ Y✝ : PreOneHypercover S} (f : X✝ ⟶ Y✝) : oneToZero.map f = f.toHom

@[simp]

theorem CategoryTheory.PreOneHypercover.oneToZero_obj {C : Type u} [Category.{v, u} C] {S : C} (f : PreOneHypercover S) : oneToZero.obj f = f.toPreZeroHypercover

def CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit {C : Type u} [Category.{v, u} C] {A : Type u_1} [Category.{v_1, 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.{v_1, 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)) (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.{v_1, 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)) (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)

@[simp]

theorem CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit_id {C : Type u} [Category.{v, u} C] {A : Type u_1} [Category.{v_1, u_1} A] {S : C} {E : PreOneHypercover S} (P : Functor Cᵒᵖ A) {c : Limits.Multifork (E.multicospanIndex P)} (hc : Limits.IsLimit c) (d : Limits.Multifork (E.multicospanIndex P)) : (id E).mapMultiforkOfIsLimit P hc d = Limits.Multifork.IsLimit.lift hc d.ι ⋯

theorem CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit_comp {C : Type u} [Category.{v, u} C] {A : Type u_1} [Category.{v_1, u_1} A] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} {G : 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)} (g : F.Hom G) (t : Limits.Multifork (G.multicospanIndex P)) (hd : Limits.IsLimit d) : (f.comp g).mapMultiforkOfIsLimit P hc t = CategoryStruct.comp (g.mapMultiforkOfIsLimit P hd t) (f.mapMultiforkOfIsLimit P hc d)

theorem CategoryTheory.PreOneHypercover.Hom.mapMultiforkOfIsLimit_comp_assoc {C : Type u} [Category.{v, u} C] {A : Type u_1} [Category.{v_1, u_1} A] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} {G : 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)} (g : F.Hom G) (t : Limits.Multifork (G.multicospanIndex P)) (hd : Limits.IsLimit d) {Z : A} (h : c.pt ⟶ Z) : CategoryStruct.comp ((f.comp g).mapMultiforkOfIsLimit P hc t) h = CategoryStruct.comp (g.mapMultiforkOfIsLimit P hd t) (CategoryStruct.comp (f.mapMultiforkOfIsLimit P hc d) h)

def CategoryTheory.PreOneHypercover.congrIndexOneOfEq {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {i i' j j' : E.I₀} (hii' : i = i') (hjj' : j = j') : E.I₁ i j ≃ E.I₁ i' j'

If i = i' and j = j' this is an equivalence between the 1-index type at i, j and the one at i', j'.

Equations

• CategoryTheory.PreOneHypercover.congrIndexOneOfEq hii' hjj' = hii' ▸ hjj' ▸ Equiv.refl (E.I₁ i j)

@[simp]

theorem CategoryTheory.PreOneHypercover.congrIndexOneOfEq_refl {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} (i j : E.I₀) : congrIndexOneOfEq ⋯ ⋯ = Equiv.refl (E.I₁ i j)

@[simp]

theorem CategoryTheory.PreOneHypercover.congrIndexOneOfEq_trans {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {i i' j j' : E.I₀} (hii' : i = i') (hjj' : j = j') {i'' j'' : E.I₀} (hii'' : i' = i'') (hjj'' : j' = j'') (k : E.I₁ i j) : (congrIndexOneOfEq hii'' hjj'') ((congrIndexOneOfEq hii' hjj') k) = (congrIndexOneOfEq ⋯ ⋯) k

theorem CategoryTheory.PreOneHypercover.congrIndexOneOfEq_naturality {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} {i i' j j' : E.I₀} (hii' : i = i') (hjj' : j = j') (u₀ : E.I₀ → F.I₀) (u₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)) (k : E.I₁ i j) : u₁ ((congrIndexOneOfEq hii' hjj') k) = (congrIndexOneOfEq ⋯ ⋯) (u₁ k)

theorem CategoryTheory.PreOneHypercover.congrIndexOneOfEq_congrFun {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} {u₀ v₀ : E.I₀ → F.I₀} {u₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)} {v₁ : ⦃i j : E.I₀⦄ → E.I₁ i j → F.I₁ (v₀ i) (v₀ j)} (h₀ : u₀ = v₀) (h₁ : ∀ (i j : E.I₀) (k : E.I₁ i j), u₁ k = (congrIndexOneOfEq ⋯ ⋯) (v₁ k)) {i j : E.I₀} (k : E.I₁ i j) : (congrIndexOneOfEq ⋯ ⋯) (v₁ k) = u₁ k

theorem CategoryTheory.PreOneHypercover.I₁'.ext {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {a b : E.I₁'} (left : a.fst.1 = b.fst.1) (right : a.fst.2 = b.fst.2) (h : (congrIndexOneOfEq left right) a.snd = b.snd) : a = b

def CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {i i' j j' : E.I₀} (hii' : i = i') (hjj' : j = j') (k : E.I₁ i j) : E.Y ((congrIndexOneOfEq hii' hjj') k) ≅ E.Y k

If i = i' and j = j' this is the isomorphism between the 1-component at congrIndexOneOfEq k : E.I₁ i' j' and the 1-component at k : E.I₁ i j.

Note: This isomorphism could also be constructed inline from eqToIso. We only use eqToIso directly to construct isomorphisms E.Y k ≅ E.Y k' where k k' : E.I₁ i j and whenever k : E.I₁ i j and k' : E.I₁ i' j' have to be related we use congrIndexOneOfEqIso, possibly combined with an additional eqToIso instead. The reason for this is that the lemmas around eqToHom_naturality are hard to apply in the case where there is a mismatch in the type of the index.

Equations

• CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso hii' hjj' k = CategoryTheory.eqToIso ⋯

@[simp]

theorem CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_refl {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {i j : E.I₀} (k : E.I₁ i j) : congrIndexOneOfEqIso ⋯ ⋯ k = Iso.refl (E.Y ((congrIndexOneOfEq ⋯ ⋯) k))

@[simp]

theorem CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_hom_p₁ {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {i i' j j' : E.I₀} (hii' : i = i') (hjj' : j = j') (k : E.I₁ i j) : CategoryStruct.comp (congrIndexOneOfEqIso hii' hjj' k).hom (E.p₁ k) = CategoryStruct.comp (E.p₁ ((congrIndexOneOfEq hii' hjj') k)) (eqToHom ⋯)

@[simp]

theorem CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_hom_p₁_assoc {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {i i' j j' : E.I₀} (hii' : i = i') (hjj' : j = j') (k : E.I₁ i j) {Z : C} (h : E.X i ⟶ Z) : CategoryStruct.comp (congrIndexOneOfEqIso hii' hjj' k).hom (CategoryStruct.comp (E.p₁ k) h) = CategoryStruct.comp (E.p₁ ((congrIndexOneOfEq hii' hjj') k)) (CategoryStruct.comp (eqToHom ⋯) h)

@[simp]

theorem CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_inv_p₁ {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {i i' j j' : E.I₀} (hii' : i = i') (hjj' : j = j') (k : E.I₁ i j) : CategoryStruct.comp (congrIndexOneOfEqIso hii' hjj' k).inv (E.p₁ ((congrIndexOneOfEq hii' hjj') k)) = CategoryStruct.comp (E.p₁ k) (eqToHom ⋯)

@[simp]

theorem CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_inv_p₁_assoc {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {i i' j j' : E.I₀} (hii' : i = i') (hjj' : j = j') (k : E.I₁ i j) {Z : C} (h : E.X i' ⟶ Z) : CategoryStruct.comp (congrIndexOneOfEqIso hii' hjj' k).inv (CategoryStruct.comp (E.p₁ ((congrIndexOneOfEq hii' hjj') k)) h) = CategoryStruct.comp (E.p₁ k) (CategoryStruct.comp (eqToHom ⋯) h)

@[simp]

theorem CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_inv_p₂ {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {i i' j j' : E.I₀} (hii' : i = i') (hjj' : j = j') (k : E.I₁ i j) : CategoryStruct.comp (congrIndexOneOfEqIso hii' hjj' k).inv (E.p₂ ((congrIndexOneOfEq hii' hjj') k)) = CategoryStruct.comp (E.p₂ k) (eqToHom ⋯)

@[simp]

theorem CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_inv_p₂_assoc {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {i i' j j' : E.I₀} (hii' : i = i') (hjj' : j = j') (k : E.I₁ i j) {Z : C} (h : E.X j' ⟶ Z) : CategoryStruct.comp (congrIndexOneOfEqIso hii' hjj' k).inv (CategoryStruct.comp (E.p₂ ((congrIndexOneOfEq hii' hjj') k)) h) = CategoryStruct.comp (E.p₂ k) (CategoryStruct.comp (eqToHom ⋯) h)

theorem CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_hom_naturality {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} {i i' j j' : E.I₀} (u₀ : E.I₀ → F.I₀) (u₁ : (i j : E.I₀) → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)) (z : (i j : E.I₀) → (k : E.I₁ i j) → E.Y k ⟶ F.Y (u₁ i j k)) (hii' : i = i') (hjj' : j = j') (k : E.I₁ i j) : CategoryStruct.comp (congrIndexOneOfEqIso hii' hjj' k).hom (z i j k) = CategoryStruct.comp (z i' j' ((congrIndexOneOfEq hii' hjj') k)) (CategoryStruct.comp (eqToHom ⋯) (congrIndexOneOfEqIso ⋯ ⋯ (u₁ i j k)).hom)

theorem CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_hom_naturality_assoc {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} {i i' j j' : E.I₀} (u₀ : E.I₀ → F.I₀) (u₁ : (i j : E.I₀) → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)) (z : (i j : E.I₀) → (k : E.I₁ i j) → E.Y k ⟶ F.Y (u₁ i j k)) (hii' : i = i') (hjj' : j = j') (k : E.I₁ i j) {Z : C} (h : F.Y (u₁ i j k) ⟶ Z) : CategoryStruct.comp (congrIndexOneOfEqIso hii' hjj' k).hom (CategoryStruct.comp (z i j k) h) = CategoryStruct.comp (z i' j' ((congrIndexOneOfEq hii' hjj') k)) (CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (congrIndexOneOfEqIso ⋯ ⋯ (u₁ i j k)).hom h))

theorem CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_inv_naturality {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} {i i' j j' : E.I₀} (u₀ : E.I₀ → F.I₀) (u₁ : (i j : E.I₀) → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)) (z : (i j : E.I₀) → (k : E.I₁ i j) → E.Y k ⟶ F.Y (u₁ i j k)) (hii' : i = i') (hjj' : j = j') (k : E.I₁ i j) : CategoryStruct.comp (congrIndexOneOfEqIso hii' hjj' k).inv (CategoryStruct.comp (z i' j' ((congrIndexOneOfEq hii' hjj') k)) (eqToHom ⋯)) = CategoryStruct.comp (z i j k) (congrIndexOneOfEqIso ⋯ ⋯ (u₁ i j k)).inv

theorem CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_inv_naturality_assoc {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} {i i' j j' : E.I₀} (u₀ : E.I₀ → F.I₀) (u₁ : (i j : E.I₀) → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)) (z : (i j : E.I₀) → (k : E.I₁ i j) → E.Y k ⟶ F.Y (u₁ i j k)) (hii' : i = i') (hjj' : j = j') (k : E.I₁ i j) {Z : C} (h : F.Y ((congrIndexOneOfEq ⋯ ⋯) (u₁ i j k)) ⟶ Z) : CategoryStruct.comp (congrIndexOneOfEqIso hii' hjj' k).inv (CategoryStruct.comp (z i' j' ((congrIndexOneOfEq hii' hjj') k)) (CategoryStruct.comp (eqToHom ⋯) h)) = CategoryStruct.comp (z i j k) (CategoryStruct.comp (congrIndexOneOfEqIso ⋯ ⋯ (u₁ i j k)).inv h)

theorem CategoryTheory.PreOneHypercover.Hom.ext' {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} {f g : E.Hom F} (hs₀ : f.s₀ = g.s₀) (hh₀ : ∀ (i : E.I₀), f.h₀ i = CategoryStruct.comp (g.h₀ i) (eqToHom ⋯)) (hs₁ : ∀ (i j : E.I₀) (k : E.I₁ i j), f.s₁ k = (congrIndexOneOfEq ⋯ ⋯) (g.s₁ k)) (hh₁ : ∀ (i j : E.I₀) (k : E.I₁ i j), f.h₁ k = CategoryStruct.comp (g.h₁ k) (CategoryStruct.comp (congrIndexOneOfEqIso ⋯ ⋯ (g.s₁ k)).inv (eqToHom ⋯))) : f = g

theorem CategoryTheory.PreOneHypercover.Hom.ext'_iff {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} {f g : E.Hom F} : f = g ↔ ∃ (hs₀ : f.s₀ = g.s₀) (_ : ∀ (i : E.I₀), f.h₀ i = CategoryStruct.comp (g.h₀ i) (eqToHom ⋯)) (hs₁ : ∀ (i j : E.I₀) (k : E.I₁ i j), f.s₁ k = (congrIndexOneOfEq ⋯ ⋯) (g.s₁ k)), ∀ (i j : E.I₀) (k : E.I₁ i j), f.h₁ k = CategoryStruct.comp (g.h₁ k) (CategoryStruct.comp (congrIndexOneOfEqIso ⋯ ⋯ (g.s₁ k)).inv (eqToHom ⋯))

theorem CategoryTheory.PreOneHypercover.congrIndexOneOfEq_equiv {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} (s₀ : E.I₀ ≃ F.I₀) (s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)) {i j : E.I₀} (k : E.I₁ i j) : (congrIndexOneOfEq ⋯ ⋯) k = s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k))

theorem CategoryTheory.PreOneHypercover.isoMk_aux {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} (s₀ : E.I₀ ≃ F.I₀) (s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)) {i j : E.I₀} (h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)) (k : E.I₁ i j) : CategoryStruct.comp (h₁ k).hom (CategoryStruct.comp (congrIndexOneOfEqIso ⋯ ⋯ (s₁ k)).inv (CategoryStruct.comp (eqToHom ⋯) (h₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k)))).inv)) = CategoryStruct.comp (congrIndexOneOfEqIso ⋯ ⋯ k).inv (eqToHom ⋯)

(Implementation): Auxiliary lemma for CategoryTheory.PreOneHypercover.isoMk.

theorem CategoryTheory.PreOneHypercover.isoMk_aux_assoc {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} (s₀ : E.I₀ ≃ F.I₀) (s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)) {i j : E.I₀} (h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)) (k : E.I₁ i j) {Z : C} (h : E.Y (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k))) ⟶ Z) : CategoryStruct.comp (h₁ k).hom (CategoryStruct.comp (congrIndexOneOfEqIso ⋯ ⋯ (s₁ k)).inv (CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (h₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) (s₁ k)))).inv h))) = CategoryStruct.comp (congrIndexOneOfEqIso ⋯ ⋯ k).inv (CategoryStruct.comp (eqToHom ⋯) h)

(Implementation): Auxiliary lemma for CategoryTheory.PreOneHypercover.isoMk.

def CategoryTheory.PreOneHypercover.isoMk {C : Type u} [Category.{v, u} C] {S : C} {E F : PreOneHypercover S} (s₀ : E.I₀ ≃ F.I₀) (h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)) (s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)) (h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)) (w₀ : ∀ (i : E.I₀), CategoryStruct.comp (h₀ i).hom (F.f (s₀ i)) = E.f i := by cat_disch) (w₁₁ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), CategoryStruct.comp (h₁ k).hom (F.p₁ (s₁ k)) = CategoryStruct.comp (E.p₁ k) (h₀ i).hom := by cat_disch) (w₁₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), CategoryStruct.comp (h₁ k).hom (F.p₂ (s₁ k)) = CategoryStruct.comp (E.p₂ k) (h₀ j).hom := by cat_disch) : E ≅ F

Construct an isomorphism of 1-hypercovers by giving the compatibility conditions only in the forward direction.

Equations

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

@[simp]

theorem CategoryTheory.PreOneHypercover.isoMk_inv_s₁ {C : Type u} [Category.{v, u} C] {S : C} {E F : PreOneHypercover S} (s₀ : E.I₀ ≃ F.I₀) (h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)) (s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)) (h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)) (w₀ : ∀ (i : E.I₀), CategoryStruct.comp (h₀ i).hom (F.f (s₀ i)) = E.f i := by cat_disch) (w₁₁ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), CategoryStruct.comp (h₁ k).hom (F.p₁ (s₁ k)) = CategoryStruct.comp (E.p₁ k) (h₀ i).hom := by cat_disch) (w₁₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), CategoryStruct.comp (h₁ k).hom (F.p₂ (s₁ k)) = CategoryStruct.comp (E.p₂ k) (h₀ j).hom := by cat_disch) {i j : F.I₀} (k : F.I₁ i j) : (isoMk s₀ h₀ s₁ h₁ w₀ w₁₁ w₁₂).inv.s₁ k = s₁.symm ((congrIndexOneOfEq ⋯ ⋯) k)

@[simp]

theorem CategoryTheory.PreOneHypercover.isoMk_inv_h₀ {C : Type u} [Category.{v, u} C] {S : C} {E F : PreOneHypercover S} (s₀ : E.I₀ ≃ F.I₀) (h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)) (s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)) (h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)) (w₀ : ∀ (i : E.I₀), CategoryStruct.comp (h₀ i).hom (F.f (s₀ i)) = E.f i := by cat_disch) (w₁₁ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), CategoryStruct.comp (h₁ k).hom (F.p₁ (s₁ k)) = CategoryStruct.comp (E.p₁ k) (h₀ i).hom := by cat_disch) (w₁₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), CategoryStruct.comp (h₁ k).hom (F.p₂ (s₁ k)) = CategoryStruct.comp (E.p₂ k) (h₀ j).hom := by cat_disch) (i : F.I₀) : (isoMk s₀ h₀ s₁ h₁ w₀ w₁₁ w₁₂).inv.h₀ i = CategoryStruct.comp (eqToHom ⋯) (h₀ (s₀.symm i)).inv

@[simp]

theorem CategoryTheory.PreOneHypercover.isoMk_hom_s₀ {C : Type u} [Category.{v, u} C] {S : C} {E F : PreOneHypercover S} (s₀ : E.I₀ ≃ F.I₀) (h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)) (s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)) (h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)) (w₀ : ∀ (i : E.I₀), CategoryStruct.comp (h₀ i).hom (F.f (s₀ i)) = E.f i := by cat_disch) (w₁₁ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), CategoryStruct.comp (h₁ k).hom (F.p₁ (s₁ k)) = CategoryStruct.comp (E.p₁ k) (h₀ i).hom := by cat_disch) (w₁₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), CategoryStruct.comp (h₁ k).hom (F.p₂ (s₁ k)) = CategoryStruct.comp (E.p₂ k) (h₀ j).hom := by cat_disch) (a : E.I₀) : (isoMk s₀ h₀ s₁ h₁ w₀ w₁₁ w₁₂).hom.s₀ a = s₀ a

@[simp]

theorem CategoryTheory.PreOneHypercover.isoMk_inv_h₁ {C : Type u} [Category.{v, u} C] {S : C} {E F : PreOneHypercover S} (s₀ : E.I₀ ≃ F.I₀) (h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)) (s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)) (h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)) (w₀ : ∀ (i : E.I₀), CategoryStruct.comp (h₀ i).hom (F.f (s₀ i)) = E.f i := by cat_disch) (w₁₁ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), CategoryStruct.comp (h₁ k).hom (F.p₁ (s₁ k)) = CategoryStruct.comp (E.p₁ k) (h₀ i).hom := by cat_disch) (w₁₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), CategoryStruct.comp (h₁ k).hom (F.p₂ (s₁ k)) = CategoryStruct.comp (E.p₂ k) (h₀ j).hom := by cat_disch) {i j : F.I₀} (k : F.I₁ i j) : (isoMk s₀ h₀ s₁ h₁ w₀ w₁₁ w₁₂).inv.h₁ k = CategoryStruct.comp (congrIndexOneOfEqIso ⋯ ⋯ k).inv (CategoryStruct.comp (eqToHom ⋯) (h₁ (s₁.symm ((congrIndexOneOfEq ⋯ ⋯) k))).inv)

@[simp]

theorem CategoryTheory.PreOneHypercover.isoMk_hom_h₁ {C : Type u} [Category.{v, u} C] {S : C} {E F : PreOneHypercover S} (s₀ : E.I₀ ≃ F.I₀) (h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)) (s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)) (h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)) (w₀ : ∀ (i : E.I₀), CategoryStruct.comp (h₀ i).hom (F.f (s₀ i)) = E.f i := by cat_disch) (w₁₁ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), CategoryStruct.comp (h₁ k).hom (F.p₁ (s₁ k)) = CategoryStruct.comp (E.p₁ k) (h₀ i).hom := by cat_disch) (w₁₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), CategoryStruct.comp (h₁ k).hom (F.p₂ (s₁ k)) = CategoryStruct.comp (E.p₂ k) (h₀ j).hom := by cat_disch) {i✝ j✝ : E.I₀} (k : E.I₁ i✝ j✝) : (isoMk s₀ h₀ s₁ h₁ w₀ w₁₁ w₁₂).hom.h₁ k = (h₁ k).hom

@[simp]

theorem CategoryTheory.PreOneHypercover.isoMk_inv_s₀ {C : Type u} [Category.{v, u} C] {S : C} {E F : PreOneHypercover S} (s₀ : E.I₀ ≃ F.I₀) (h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)) (s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)) (h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)) (w₀ : ∀ (i : E.I₀), CategoryStruct.comp (h₀ i).hom (F.f (s₀ i)) = E.f i := by cat_disch) (w₁₁ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), CategoryStruct.comp (h₁ k).hom (F.p₁ (s₁ k)) = CategoryStruct.comp (E.p₁ k) (h₀ i).hom := by cat_disch) (w₁₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), CategoryStruct.comp (h₁ k).hom (F.p₂ (s₁ k)) = CategoryStruct.comp (E.p₂ k) (h₀ j).hom := by cat_disch) (a : F.I₀) : (isoMk s₀ h₀ s₁ h₁ w₀ w₁₁ w₁₂).inv.s₀ a = s₀.symm a

@[simp]

theorem CategoryTheory.PreOneHypercover.isoMk_hom_s₁ {C : Type u} [Category.{v, u} C] {S : C} {E F : PreOneHypercover S} (s₀ : E.I₀ ≃ F.I₀) (h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)) (s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)) (h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)) (w₀ : ∀ (i : E.I₀), CategoryStruct.comp (h₀ i).hom (F.f (s₀ i)) = E.f i := by cat_disch) (w₁₁ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), CategoryStruct.comp (h₁ k).hom (F.p₁ (s₁ k)) = CategoryStruct.comp (E.p₁ k) (h₀ i).hom := by cat_disch) (w₁₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), CategoryStruct.comp (h₁ k).hom (F.p₂ (s₁ k)) = CategoryStruct.comp (E.p₂ k) (h₀ j).hom := by cat_disch) {i✝ j✝ : E.I₀} (k : E.I₁ i✝ j✝) : (isoMk s₀ h₀ s₁ h₁ w₀ w₁₁ w₁₂).hom.s₁ k = s₁ k

@[simp]

theorem CategoryTheory.PreOneHypercover.isoMk_hom_h₀ {C : Type u} [Category.{v, u} C] {S : C} {E F : PreOneHypercover S} (s₀ : E.I₀ ≃ F.I₀) (h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)) (s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j)) (h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k)) (w₀ : ∀ (i : E.I₀), CategoryStruct.comp (h₀ i).hom (F.f (s₀ i)) = E.f i := by cat_disch) (w₁₁ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), CategoryStruct.comp (h₁ k).hom (F.p₁ (s₁ k)) = CategoryStruct.comp (E.p₁ k) (h₀ i).hom := by cat_disch) (w₁₂ : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), CategoryStruct.comp (h₁ k).hom (F.p₂ (s₁ k)) = CategoryStruct.comp (E.p₂ k) (h₀ j).hom := by cat_disch) (i : E.I₀) : (isoMk s₀ h₀ s₁ h₁ w₀ w₁₁ w₁₂).hom.h₀ i = (h₀ i).hom

@[simp]

theorem CategoryTheory.PreOneHypercover.hom_inv_s₀_apply {C : Type u} [Category.{v, u} C] {S : C} {E F : PreOneHypercover S} (e : E ≅ F) (i : E.I₀) : e.inv.s₀ (e.hom.s₀ i) = i

@[simp]

theorem CategoryTheory.PreOneHypercover.inv_hom_s₀_apply {C : Type u} [Category.{v, u} C] {S : C} {E F : PreOneHypercover S} (e : E ≅ F) (i : F.I₀) : e.hom.s₀ (e.inv.s₀ i) = i

@[simp]

theorem CategoryTheory.PreOneHypercover.hom_inv_s₁_apply {C : Type u} [Category.{v, u} C] {S : C} {E F : PreOneHypercover S} (e : E ≅ F) {i j : E.I₀} (k : E.I₁ i j) : e.inv.s₁ (e.hom.s₁ k) = (congrIndexOneOfEq ⋯ ⋯) k

@[simp]

theorem CategoryTheory.PreOneHypercover.inv_hom_s₁_apply {C : Type u} [Category.{v, u} C] {S : C} {E F : PreOneHypercover S} (e : E ≅ F) {i j : F.I₀} (k : F.I₁ i j) : e.hom.s₁ (e.inv.s₁ k) = (congrIndexOneOfEq ⋯ ⋯) k

@[simp]

theorem CategoryTheory.PreOneHypercover.hom_inv_h₀ {C : Type u} [Category.{v, u} C] {S : C} {E F : PreOneHypercover S} (e : E ≅ F) (i : E.I₀) : CategoryStruct.comp (e.hom.h₀ i) (e.inv.h₀ (e.hom.s₀ i)) = eqToHom ⋯

@[simp]

theorem CategoryTheory.PreOneHypercover.hom_inv_h₀_assoc {C : Type u} [Category.{v, u} C] {S : C} {E F : PreOneHypercover S} (e : E ≅ F) (i : E.I₀) {Z : C} (h : E.X (e.inv.s₀ (e.hom.s₀ i)) ⟶ Z) : CategoryStruct.comp (e.hom.h₀ i) (CategoryStruct.comp (e.inv.h₀ (e.hom.s₀ i)) h) = CategoryStruct.comp (eqToHom ⋯) h

@[simp]

theorem CategoryTheory.PreOneHypercover.inv_hom_h₀ {C : Type u} [Category.{v, u} C] {S : C} {E F : PreOneHypercover S} (e : E ≅ F) (i : F.I₀) : CategoryStruct.comp (e.inv.h₀ i) (e.hom.h₀ (e.inv.s₀ i)) = eqToHom ⋯

@[simp]

theorem CategoryTheory.PreOneHypercover.inv_hom_h₀_assoc {C : Type u} [Category.{v, u} C] {S : C} {E F : PreOneHypercover S} (e : E ≅ F) (i : F.I₀) {Z : C} (h : F.X (e.hom.s₀ (e.inv.s₀ i)) ⟶ Z) : CategoryStruct.comp (e.inv.h₀ i) (CategoryStruct.comp (e.hom.h₀ (e.inv.s₀ i)) h) = CategoryStruct.comp (eqToHom ⋯) h

@[simp]

theorem CategoryTheory.PreOneHypercover.hom_inv_h₁ {C : Type u} [Category.{v, u} C] {S : C} {E F : PreOneHypercover S} (e : E ≅ F) {i j : E.I₀} (k : E.I₁ i j) : CategoryStruct.comp (e.hom.h₁ k) (e.inv.h₁ (e.hom.s₁ k)) = CategoryStruct.comp (congrIndexOneOfEqIso ⋯ ⋯ k).inv (eqToHom ⋯)

@[simp]

theorem CategoryTheory.PreOneHypercover.hom_inv_h₁_assoc {C : Type u} [Category.{v, u} C] {S : C} {E F : PreOneHypercover S} (e : E ≅ F) {i j : E.I₀} (k : E.I₁ i j) {Z : C} (h : E.Y (e.inv.s₁ (e.hom.s₁ k)) ⟶ Z) : CategoryStruct.comp (e.hom.h₁ k) (CategoryStruct.comp (e.inv.h₁ (e.hom.s₁ k)) h) = CategoryStruct.comp (congrIndexOneOfEqIso ⋯ ⋯ k).inv (CategoryStruct.comp (eqToHom ⋯) h)

@[simp]

theorem CategoryTheory.PreOneHypercover.inv_hom_h₁ {C : Type u} [Category.{v, u} C] {S : C} {E F : PreOneHypercover S} (e : E ≅ F) {i j : F.I₀} (k : F.I₁ i j) : CategoryStruct.comp (e.inv.h₁ k) (e.hom.h₁ (e.inv.s₁ k)) = CategoryStruct.comp (congrIndexOneOfEqIso ⋯ ⋯ k).inv (eqToHom ⋯)

@[simp]

theorem CategoryTheory.PreOneHypercover.inv_hom_h₁_assoc {C : Type u} [Category.{v, u} C] {S : C} {E F : PreOneHypercover S} (e : E ≅ F) {i j : F.I₀} (k : F.I₁ i j) {Z : C} (h : F.Y (e.hom.s₁ (e.inv.s₁ k)) ⟶ Z) : CategoryStruct.comp (e.inv.h₁ k) (CategoryStruct.comp (e.hom.h₁ (e.inv.s₁ k)) h) = CategoryStruct.comp (congrIndexOneOfEqIso ⋯ ⋯ k).inv (CategoryStruct.comp (eqToHom ⋯) h)

instance CategoryTheory.PreOneHypercover.instIsIsoH₀Hom {C : Type u} [Category.{v, u} C] {S : C} {E F : PreOneHypercover S} (e : E ≅ F) (i : E.I₀) : IsIso (e.hom.h₀ i)

instance CategoryTheory.PreOneHypercover.instIsIsoH₀Inv {C : Type u} [Category.{v, u} C] {S : C} {E F : PreOneHypercover S} (e : E ≅ F) (i : F.I₀) : IsIso (e.inv.h₀ i)

instance CategoryTheory.PreOneHypercover.instIsIsoH₁Hom {C : Type u} [Category.{v, u} C] {S : C} {E F : PreOneHypercover S} (e : E ≅ F) {i j : E.I₀} (k : E.I₁ i j) : IsIso (e.hom.h₁ k)

instance CategoryTheory.PreOneHypercover.instIsIsoH₁Inv {C : Type u} [Category.{v, u} C] {S : C} {E F : PreOneHypercover S} (e : E ≅ F) {i j : F.I₀} (k : F.I₁ i j) : IsIso (e.inv.h₁ k)

def CategoryTheory.PreOneHypercover.Hom.mapMulticospan {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} (f : E.Hom F) : Functor (Limits.WalkingMulticospan E.multicospanShape) (Limits.WalkingMulticospan F.multicospanShape)

A refinement morphism E ⟶ F induces a functor between the multifork indexing categories.

Equations

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

@[simp]

theorem CategoryTheory.PreOneHypercover.Hom.mapMulticospan_obj {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} (f : E.Hom F) (x✝ : Limits.WalkingMulticospan E.multicospanShape) : f.mapMulticospan.obj x✝ = match x✝ with | Limits.WalkingMulticospan.left i => Limits.WalkingMulticospan.left (f.s₀ i) | Limits.WalkingMulticospan.right i => Limits.WalkingMulticospan.right (f.s₁' i)

@[simp]

theorem CategoryTheory.PreOneHypercover.Hom.mapMulticospan_map {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} (f : E.Hom F) {X✝ Y✝ : Limits.WalkingMulticospan E.multicospanShape} (x✝ : X✝ ⟶ Y✝) : f.mapMulticospan.map x✝ = match X✝, Y✝, x✝ with | x, .(x), Limits.WalkingMulticospan.Hom.id .(x) => Limits.WalkingMulticospan.Hom.id (match x with | Limits.WalkingMulticospan.left i => Limits.WalkingMulticospan.left (f.s₀ i) | Limits.WalkingMulticospan.right i => Limits.WalkingMulticospan.right (f.s₁' i)) | .(Limits.WalkingMulticospan.left (E.multicospanShape.fst i)), .(Limits.WalkingMulticospan.right i), Limits.WalkingMulticospan.Hom.fst i => Limits.WalkingMulticospan.Hom.fst (f.s₁' i) | .(Limits.WalkingMulticospan.left (E.multicospanShape.snd i)), .(Limits.WalkingMulticospan.right i), Limits.WalkingMulticospan.Hom.snd i => Limits.WalkingMulticospan.Hom.snd (f.s₁' i)

def CategoryTheory.PreOneHypercover.equivalenceMulticospanOfIso {C : Type u} [Category.{v, u} C] {S : C} {E F : PreOneHypercover S} (f : E ≅ F) : Limits.WalkingMulticospan E.multicospanShape ≌ Limits.WalkingMulticospan F.multicospanShape

Isomorphic pre-1-hypercovers have equivalent mutifork index categories.

Equations

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

@[simp]

theorem CategoryTheory.PreOneHypercover.equivalenceMulticospanOfIso_functor {C : Type u} [Category.{v, u} C] {S : C} {E F : PreOneHypercover S} (f : E ≅ F) : (equivalenceMulticospanOfIso f).functor = Hom.mapMulticospan f.hom

@[simp]

theorem CategoryTheory.PreOneHypercover.equivalenceMulticospanOfIso_inverse {C : Type u} [Category.{v, u} C] {S : C} {E F : PreOneHypercover S} (f : E ≅ F) : (equivalenceMulticospanOfIso f).inverse = Hom.mapMulticospan f.inv

noncomputable def CategoryTheory.PreOneHypercover.isLimitEquivOfIso {C : Type u} [Category.{v, u} C] {A : Type u_1} [Category.{v_1, u_1} A] {S : C} {E F : PreOneHypercover S} (f : E ≅ F) (G : Functor Cᵒᵖ A) : Limits.IsLimit (E.multifork G) ≃ Limits.IsLimit (F.multifork G)

If E and F are isomorphic pre-1-hypercovers and G is a presheaf, the multifork for E is exact if and only if the multifork for E is exact.

Equations

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

noncomputable def CategoryTheory.PreOneHypercover.interFst {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (F : PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), Limits.HasPullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryStruct.comp (F.p₁ l) (F.f a))] : (E.inter F).Hom E

First projection from the intersection of two pre-1-hypercovers.

Equations

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

@[simp]

theorem CategoryTheory.PreOneHypercover.interFst_toHom {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (F : PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), Limits.HasPullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryStruct.comp (F.p₁ l) (F.f a))] : (E.interFst F).toHom = E.interFst F.toPreZeroHypercover

@[simp]

theorem CategoryTheory.PreOneHypercover.interFst_s₁ {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (F : PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), Limits.HasPullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryStruct.comp (F.p₁ l) (F.f a))] {i j : (E.inter F).I₀} (k : (E.inter F).I₁ i j) : (E.interFst F).s₁ k = k.1

noncomputable def CategoryTheory.PreOneHypercover.interSnd {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (F : PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), Limits.HasPullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryStruct.comp (F.p₁ l) (F.f a))] : (E.inter F).Hom F

Second projection from the intersection of two pre-1-hypercovers.

Equations

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

@[simp]

theorem CategoryTheory.PreOneHypercover.interSnd_toHom {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (F : PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), Limits.HasPullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryStruct.comp (F.p₁ l) (F.f a))] : (E.interSnd F).toHom = E.interSnd F.toPreZeroHypercover

@[simp]

theorem CategoryTheory.PreOneHypercover.interSnd_s₁ {C : Type u} [Category.{v, u} C] {S : C} (E : PreOneHypercover S) (F : PreOneHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), Limits.HasPullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryStruct.comp (F.p₁ l) (F.f a))] {i j : (E.inter F).I₀} (k : (E.inter F).I₁ i j) : (E.interSnd F).s₁ k = k.2

noncomputable def CategoryTheory.PreOneHypercover.interLift {C : Type u} [Category.{v, u} C] {S : C} {E : PreOneHypercover S} {F : PreOneHypercover S} [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), Limits.HasPullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryStruct.comp (F.p₁ l) (F.f a))] {G : PreOneHypercover S} (f : G.Hom E) (g : G.Hom F) : G.Hom (E.inter F)

Universal property of the intersection of two pre-1-hypercovers.

Equations

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

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.{v_1, u_1} A] {J : GrothendieckTopology C} {S : C} {E : J.OneHypercover S} {F : Sheaf J A} (c : Limits.Multifork (E.multicospanIndex F.obj)) : c.pt ⟶ F.obj.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.{v_1, u_1} A] {J : GrothendieckTopology C} {S : C} {E : J.OneHypercover S} {F : Sheaf J A} (c : Limits.Multifork (E.multicospanIndex F.obj)) (i₀ : E.I₀) : CategoryStruct.comp (multiforkLift c) (F.obj.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.{v_1, u_1} A] {J : GrothendieckTopology C} {S : C} {E : J.OneHypercover S} {F : Sheaf J A} (c : Limits.Multifork (E.multicospanIndex F.obj)) (i₀ : E.I₀) {Z : A} (h : F.obj.obj (Opposite.op (E.X i₀)) ⟶ Z) : CategoryStruct.comp (multiforkLift c) (CategoryStruct.comp (F.obj.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.{v_1, u_1} A] {J : GrothendieckTopology C} {S : C} (E : J.OneHypercover S) (F : Sheaf J A) : Limits.IsLimit (E.multifork F.obj)

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.

def CategoryTheory.GrothendieckTopology.OneHypercover.toZeroHypercover {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} (E : J.OneHypercover S) : J.toPrecoverage.ZeroHypercover S

Forget the 1-components of a OneHypercover.

Equations

• E.toZeroHypercover = { toPreZeroHypercover := E.toPreZeroHypercover, mem₀ := ⋯ }

@[simp]

theorem CategoryTheory.GrothendieckTopology.OneHypercover.toZeroHypercover_toPreZeroHypercover {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} (E : J.OneHypercover S) : E.toZeroHypercover.toPreZeroHypercover = E.toPreZeroHypercover

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

The trivial 1-hypercover of S where a single component S.

Equations

• CategoryTheory.GrothendieckTopology.OneHypercover.trivial J S = { toPreOneHypercover := CategoryTheory.PreOneHypercover.trivial S, mem₀ := ⋯, mem₁ := ⋯ }

@[simp]

theorem CategoryTheory.GrothendieckTopology.OneHypercover.trivial_toPreOneHypercover {C : Type u} [Category.{v, u} C] (J : GrothendieckTopology C) (S : C) : (trivial J S).toPreOneHypercover = PreOneHypercover.trivial S

instance CategoryTheory.GrothendieckTopology.OneHypercover.instNonempty {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} (S : C) : Nonempty (J.OneHypercover S)

noncomputable def CategoryTheory.GrothendieckTopology.OneHypercover.inter {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} [Limits.HasPullbacks C] (E : J.OneHypercover S) (F : J.OneHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), Limits.HasPullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryStruct.comp (F.p₁ l) (F.f a))] : J.OneHypercover S

Intersection of two 1-hypercovers.

Equations

• E.inter F = { toPreOneHypercover := E.inter F.toPreOneHypercover, mem₀ := ⋯, mem₁ := ⋯ }

@[simp]

theorem CategoryTheory.GrothendieckTopology.OneHypercover.inter_toPreOneHypercover {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} [Limits.HasPullbacks C] (E : J.OneHypercover S) (F : J.OneHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b), Limits.HasPullback (CategoryStruct.comp (E.p₁ k) (E.f i)) (CategoryStruct.comp (F.p₁ l) (F.f a))] : (E.inter F).toPreOneHypercover = E.inter F.toPreOneHypercover

@[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

@[implicit_reducible]

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

Equations

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

@[simp]

theorem CategoryTheory.GrothendieckTopology.OneHypercover.comp_h₀ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} {X✝ Y✝ Z✝ : J.OneHypercover 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))

@[simp]

theorem CategoryTheory.GrothendieckTopology.OneHypercover.comp_h₁ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} {X✝ Y✝ Z✝ : J.OneHypercover 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.GrothendieckTopology.OneHypercover.id_s₁ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} (E : J.OneHypercover S) {i✝ j✝ : E.I₀} (a : E.I₁ i✝ j✝) : (CategoryStruct.id E).s₁ a = a

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.GrothendieckTopology.OneHypercover.comp_s₀ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} {X✝ Y✝ Z✝ : J.OneHypercover 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.GrothendieckTopology.OneHypercover.comp_s₁ {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} {X✝ Y✝ Z✝ : J.OneHypercover 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✝)

def CategoryTheory.GrothendieckTopology.OneHypercover.isoMk {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} {E F : J.OneHypercover S} (f : E.toPreOneHypercover ≅ F.toPreOneHypercover) : E ≅ F

An isomorphism of 1-hypercovers is an isomorphism of pre-1-hypercovers.

Equations

• CategoryTheory.GrothendieckTopology.OneHypercover.isoMk f = { hom := f.hom, inv := f.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.GrothendieckTopology.OneHypercover.isoMk_hom {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} {E F : J.OneHypercover S} (f : E.toPreOneHypercover ≅ F.toPreOneHypercover) : (isoMk f).hom = f.hom

@[simp]

theorem CategoryTheory.GrothendieckTopology.OneHypercover.isoMk_inv {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} {S : C} {E F : J.OneHypercover S} (f : E.toPreOneHypercover ≅ F.toPreOneHypercover) : (isoMk f).inv = f.inv

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_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_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_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_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_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_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

theorem CategoryTheory.PreZeroHypercover.ext_of_isSeparatedFor {C : Type u} [Category.{v, u} C] {P : Functor Cᵒᵖ (Type u_2)} {S : C} (E : PreZeroHypercover S) (h : Presieve.IsSeparatedFor P E.presieve₀) {x y : P.obj (Opposite.op S)} (hi : ∀ (i : E.I₀), P.map (E.f i).op x = P.map (E.f i).op y) : x = y

noncomputable def CategoryTheory.PreZeroHypercover.toPreOneHypercover {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) [E.HasPullbacks] : PreOneHypercover S

If the pairwise pullbacks exist, this is the pre-1-hypercover where the covers by the pullbacks are given by the pullbacks themselves.

Equations

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

@[simp]

theorem CategoryTheory.PreZeroHypercover.toPreOneHypercover_I₁ {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) [E.HasPullbacks] (x✝ x✝¹ : E.I₀) : E.toPreOneHypercover.I₁ x✝ x✝¹ = PUnit.{u_2 + 1}

@[simp]

theorem CategoryTheory.PreZeroHypercover.toPreOneHypercover_toPreZeroHypercover {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) [E.HasPullbacks] : E.toPreOneHypercover.toPreZeroHypercover = E

@[simp]

theorem CategoryTheory.PreZeroHypercover.toPreOneHypercover_p₂ {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) [E.HasPullbacks] (x✝ x✝¹ : E.I₀) (x✝² : PUnit.{u_2 + 1}) : E.toPreOneHypercover.p₂ x✝² = Limits.pullback.snd (E.f x✝) (E.f x✝¹)

@[simp]

theorem CategoryTheory.PreZeroHypercover.toPreOneHypercover_p₁ {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) [E.HasPullbacks] (x✝ x✝¹ : E.I₀) (x✝² : PUnit.{u_2 + 1}) : E.toPreOneHypercover.p₁ x✝² = Limits.pullback.fst (E.f x✝) (E.f x✝¹)

@[simp]

theorem CategoryTheory.PreZeroHypercover.toPreOneHypercover_Y {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) [E.HasPullbacks] (i j : E.I₀) (x✝ : PUnit.{u_2 + 1}) : E.toPreOneHypercover.Y x✝ = Limits.pullback (E.f i) (E.f j)

instance CategoryTheory.instHasPullbacksToPreOneHypercover {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) [E.HasPullbacks] : E.toPreOneHypercover.HasPullbacks

@[simp]

theorem CategoryTheory.sieve₁'_toPreOneHypercover_eq_top {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) [E.HasPullbacks] (i j : E.I₀) : E.toPreOneHypercover.sieve₁' i j = ⊤

noncomputable def CategoryTheory.Precoverage.ZeroHypercover.toOneHypercover {C : Type u} [Category.{v, u} C] {J : Precoverage C} {S : C} (E : J.ZeroHypercover S) [E.HasPullbacks] : J.toGrothendieck.OneHypercover S

If the pairwise pullbacks exist, this is the pre-1-hypercover where the covers by the pullbacks are given by the pullbacks themselves.

Equations

• E.toOneHypercover = CategoryTheory.GrothendieckTopology.OneHypercover.mk' E.toPreOneHypercover ⋯ ⋯

@[simp]

theorem CategoryTheory.Precoverage.ZeroHypercover.toOneHypercover_toPreOneHypercover {C : Type u} [Category.{v, u} C] {J : Precoverage C} {S : C} (E : J.ZeroHypercover S) [E.HasPullbacks] : E.toOneHypercover.toPreOneHypercover = E.toPreOneHypercover

noncomputable def CategoryTheory.PreZeroHypercover.refineOneHypercover {C : Type u} [Category.{v, u} C] {X : C} (E : PreZeroHypercover X) [E.HasPullbacks] (F : (i j : E.I₀) → PreZeroHypercover (Limits.pullback (E.f i) (E.f j))) : PreOneHypercover X

Refine a pre-0-hypercover by 0-hypercovers of the pairwise pullbacks.

Equations

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

@[simp]

theorem CategoryTheory.PreZeroHypercover.refineOneHypercover_p₁ {C : Type u} [Category.{v, u} C] {X : C} (E : PreZeroHypercover X) [E.HasPullbacks] (F : (i j : E.I₀) → PreZeroHypercover (Limits.pullback (E.f i) (E.f j))) (i j : E.I₀) (k : (F i j).I₀) : (E.refineOneHypercover F).p₁ k = CategoryStruct.comp ((F i j).f k) (Limits.pullback.fst (E.f i) (E.f j))

@[simp]

theorem CategoryTheory.PreZeroHypercover.refineOneHypercover_Y {C : Type u} [Category.{v, u} C] {X : C} (E : PreZeroHypercover X) [E.HasPullbacks] (F : (i j : E.I₀) → PreZeroHypercover (Limits.pullback (E.f i) (E.f j))) (i j : E.I₀) (k : (F i j).I₀) : (E.refineOneHypercover F).Y k = (F i j).X k

@[simp]

theorem CategoryTheory.PreZeroHypercover.refineOneHypercover_p₂ {C : Type u} [Category.{v, u} C] {X : C} (E : PreZeroHypercover X) [E.HasPullbacks] (F : (i j : E.I₀) → PreZeroHypercover (Limits.pullback (E.f i) (E.f j))) (i j : E.I₀) (k : (F i j).I₀) : (E.refineOneHypercover F).p₂ k = CategoryStruct.comp ((F i j).f k) (Limits.pullback.snd (E.f i) (E.f j))

@[simp]

theorem CategoryTheory.PreZeroHypercover.refineOneHypercover_toPreZeroHypercover {C : Type u} [Category.{v, u} C] {X : C} (E : PreZeroHypercover X) [E.HasPullbacks] (F : (i j : E.I₀) → PreZeroHypercover (Limits.pullback (E.f i) (E.f j))) : (E.refineOneHypercover F).toPreZeroHypercover = E

@[simp]

theorem CategoryTheory.PreZeroHypercover.refineOneHypercover_I₁ {C : Type u} [Category.{v, u} C] {X : C} (E : PreZeroHypercover X) [E.HasPullbacks] (F : (i j : E.I₀) → PreZeroHypercover (Limits.pullback (E.f i) (E.f j))) (i j : E.I₀) : (E.refineOneHypercover F).I₁ i j = (F i j).I₀

instance CategoryTheory.instHasPullbacksRefineOneHypercover {C : Type u} [Category.{v, u} C] {X : C} (E : PreZeroHypercover X) [E.HasPullbacks] (F : (i j : E.I₀) → PreZeroHypercover (Limits.pullback (E.f i) (E.f j))) : (E.refineOneHypercover F).HasPullbacks

@[simp]

theorem CategoryTheory.PreZeroHypercover.sieve₁'_refineOneHypercover {C : Type u} [Category.{v, u} C] {X : C} (E : PreZeroHypercover X) [E.HasPullbacks] (F : (i j : E.I₀) → PreZeroHypercover (Limits.pullback (E.f i) (E.f j))) (i j : E.I₀) : (E.refineOneHypercover F).sieve₁' i j = (F i j).sieve₀