0-hypercovers

Given a coverage J on a category C, we define the type of 0-hypercovers of an object S : C. They consist of a covering family of morphisms X i ⟶ S indexed by a type I₀ such that the induced presieve is in J.

We define this with respect to a coverage and not to a Grothendieck topology, because this yields more control over the components of the cover.

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

The categorical data that is involved in a 0-hypercover of an object S. This consists of a family of morphisms f i : X i ⟶ S for i : I₀.

• 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

theorem CategoryTheory.PreZeroHypercover.ext {C : Type u} {inst✝ : Category.{v, u} C} {S : C} {x y : PreZeroHypercover S} (I₀ : x.I₀ = y.I₀) (X : x.X ≍ y.X) (f : x.f ≍ y.f) : x = y

theorem CategoryTheory.PreZeroHypercover.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {S : C} {x y : PreZeroHypercover S} : x = y ↔ x.I₀ = y.I₀ ∧ x.X ≍ y.X ∧ x.f ≍ y.f

@[reducible, inline]

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

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

@[reducible, inline]

abbrev CategoryTheory.PreZeroHypercover.presieve₀ {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) : Presieve S

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

@[simp]

theorem CategoryTheory.PreZeroHypercover.presieve₀_f {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) (i : E.I₀) : E.presieve₀ (E.f i)

@[reducible, inline]

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

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

theorem CategoryTheory.PreZeroHypercover.sieve₀_f {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) (i : E.I₀) : E.sieve₀.arrows (E.f i)

def CategoryTheory.PreZeroHypercover.singleton {C : Type u} [Category.{v, u} C] {S T : C} (f : S ⟶ T) : PreZeroHypercover T

The pre-0-hypercover defined by a single morphism.

@[simp]

theorem CategoryTheory.PreZeroHypercover.singleton_I₀ {C : Type u} [Category.{v, u} C] {S T : C} (f : S ⟶ T) : (singleton f).I₀ = PUnit.{w + 1}

@[simp]

theorem CategoryTheory.PreZeroHypercover.singleton_f {C : Type u} [Category.{v, u} C] {S T : C} (f : S ⟶ T) (x✝ : PUnit.{w + 1}) : (singleton f).f x✝ = f

@[simp]

theorem CategoryTheory.PreZeroHypercover.singleton_X {C : Type u} [Category.{v, u} C] {S T : C} (f : S ⟶ T) (x✝ : PUnit.{w + 1}) : (singleton f).X x✝ = S

@[simp]

theorem CategoryTheory.PreZeroHypercover.presieve₀_singleton {C : Type u} [Category.{v, u} C] {S T : C} (f : S ⟶ T) : (singleton f).presieve₀ = Presieve.singleton f

instance CategoryTheory.PreZeroHypercover.instUniqueI₀Singleton {C : Type u} [Category.{v, u} C] {S T : C} (f : S ⟶ T) : Unique (singleton f).I₀

noncomputable def CategoryTheory.PreZeroHypercover.pullback₁ {C : Type u} [Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : PreZeroHypercover T) [∀ (i : E.I₀), Limits.HasPullback f (E.f i)] : PreZeroHypercover S

Pullback of a pre-0-hypercover along a morphism. The components are pullback f (E.f i).

@[simp]

theorem CategoryTheory.PreZeroHypercover.pullback₁_I₀ {C : Type u} [Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : PreZeroHypercover T) [∀ (i : E.I₀), Limits.HasPullback f (E.f i)] : (pullback₁ f E).I₀ = E.I₀

@[simp]

theorem CategoryTheory.PreZeroHypercover.pullback₁_f {C : Type u} [Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : PreZeroHypercover T) [∀ (i : E.I₀), Limits.HasPullback f (E.f i)] (x✝ : E.I₀) : (pullback₁ f E).f x✝ = Limits.pullback.fst f (E.f x✝)

@[simp]

theorem CategoryTheory.PreZeroHypercover.pullback₁_X {C : Type u} [Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : PreZeroHypercover T) [∀ (i : E.I₀), Limits.HasPullback f (E.f i)] (i : E.I₀) : (pullback₁ f E).X i = Limits.pullback f (E.f i)

noncomputable def CategoryTheory.PreZeroHypercover.pullback₂ {C : Type u} [Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : PreZeroHypercover T) [∀ (i : E.I₀), Limits.HasPullback (E.f i) f] : PreZeroHypercover S

Pullback of a pre-0-hypercover along a morphism. The components are pullback (E.f i) f.

@[simp]

theorem CategoryTheory.PreZeroHypercover.pullback₂_f {C : Type u} [Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : PreZeroHypercover T) [∀ (i : E.I₀), Limits.HasPullback (E.f i) f] (x✝ : E.I₀) : (pullback₂ f E).f x✝ = Limits.pullback.snd (E.f x✝) f

@[simp]

theorem CategoryTheory.PreZeroHypercover.pullback₂_X {C : Type u} [Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : PreZeroHypercover T) [∀ (i : E.I₀), Limits.HasPullback (E.f i) f] (i : E.I₀) : (pullback₂ f E).X i = Limits.pullback (E.f i) f

@[simp]

theorem CategoryTheory.PreZeroHypercover.pullback₂_I₀ {C : Type u} [Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : PreZeroHypercover T) [∀ (i : E.I₀), Limits.HasPullback (E.f i) f] : (pullback₂ f E).I₀ = E.I₀

theorem CategoryTheory.PreZeroHypercover.presieve₀_pullback₁ {C : Type u} [Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : PreZeroHypercover T) [∀ (i : E.I₀), Limits.HasPullback (E.f i) f] : (pullback₂ f E).presieve₀ = Presieve.pullbackArrows f E.presieve₀

noncomputable def CategoryTheory.PreZeroHypercover.pullbackCoverOfLeft {C : Type u} [Category.{v, u} C] {X : C} (E : PreZeroHypercover X) {Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [Limits.HasPullback f g] [∀ (i : E.I₀), Limits.HasPullback (CategoryStruct.comp (E.f i) f) g] : PreZeroHypercover (Limits.pullback f g)

If {Uᵢ} covers X, this is the pre-0-hypercover of X ×[Z] Y given by {Uᵢ ×[Z] Y}.

@[simp]

theorem CategoryTheory.PreZeroHypercover.pullbackCoverOfLeft_f {C : Type u} [Category.{v, u} C] {X : C} (E : PreZeroHypercover X) {Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [Limits.HasPullback f g] [∀ (i : E.I₀), Limits.HasPullback (CategoryStruct.comp (E.f i) f) g] (i : E.I₀) : (E.pullbackCoverOfLeft f g).f i = Limits.pullback.map (CategoryStruct.comp (E.f i) f) g f g (E.f i) (CategoryStruct.id Y) (CategoryStruct.id Z) ⋯ ⋯

@[simp]

theorem CategoryTheory.PreZeroHypercover.pullbackCoverOfLeft_I₀ {C : Type u} [Category.{v, u} C] {X : C} (E : PreZeroHypercover X) {Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [Limits.HasPullback f g] [∀ (i : E.I₀), Limits.HasPullback (CategoryStruct.comp (E.f i) f) g] : (E.pullbackCoverOfLeft f g).I₀ = E.I₀

@[simp]

theorem CategoryTheory.PreZeroHypercover.pullbackCoverOfLeft_X {C : Type u} [Category.{v, u} C] {X : C} (E : PreZeroHypercover X) {Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [Limits.HasPullback f g] [∀ (i : E.I₀), Limits.HasPullback (CategoryStruct.comp (E.f i) f) g] (i : E.I₀) : (E.pullbackCoverOfLeft f g).X i = Limits.pullback (CategoryStruct.comp (E.f i) f) g

noncomputable def CategoryTheory.PreZeroHypercover.pullbackCoverOfRight {C : Type u} [Category.{v, u} C] {Y : C} (E : PreZeroHypercover Y) {X Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [Limits.HasPullback f g] [∀ (i : E.I₀), Limits.HasPullback f (CategoryStruct.comp (E.f i) g)] : PreZeroHypercover (Limits.pullback f g)

If {Uᵢ} covers Y, this is the pre-0-hypercover of X ×[Z] Y given by {X ×[Z] Uᵢ}.

@[simp]

theorem CategoryTheory.PreZeroHypercover.pullbackCoverOfRight_I₀ {C : Type u} [Category.{v, u} C] {Y : C} (E : PreZeroHypercover Y) {X Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [Limits.HasPullback f g] [∀ (i : E.I₀), Limits.HasPullback f (CategoryStruct.comp (E.f i) g)] : (E.pullbackCoverOfRight f g).I₀ = E.I₀

@[simp]

theorem CategoryTheory.PreZeroHypercover.pullbackCoverOfRight_X {C : Type u} [Category.{v, u} C] {Y : C} (E : PreZeroHypercover Y) {X Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [Limits.HasPullback f g] [∀ (i : E.I₀), Limits.HasPullback f (CategoryStruct.comp (E.f i) g)] (i : E.I₀) : (E.pullbackCoverOfRight f g).X i = Limits.pullback f (CategoryStruct.comp (E.f i) g)

@[simp]

theorem CategoryTheory.PreZeroHypercover.pullbackCoverOfRight_f {C : Type u} [Category.{v, u} C] {Y : C} (E : PreZeroHypercover Y) {X Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [Limits.HasPullback f g] [∀ (i : E.I₀), Limits.HasPullback f (CategoryStruct.comp (E.f i) g)] (i : E.I₀) : (E.pullbackCoverOfRight f g).f i = Limits.pullback.map f (CategoryStruct.comp (E.f i) g) f g (CategoryStruct.id X) (E.f i) (CategoryStruct.id Z) ⋯ ⋯

def CategoryTheory.PreZeroHypercover.bind {C : Type u} [Category.{v, u} C] {T : C} (E : PreZeroHypercover T) (F : (i : E.I₀) → PreZeroHypercover (E.X i)) : PreZeroHypercover T

Refining each component of a pre-0-hypercover yields a refined pre-0-hypercover of the base.

@[simp]

theorem CategoryTheory.PreZeroHypercover.bind_X {C : Type u} [Category.{v, u} C] {T : C} (E : PreZeroHypercover T) (F : (i : E.I₀) → PreZeroHypercover (E.X i)) (ij : (i : E.I₀) × (F i).I₀) : (E.bind F).X ij = (F ij.fst).X ij.snd

@[simp]

theorem CategoryTheory.PreZeroHypercover.bind_I₀ {C : Type u} [Category.{v, u} C] {T : C} (E : PreZeroHypercover T) (F : (i : E.I₀) → PreZeroHypercover (E.X i)) : (E.bind F).I₀ = ((i : E.I₀) × (F i).I₀)

@[simp]

theorem CategoryTheory.PreZeroHypercover.bind_f {C : Type u} [Category.{v, u} C] {T : C} (E : PreZeroHypercover T) (F : (i : E.I₀) → PreZeroHypercover (E.X i)) (ij : (i : E.I₀) × (F i).I₀) : (E.bind F).f ij = CategoryStruct.comp ((F ij.fst).f ij.snd) (E.f ij.fst)

def CategoryTheory.PreZeroHypercover.restrictIndex {C : Type u} [Category.{v, u} C] {T : C} (E : PreZeroHypercover T) {ι : Type w'} (f : ι → E.I₀) : PreZeroHypercover T

Restrict the indexing type to ι by precomposing with a function ι → E.I₀.

@[simp]

theorem CategoryTheory.PreZeroHypercover.restrictIndex_X {C : Type u} [Category.{v, u} C] {T : C} (E : PreZeroHypercover T) {ι : Type w'} (f : ι → E.I₀) (a✝ : ι) : (E.restrictIndex f).X a✝ = (E.X ∘ f) a✝

@[simp]

theorem CategoryTheory.PreZeroHypercover.restrictIndex_f {C : Type u} [Category.{v, u} C] {T : C} (E : PreZeroHypercover T) {ι : Type w'} (f : ι → E.I₀) (i : ι) : (E.restrictIndex f).f i = E.f (f i)

@[simp]

theorem CategoryTheory.PreZeroHypercover.restrictIndex_I₀ {C : Type u} [Category.{v, u} C] {T : C} (E : PreZeroHypercover T) {ι : Type w'} (f : ι → E.I₀) : (E.restrictIndex f).I₀ = ι

@[simp]

theorem CategoryTheory.PreZeroHypercover.presieve₀_restrictIndex_equiv {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) {ι : Type w'} (e : ι ≃ E.I₀) : (E.restrictIndex ⇑e).presieve₀ = E.presieve₀

@[simp]

theorem CategoryTheory.PreZeroHypercover.presieve₀_restrictIndex_le {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) {ι : Type u_1} (f : ι → E.I₀) : (E.restrictIndex f).presieve₀ ≤ E.presieve₀

def CategoryTheory.PreZeroHypercover.reindex {C : Type u} [Category.{v, u} C] {T : C} (E : PreZeroHypercover T) {ι : Type w'} (e : ι ≃ E.I₀) : PreZeroHypercover T

Replace the indexing type of a pre-0-hypercover.

@[simp]

theorem CategoryTheory.PreZeroHypercover.reindex_X {C : Type u} [Category.{v, u} C] {T : C} (E : PreZeroHypercover T) {ι : Type w'} (e : ι ≃ E.I₀) (a✝ : ι) : (E.reindex e).X a✝ = E.X (e a✝)

@[simp]

theorem CategoryTheory.PreZeroHypercover.reindex_f {C : Type u} [Category.{v, u} C] {T : C} (E : PreZeroHypercover T) {ι : Type w'} (e : ι ≃ E.I₀) (i : ι) : (E.reindex e).f i = E.f (e i)

@[simp]

theorem CategoryTheory.PreZeroHypercover.reindex_I₀ {C : Type u} [Category.{v, u} C] {T : C} (E : PreZeroHypercover T) {ι : Type w'} (e : ι ≃ E.I₀) : (E.reindex e).I₀ = ι

@[simp]

theorem CategoryTheory.PreZeroHypercover.presieve₀_reindex {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) {ι : Type w'} (e : ι ≃ E.I₀) : (E.reindex e).presieve₀ = E.presieve₀

noncomputable def CategoryTheory.PreZeroHypercover.inter {C : Type u} [Category.{v, u} C] {T : C} (E : PreZeroHypercover T) (F : PreZeroHypercover T) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] : PreZeroHypercover T

Pairwise intersection of two pre-0-hypercovers.

@[simp]

theorem CategoryTheory.PreZeroHypercover.inter_X {C : Type u} [Category.{v, u} C] {T : C} (E : PreZeroHypercover T) (F : PreZeroHypercover T) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] (a✝ : E.I₀ × F.1) : (E.inter F).X a✝ = Limits.pullback (E.f a✝.1) (F.f a✝.2)

@[simp]

theorem CategoryTheory.PreZeroHypercover.inter_f {C : Type u} [Category.{v, u} C] {T : C} (E : PreZeroHypercover T) (F : PreZeroHypercover T) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] (i : E.I₀ × F.1) : (E.inter F).f i = CategoryStruct.comp (Limits.pullback.fst (E.f i.1) (F.f i.2)) (E.f i.1)

@[simp]

theorem CategoryTheory.PreZeroHypercover.inter_I₀ {C : Type u} [Category.{v, u} C] {T : C} (E : PreZeroHypercover T) (F : PreZeroHypercover T) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] : (E.inter F).I₀ = (E.I₀ × F.1)

theorem CategoryTheory.PreZeroHypercover.inter_def {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) (F : PreZeroHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] : E.inter F = (E.bind fun (i : E.I₀) => pullback₁ (E.f i) F).reindex (Equiv.sigmaEquivProd E.I₀ F.1).symm

def CategoryTheory.PreZeroHypercover.sum {C : Type u} [Category.{v, u} C] {X : C} (E : PreZeroHypercover X) (F : PreZeroHypercover X) : PreZeroHypercover X

Disjoint union of two pre-0-hypercovers.

@[simp]

theorem CategoryTheory.PreZeroHypercover.sum_I₀ {C : Type u} [Category.{v, u} C] {X : C} (E : PreZeroHypercover X) (F : PreZeroHypercover X) : (E.sum F).I₀ = (E.I₀ ⊕ F.I₀)

theorem CategoryTheory.PreZeroHypercover.sum_f {C : Type u} [Category.{v, u} C] {X : C} (E : PreZeroHypercover X) (F : PreZeroHypercover X) (x✝ : E.I₀ ⊕ F.I₀) : (E.sum F).f x✝ = match x✝ with | Sum.inl i => E.f i | Sum.inr i => F.f i

theorem CategoryTheory.PreZeroHypercover.sum_X {C : Type u} [Category.{v, u} C] {X : C} (E : PreZeroHypercover X) (F : PreZeroHypercover X) (a✝ : E.I₀ ⊕ F.I₀) : (E.sum F).X a✝ = Sum.elim E.X F.X a✝

@[simp]

theorem CategoryTheory.PreZeroHypercover.sum_X_inl {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) (F : PreZeroHypercover S) (i : E.I₀) : (E.sum F).X (Sum.inl i) = E.X i

@[simp]

theorem CategoryTheory.PreZeroHypercover.sum_X_inr {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) (F : PreZeroHypercover S) (i : F.I₀) : (E.sum F).X (Sum.inr i) = F.X i

@[simp]

theorem CategoryTheory.PreZeroHypercover.sum_f_inl {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) (F : PreZeroHypercover S) (i : E.I₀) : (E.sum F).f (Sum.inl i) = E.f i

@[simp]

theorem CategoryTheory.PreZeroHypercover.sum_f_inr {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) (F : PreZeroHypercover S) (i : F.I₀) : (E.sum F).f (Sum.inr i) = F.f i

@[simp]

theorem CategoryTheory.PreZeroHypercover.presieve₀_sum {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) (F : PreZeroHypercover S) : (E.sum F).presieve₀ = E.presieve₀ ⊔ F.presieve₀

def CategoryTheory.PreZeroHypercover.add {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) {T : C} (f : T ⟶ S) : PreZeroHypercover S

Add a morphism to a pre-0-hypercover.

@[simp]

theorem CategoryTheory.PreZeroHypercover.add_I₀ {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) {T : C} (f : T ⟶ S) : (E.add f).I₀ = Option E.I₀

@[simp]

theorem CategoryTheory.PreZeroHypercover.add_X_some {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) {T : C} (f : T ⟶ S) (i : E.I₀) : (E.add f).X (some i) = E.X i

@[simp]

theorem CategoryTheory.PreZeroHypercover.add_X_none {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) {T : C} (f : T ⟶ S) : (E.add f).X none = T

@[simp]

theorem CategoryTheory.PreZeroHypercover.add_f_some {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) {T : C} (f : T ⟶ S) (i : E.I₀) : (E.add f).f (some i) = E.f i

@[simp]

theorem CategoryTheory.PreZeroHypercover.add_f_nome {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) {T : C} (f : T ⟶ S) : (E.add f).f none = f

@[simp]

theorem CategoryTheory.PreZeroHypercover.presieve₀_add {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) {T : C} (f : T ⟶ S) : (E.add f).presieve₀ = E.presieve₀ ⊔ Presieve.singleton f

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

The single object pre-0-hypercover obtained from taking the coproduct of the components.

@[simp]

theorem CategoryTheory.PreZeroHypercover.sigmaOfIsColimit_X {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) {c : Limits.Cofan E.X} (hc : Limits.IsColimit c) (x✝ : PUnit.{w + 1}) : (E.sigmaOfIsColimit hc).X x✝ = c.pt

@[simp]

theorem CategoryTheory.PreZeroHypercover.sigmaOfIsColimit_I₀ {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) {c : Limits.Cofan E.X} (hc : Limits.IsColimit c) : (E.sigmaOfIsColimit hc).I₀ = PUnit.{w + 1}

@[simp]

theorem CategoryTheory.PreZeroHypercover.inj_sigmaOfIsColimit_f {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) {c : Limits.Cofan E.X} (hc : Limits.IsColimit c) (i : E.I₀) (r : PUnit.{w + 1}) : CategoryStruct.comp (c.inj i) ((E.sigmaOfIsColimit hc).f r) = E.f i

@[simp]

theorem CategoryTheory.PreZeroHypercover.inj_sigmaOfIsColimit_f_assoc {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) {c : Limits.Cofan E.X} (hc : Limits.IsColimit c) (i : E.I₀) (r : PUnit.{w + 1}) {Z : C} (h : S ⟶ Z) : CategoryStruct.comp (c.inj i) (CategoryStruct.comp ((E.sigmaOfIsColimit hc).f r) h) = CategoryStruct.comp (E.f i) h

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

A morphism of pre-0-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

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

  The refinement morphisms between objects in the coverings of S.

• w₀ (i : E.I₀) : CategoryStruct.comp (self.h₀ i) (F.f (self.s₀ i)) = E.f i

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

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

@[simp]

theorem CategoryTheory.PreZeroHypercover.Hom.w₀_assoc {C : Type u} [Category.{v, u} C] {S : C} {E : PreZeroHypercover S} {F : PreZeroHypercover 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

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

The identity refinement of a pre-0-hypercover.

@[simp]

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

@[simp]

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

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

Composition of refinement morphisms of pre-0-hypercovers.

@[simp]

theorem CategoryTheory.PreZeroHypercover.Hom.comp_h₀ {C : Type u} [Category.{v, u} C] {S : C} {E : PreZeroHypercover S} {F : PreZeroHypercover S} {G : PreZeroHypercover 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.PreZeroHypercover.Hom.comp_s₀ {C : Type u} [Category.{v, u} C] {S : C} {E : PreZeroHypercover S} {F : PreZeroHypercover S} {G : PreZeroHypercover S} (f : E.Hom F) (g : F.Hom G) (a✝ : E.I₀) : (f.comp g).s₀ a✝ = (g.s₀ ∘ f.s₀) a✝

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

@[simp]

theorem CategoryTheory.PreZeroHypercover.comp_h₀ {C : Type u} [Category.{v, u} C] {S : C} {X✝ Y✝ Z✝ : PreZeroHypercover 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.PreZeroHypercover.id_h₀ {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) (x✝ : E.I₀) : (CategoryStruct.id E).h₀ x✝ = CategoryStruct.id (E.X x✝)

@[simp]

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

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

theorem CategoryTheory.PreZeroHypercover.Hom.ext'_iff {C : Type u} [Category.{v, u} C] {S : C} {E : PreZeroHypercover S} {F : PreZeroHypercover 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 ⋯)

def CategoryTheory.PreZeroHypercover.isoMk {C : Type u} [Category.{v, u} C] {S : C} {E F : PreZeroHypercover S} (s₀ : E.I₀ ≃ F.I₀) (h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)) (w₀ : ∀ (i : E.I₀), CategoryStruct.comp (h₀ i).hom (F.f (s₀ i)) = E.f i := by cat_disch) : E ≅ F

Constructor for isomorphisms of pre-0-hypercovers.

@[simp]

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

@[simp]

theorem CategoryTheory.PreZeroHypercover.isoMk_hom_h₀ {C : Type u} [Category.{v, u} C] {S : C} {E F : PreZeroHypercover S} (s₀ : E.I₀ ≃ F.I₀) (h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)) (w₀ : ∀ (i : E.I₀), CategoryStruct.comp (h₀ i).hom (F.f (s₀ i)) = E.f i := by cat_disch) (i : E.I₀) : (isoMk s₀ h₀ w₀).hom.h₀ i = (h₀ i).hom

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.PreZeroHypercover.hom_inv_h₀_assoc {C : Type u} [Category.{v, u} C] {S : C} {E F : PreZeroHypercover 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.PreZeroHypercover.inv_hom_h₀ {C : Type u} [Category.{v, u} C] {S : C} {E F : PreZeroHypercover S} (e : E ≅ F) (i : F.I₀) : CategoryStruct.comp (e.inv.h₀ i) (e.hom.h₀ (e.inv.s₀ i)) = eqToHom ⋯

@[simp]

theorem CategoryTheory.PreZeroHypercover.inv_hom_h₀_assoc {C : Type u} [Category.{v, u} C] {S : C} {E F : PreZeroHypercover 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

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.PreZeroHypercover.inv_inv_h₀_comp_f {C : Type u} [Category.{v, u} C] {S : C} {E F : PreZeroHypercover S} (e : E ≅ F) (i : F.I₀) : CategoryStruct.comp (inv (e.inv.h₀ i)) (F.f i) = E.f (e.inv.s₀ i)

@[simp]

theorem CategoryTheory.PreZeroHypercover.inv_inv_h₀_comp_f_assoc {C : Type u} [Category.{v, u} C] {S : C} {E F : PreZeroHypercover S} (e : E ≅ F) (i : F.I₀) {Z : C} (h : S ⟶ Z) : CategoryStruct.comp (inv (e.inv.h₀ i)) (CategoryStruct.comp (F.f i) h) = CategoryStruct.comp (E.f (e.inv.s₀ i)) h

theorem CategoryTheory.PreZeroHypercover.Hom.sieve₀_le_sieve₀ {C : Type u} [Category.{v, u} C] {S : C} {E : PreZeroHypercover S} {F : PreZeroHypercover S} (f : E.Hom F) : E.sieve₀ ≤ F.sieve₀

theorem CategoryTheory.PreZeroHypercover.sieve₀_eq_of_iso {C : Type u} [Category.{v, u} C] {S : C} {E F : PreZeroHypercover S} (e : E ≅ F) : E.sieve₀ = F.sieve₀

def CategoryTheory.PreZeroHypercover.map {C : Type u} [Category.{v, u} C] {S : C} {D : Type u_1} [Category.{v_1, u_1} D] (F : Functor C D) (E : PreZeroHypercover S) : PreZeroHypercover (F.obj S)

The image of a pre-0-hypercover under a functor.

@[simp]

theorem CategoryTheory.PreZeroHypercover.map_f {C : Type u} [Category.{v, u} C] {S : C} {D : Type u_1} [Category.{v_1, u_1} D] (F : Functor C D) (E : PreZeroHypercover S) (i : E.I₀) : (map F E).f i = F.map (E.f i)

@[simp]

theorem CategoryTheory.PreZeroHypercover.map_I₀ {C : Type u} [Category.{v, u} C] {S : C} {D : Type u_1} [Category.{v_1, u_1} D] (F : Functor C D) (E : PreZeroHypercover S) : (map F E).I₀ = E.I₀

@[simp]

theorem CategoryTheory.PreZeroHypercover.map_X {C : Type u} [Category.{v, u} C] {S : C} {D : Type u_1} [Category.{v_1, u_1} D] (F : Functor C D) (E : PreZeroHypercover S) (i : E.I₀) : (map F E).X i = F.obj (E.X i)

theorem CategoryTheory.PreZeroHypercover.presieve₀_map {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) {D : Type u_1} [Category.{v_1, u_1} D] {F : Functor C D} : (map F E).presieve₀ = Presieve.map F E.presieve₀

noncomputable def CategoryTheory.PreZeroHypercover.pullbackIso {C : Type u} [Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : PreZeroHypercover T) [∀ (i : E.I₀), Limits.HasPullback f (E.f i)] [∀ (i : E.I₀), Limits.HasPullback (E.f i) f] : pullback₁ f E ≅ pullback₂ f E

Pullback symmetry isomorphism.

@[simp]

theorem CategoryTheory.PreZeroHypercover.pullbackIso_hom_h₀ {C : Type u} [Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : PreZeroHypercover T) [∀ (i : E.I₀), Limits.HasPullback f (E.f i)] [∀ (i : E.I₀), Limits.HasPullback (E.f i) f] (i : (pullback₁ f E).I₀) : (pullbackIso f E).hom.h₀ i = (Limits.pullbackSymmetry f (E.f i)).hom

@[simp]

theorem CategoryTheory.PreZeroHypercover.pullbackIso_inv_s₀ {C : Type u} [Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : PreZeroHypercover T) [∀ (i : E.I₀), Limits.HasPullback f (E.f i)] [∀ (i : E.I₀), Limits.HasPullback (E.f i) f] (a : (pullback₂ f E).I₀) : (pullbackIso f E).inv.s₀ a = id a

@[simp]

theorem CategoryTheory.PreZeroHypercover.pullbackIso_hom_s₀ {C : Type u} [Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : PreZeroHypercover T) [∀ (i : E.I₀), Limits.HasPullback f (E.f i)] [∀ (i : E.I₀), Limits.HasPullback (E.f i) f] (a : (pullback₁ f E).I₀) : (pullbackIso f E).hom.s₀ a = id a

@[simp]

theorem CategoryTheory.PreZeroHypercover.pullbackIso_inv_h₀ {C : Type u} [Category.{v, u} C] {S T : C} (f : S ⟶ T) (E : PreZeroHypercover T) [∀ (i : E.I₀), Limits.HasPullback f (E.f i)] [∀ (i : E.I₀), Limits.HasPullback (E.f i) f] (i : (pullback₂ f E).I₀) : (pullbackIso f E).inv.h₀ i = (Limits.pullbackSymmetry f (E.f i)).inv

def CategoryTheory.PreZeroHypercover.sumInl {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) (F : PreZeroHypercover S) : E.Hom (E.sum F)

The left inclusion into the disjoint union.

@[simp]

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

@[simp]

theorem CategoryTheory.PreZeroHypercover.sumInl_s₀ {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) (F : PreZeroHypercover S) (val : E.I₀) : (E.sumInl F).s₀ val = Sum.inl val

def CategoryTheory.PreZeroHypercover.sumInr {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) (F : PreZeroHypercover S) : F.Hom (E.sum F)

The right inclusion into the disjoint union.

@[simp]

theorem CategoryTheory.PreZeroHypercover.sumInr_s₀ {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) (F : PreZeroHypercover S) (val : F.I₀) : (E.sumInr F).s₀ val = Sum.inr val

@[simp]

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

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

To give a refinement of the disjoint union, it suffices to give refinements of both components.

@[simp]

theorem CategoryTheory.PreZeroHypercover.sumLift_s₀ {C : Type u} [Category.{v, u} C] {S : C} {E : PreZeroHypercover S} {F : PreZeroHypercover S} {G : PreZeroHypercover S} (f : E.Hom G) (g : F.Hom G) (a✝ : E.I₀ ⊕ F.I₀) : (sumLift f g).s₀ a✝ = Sum.elim f.s₀ g.s₀ a✝

@[simp]

theorem CategoryTheory.PreZeroHypercover.sumLift_h₀ {C : Type u} [Category.{v, u} C] {S : C} {E : PreZeroHypercover S} {F : PreZeroHypercover S} {G : PreZeroHypercover S} (f : E.Hom G) (g : F.Hom G) (x✝ : (E.sum F).I₀) : (sumLift f g).h₀ x✝ = match x✝ with | Sum.inl i => f.h₀ i | Sum.inr i => g.h₀ i

noncomputable def CategoryTheory.PreZeroHypercover.interFst {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) (F : PreZeroHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] : (E.inter F).Hom E

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

@[simp]

theorem CategoryTheory.PreZeroHypercover.interFst_h₀ {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) (F : PreZeroHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] (x✝ : (E.inter F).I₀) : (E.interFst F).h₀ x✝ = Limits.pullback.fst (E.f ((Equiv.sigmaEquivProd E.I₀ F.1).symm x✝).fst) (F.f ((Equiv.sigmaEquivProd E.I₀ F.1).symm x✝).snd)

@[simp]

theorem CategoryTheory.PreZeroHypercover.interFst_s₀ {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) (F : PreZeroHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] (i : (E.inter F).I₀) : (E.interFst F).s₀ i = i.1

noncomputable def CategoryTheory.PreZeroHypercover.interSnd {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) (F : PreZeroHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] : (E.inter F).Hom F

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

@[simp]

theorem CategoryTheory.PreZeroHypercover.interSnd_s₀ {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) (F : PreZeroHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] (i : (E.inter F).I₀) : (E.interSnd F).s₀ i = i.2

@[simp]

theorem CategoryTheory.PreZeroHypercover.interSnd_h₀ {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) (F : PreZeroHypercover S) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] (x✝ : (E.inter F).I₀) : (E.interSnd F).h₀ x✝ = Limits.pullback.snd (E.f ((Equiv.sigmaEquivProd E.I₀ F.1).symm x✝).fst) (F.f ((Equiv.sigmaEquivProd E.I₀ F.1).symm x✝).snd)

noncomputable def CategoryTheory.PreZeroHypercover.interLift {C : Type u} [Category.{v, u} C] {S : C} {E : PreZeroHypercover S} {F : PreZeroHypercover S} {G : PreZeroHypercover S} [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] (f : G.Hom E) (g : G.Hom F) : G.Hom (E.inter F)

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

@[simp]

theorem CategoryTheory.PreZeroHypercover.interLift_s₀ {C : Type u} [Category.{v, u} C] {S : C} {E : PreZeroHypercover S} {F : PreZeroHypercover S} {G : PreZeroHypercover S} [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] (f : G.Hom E) (g : G.Hom F) (i : G.I₀) : (interLift f g).s₀ i = (f.s₀ i, g.s₀ i)

@[simp]

theorem CategoryTheory.PreZeroHypercover.interLift_h₀ {C : Type u} [Category.{v, u} C] {S : C} {E : PreZeroHypercover S} {F : PreZeroHypercover S} {G : PreZeroHypercover S} [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] (f : G.Hom E) (g : G.Hom F) (i : G.I₀) : (interLift f g).h₀ i = Limits.pullback.lift (f.h₀ i) (g.h₀ i) ⋯

def CategoryTheory.PreZeroHypercover.restrictIndexHom {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) {ι : Type w'} (f : ι → E.I₀) : (E.restrictIndex f).Hom E

The refinement given by restricting the indexing type.

@[simp]

theorem CategoryTheory.PreZeroHypercover.restrictIndexHom_h₀ {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) {ι : Type w'} (f : ι → E.I₀) (x✝ : (E.restrictIndex f).I₀) : (E.restrictIndexHom f).h₀ x✝ = CategoryStruct.id ((E.restrictIndex f).X x✝)

@[simp]

theorem CategoryTheory.PreZeroHypercover.restrictIndexHom_s₀ {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) {ι : Type w'} (f : ι → E.I₀) (a✝ : ι) : (E.restrictIndexHom f).s₀ a✝ = f a✝

noncomputable def CategoryTheory.PreZeroHypercover.pullbackCoverOfLeftIsoPullback₁ {C : Type u} [Category.{v, u} C] {X : C} (E : PreZeroHypercover X) {Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [Limits.HasPullback f g] [∀ (i : E.I₀), Limits.HasPullback (Limits.pullback.fst f g) (E.f i)] [∀ (i : E.I₀), Limits.HasPullback (E.f i) (Limits.pullback.fst f g)] : E.pullbackCoverOfLeft f g ≅ pullback₁ (Limits.pullback.fst f g) E

If {Uᵢ} covers X, the pre-0-hypercover {Uᵢ ×[Z] Y} of X ×[Z] Y is isomorphic to the pullback of {Uᵢ} along the first projection.

noncomputable def CategoryTheory.PreZeroHypercover.pullbackCoverOfRightIsoPullback₂ {C : Type u} [Category.{v, u} C] {Y : C} (E : PreZeroHypercover Y) {X Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [Limits.HasPullback f g] [∀ (i : E.I₀), Limits.HasPullback (E.f i) (Limits.pullback.snd f g)] [∀ (i : E.I₀), Limits.HasPullback (Limits.pullback.snd f g) (E.f i)] : E.pullbackCoverOfRight f g ≅ pullback₂ (Limits.pullback.snd f g) E

If {Uᵢ} covers Y, the pre-0-hypercover {X ×[Z] Uᵢ} of X ×[Z] Y is isomorphic to the pullback of {Uᵢ} along the second projection.

def CategoryTheory.Presieve.preZeroHypercover {C : Type u} [Category.{v, u} C] {S : C} (R : Presieve S) : PreZeroHypercover S

The pre-0-hypercover associated to a presieve R. It is indexed by the morphisms in R.

theorem CategoryTheory.Presieve.preZeroHypercover_I₀ {C : Type u} [Category.{v, u} C] {S : C} (R : Presieve S) : R.preZeroHypercover.I₀ = ↑R.uncurry

theorem CategoryTheory.Presieve.preZeroHypercover_f {C : Type u} [Category.{v, u} C] {S : C} (R : Presieve S) (i : ↑R.uncurry) : R.preZeroHypercover.f i = (↑i).snd

theorem CategoryTheory.Presieve.preZeroHypercover_X {C : Type u} [Category.{v, u} C] {S : C} (R : Presieve S) (i : ↑R.uncurry) : R.preZeroHypercover.X i = (↑i).fst

@[simp]

theorem CategoryTheory.Presieve.presieve₀_preZeroHypercover {C : Type u} [Category.{v, u} C] {S : C} (R : Presieve S) : R.preZeroHypercover.presieve₀ = R

theorem CategoryTheory.Presieve.exists_eq_preZeroHypercover {C : Type u} [Category.{v, u} C] {S : C} (R : Presieve S) : ∃ (E : PreZeroHypercover S), R = E.presieve₀

def CategoryTheory.PreZeroHypercover.shrink {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) : PreZeroHypercover S

The deduplication of a pre-0-hypercover E in universe w to a pre-0-hypercover in universe max u v. This is indexed by the morphisms of E.

theorem CategoryTheory.PreZeroHypercover.shrink_I₀ {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) : E.shrink.I₀ = ↑(Set.range fun (i : E.I₀) => ⟨E.X i, E.f i⟩)

theorem CategoryTheory.PreZeroHypercover.shrink_X {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) (i : ↑E.presieve₀.uncurry) : E.shrink.X i = (↑i).fst

theorem CategoryTheory.PreZeroHypercover.shrink_f {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) (i : ↑E.presieve₀.uncurry) : E.shrink.f i = (↑i).snd

@[simp]

theorem CategoryTheory.PreZeroHypercover.presieve₀_shrink {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) : E.shrink.presieve₀ = E.presieve₀

theorem CategoryTheory.PreZeroHypercover.shrink_eq_shrink_of_presieve₀_eq_presieve₀ {C : Type u} [Category.{v, u} C] {S : C} {E F : PreZeroHypercover S} (h : E.presieve₀ = F.presieve₀) : E.shrink = F.shrink

theorem CategoryTheory.PreZeroHypercover.presieve₀_eq_presieve₀_iff {C : Type u} [Category.{v, u} C] {S : C} {E F : PreZeroHypercover S} : E.presieve₀ = F.presieve₀ ↔ E.shrink = F.shrink

def CategoryTheory.PreZeroHypercover.toShrink {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) : E.Hom E.shrink

E refines its deduplication.

noncomputable def CategoryTheory.PreZeroHypercover.fromShrink {C : Type u} [Category.{v, u} C] {S : C} (E : PreZeroHypercover S) : E.shrink.Hom E

The deduplication of E refines E.

class CategoryTheory.Precoverage.RespectsIso {C : Type u} [Category.{v, u} C] (J : Precoverage C) : Prop

A precoverage respects isomorphisms if the property of being covering is stable under isomorphism. Use PreZeroHypercover.presieve₀_mem_of_iso for no universe restrictions.

• of_iso {S : C} {E F : PreZeroHypercover S} (e : E ≅ F) : E.presieve₀ ∈ J.coverings S → F.presieve₀ ∈ J.coverings S

theorem CategoryTheory.Precoverage.RespectsIso.of_forall_exists_iso {C : Type u} [Category.{v, u} C] {J : Precoverage C} [J.RespectsIso] {S : C} {R T : Presieve S} (hRT : ∀ ⦃Z : C⦄ (g : Z ⟶ S), R g → ∃ (Y : C) (e : Y ≅ Z), T (CategoryStruct.comp e.hom g)) (hTR : ∀ ⦃Z : C⦄ (g : Z ⟶ S), T g → ∃ (Y : C) (e : Y ≅ Z), R (CategoryStruct.comp e.hom g)) (hR : R ∈ J.coverings S) : T ∈ J.coverings S

theorem CategoryTheory.PreZeroHypercover.presieve₀_mem_of_iso {C : Type u} [Category.{v, u} C] {J : Precoverage C} [J.RespectsIso] {S : C} {E F : PreZeroHypercover S} (e : E ≅ F) (hE : E.presieve₀ ∈ J.coverings S) : F.presieve₀ ∈ J.coverings S

theorem CategoryTheory.PreZeroHypercover.presieve₀_mem_iff_of_iso {C : Type u} [Category.{v, u} C] {J : Precoverage C} [J.RespectsIso] {S : C} {E F : PreZeroHypercover S} (e : E ≅ F) : E.presieve₀ ∈ J.coverings S ↔ F.presieve₀ ∈ J.coverings S

structure CategoryTheory.Precoverage.ZeroHypercover {C : Type u} [Category.{v, u} C] (J : Precoverage C) (S : C) extends CategoryTheory.PreZeroHypercover S : Type (max (max u v) (w + 1))

The type of 0-hypercovers of an object S : C in a category equipped with a coverage J. This can be constructed from a covering of S.

• I₀ : Type w
• X (i : self.I₀) : C
• f (i : self.I₀) : self.X i ⟶ S
• mem₀ : self.presieve₀ ∈ J.coverings S

def CategoryTheory.Precoverage.ZeroHypercover.singleton {C : Type u} [Category.{v, u} C] {J : Precoverage C} {S T : C} (f : S ⟶ T) (hf : Presieve.singleton f ∈ J.coverings T) : J.ZeroHypercover T

The 0-hypercover defined by a single covering morphism.

@[simp]

theorem CategoryTheory.Precoverage.ZeroHypercover.singleton_toPreZeroHypercover {C : Type u} [Category.{v, u} C] {J : Precoverage C} {S T : C} (f : S ⟶ T) (hf : Presieve.singleton f ∈ J.coverings T) : (singleton f hf).toPreZeroHypercover = PreZeroHypercover.singleton f

noncomputable def CategoryTheory.Precoverage.ZeroHypercover.pullback₁ {C : Type u} [Category.{v, u} C] {J : Precoverage C} {S T : C} [J.IsStableUnderBaseChange] (f : S ⟶ T) (E : J.ZeroHypercover T) [∀ (i : E.I₀), Limits.HasPullback f (E.f i)] : J.ZeroHypercover S

Pullback of a 0-hypercover along a morphism. The components are pullback f (E.f i).

@[simp]

theorem CategoryTheory.Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover {C : Type u} [Category.{v, u} C] {J : Precoverage C} {S T : C} [J.IsStableUnderBaseChange] (f : S ⟶ T) (E : J.ZeroHypercover T) [∀ (i : E.I₀), Limits.HasPullback f (E.f i)] : (pullback₁ f E).toPreZeroHypercover = PreZeroHypercover.pullback₁ f E.toPreZeroHypercover

noncomputable def CategoryTheory.Precoverage.ZeroHypercover.pullback₂ {C : Type u} [Category.{v, u} C] {J : Precoverage C} {S T : C} [J.IsStableUnderBaseChange] (f : S ⟶ T) (E : J.ZeroHypercover T) [∀ (i : E.I₀), Limits.HasPullback (E.f i) f] : J.ZeroHypercover S

Pullback of a 0-hypercover along a morphism. The components are pullback (E.f i) f.

@[simp]

theorem CategoryTheory.Precoverage.ZeroHypercover.pullback₂_toPreZeroHypercover {C : Type u} [Category.{v, u} C] {J : Precoverage C} {S T : C} [J.IsStableUnderBaseChange] (f : S ⟶ T) (E : J.ZeroHypercover T) [∀ (i : E.I₀), Limits.HasPullback (E.f i) f] : (pullback₂ f E).toPreZeroHypercover = PreZeroHypercover.pullback₂ f E.toPreZeroHypercover

def CategoryTheory.Precoverage.ZeroHypercover.bind {C : Type u} [Category.{v, u} C] {J : Precoverage C} {T : C} [J.IsStableUnderComposition] (E : J.ZeroHypercover T) (F : (i : E.I₀) → J.ZeroHypercover (E.X i)) : J.ZeroHypercover T

Refining each component of a 0-hypercover yields a refined 0-hypercover of the base.

@[simp]

theorem CategoryTheory.Precoverage.ZeroHypercover.bind_toPreZeroHypercover {C : Type u} [Category.{v, u} C] {J : Precoverage C} {T : C} [J.IsStableUnderComposition] (E : J.ZeroHypercover T) (F : (i : E.I₀) → J.ZeroHypercover (E.X i)) : (E.bind F).toPreZeroHypercover = E.bind fun (i : E.I₀) => (F i).toPreZeroHypercover

noncomputable def CategoryTheory.Precoverage.ZeroHypercover.inter {C : Type u} [Category.{v, u} C] {J : Precoverage C} {T : C} [J.IsStableUnderBaseChange] [J.IsStableUnderComposition] (E : J.ZeroHypercover T) (F : J.ZeroHypercover T) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] : J.ZeroHypercover T

Pairwise intersection of two 0-hypercovers.

@[simp]

theorem CategoryTheory.Precoverage.ZeroHypercover.inter_toPreZeroHypercover {C : Type u} [Category.{v, u} C] {J : Precoverage C} {T : C} [J.IsStableUnderBaseChange] [J.IsStableUnderComposition] (E : J.ZeroHypercover T) (F : J.ZeroHypercover T) [∀ (i : E.I₀) (j : F.I₀), Limits.HasPullback (E.f i) (F.f j)] : (E.inter F).toPreZeroHypercover = E.inter F.toPreZeroHypercover

def CategoryTheory.Precoverage.ZeroHypercover.reindex {C : Type u} [Category.{v, u} C] {J : Precoverage C} {T : C} (E : J.ZeroHypercover T) {ι : Type w'} (e : ι ≃ E.I₀) : J.ZeroHypercover T

Replace the indexing type of a 0-hypercover.

@[simp]

theorem CategoryTheory.Precoverage.ZeroHypercover.reindex_toPreZeroHypercover {C : Type u} [Category.{v, u} C] {J : Precoverage C} {T : C} (E : J.ZeroHypercover T) {ι : Type w'} (e : ι ≃ E.I₀) : (E.reindex e).toPreZeroHypercover = E.reindex e

def CategoryTheory.Precoverage.ZeroHypercover.sum {C : Type u} [Category.{v, u} C] {J : Precoverage C} {S : C} [J.IsStableUnderSup] (E : J.ZeroHypercover S) (F : J.ZeroHypercover S) : J.ZeroHypercover S

Disjoint union of two 0-hypercovers.

@[simp]

theorem CategoryTheory.Precoverage.ZeroHypercover.sum_toPreZeroHypercover {C : Type u} [Category.{v, u} C] {J : Precoverage C} {S : C} [J.IsStableUnderSup] (E : J.ZeroHypercover S) (F : J.ZeroHypercover S) : (E.sum F).toPreZeroHypercover = E.sum F.toPreZeroHypercover

def CategoryTheory.Precoverage.ZeroHypercover.add {C : Type u} [Category.{v, u} C] {J : Precoverage C} {S : C} (E : J.ZeroHypercover S) {T : C} (f : T ⟶ S) (hf : E.presieve₀ ⊔ Presieve.singleton f ∈ J.coverings S) : J.ZeroHypercover S

Add a single morphism to a 0-hypercover.

@[simp]

theorem CategoryTheory.Precoverage.ZeroHypercover.add_toPreZeroHypercover {C : Type u} [Category.{v, u} C] {J : Precoverage C} {S : C} (E : J.ZeroHypercover S) {T : C} (f : T ⟶ S) (hf : E.presieve₀ ⊔ Presieve.singleton f ∈ J.coverings S) : (E.add f hf).toPreZeroHypercover = E.add f

def CategoryTheory.Precoverage.ZeroHypercover.weaken {C : Type u} [Category.{v, u} C] {K L : Precoverage C} {X : C} (E : K.ZeroHypercover X) (h : K ≤ L) : L.ZeroHypercover X

If L is a finer precoverage than K, any 0-hypercover wrt. K is in particular a 0-hypercover wrt. to L.

@[simp]

theorem CategoryTheory.Precoverage.ZeroHypercover.weaken_toPreZeroHypercover {C : Type u} [Category.{v, u} C] {K L : Precoverage C} {X : C} (E : K.ZeroHypercover X) (h : K ≤ L) : (E.weaken h).toPreZeroHypercover = E.toPreZeroHypercover

instance CategoryTheory.Precoverage.ZeroHypercover.instHasPullbacksPresieve₀OfHasPullbacks {C : Type u} [Category.{v, u} C] (K : Precoverage C) [K.HasPullbacks] {X Y : C} (E : K.ZeroHypercover X) (f : Y ⟶ X) : E.presieve₀.HasPullbacks f

instance CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀ {C : Type u} [Category.{v, u} C] {X Y : C} (E : PreZeroHypercover X) (f : Y ⟶ X) [E.presieve₀.HasPullbacks f] (i : E.I₀) : Limits.HasPullback (E.f i) f

instance CategoryTheory.Precoverage.ZeroHypercover.instHasPullbackFOfHasPullbacksPresieve₀_1 {C : Type u} [Category.{v, u} C] {X Y : C} (E : PreZeroHypercover X) (f : Y ⟶ X) [E.presieve₀.HasPullbacks f] (i : E.I₀) : Limits.HasPullback f (E.f i)

@[reducible, inline]

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

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

instance CategoryTheory.Precoverage.ZeroHypercover.instCategory {C : Type u} [Category.{v, u} C] {J : Precoverage C} {S : C} : Category.{max v w, max (max (w + 1) u) v} (J.ZeroHypercover S)

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Precoverage.ZeroHypercover.id_s₀ {C : Type u} [Category.{v, u} C] {J : Precoverage C} {S : C} (x✝ : J.ZeroHypercover S) (a : x✝.I₀) : (CategoryStruct.id x✝).s₀ a = a

@[simp]

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

def CategoryTheory.Precoverage.ZeroHypercover.isoMk {C : Type u} [Category.{v, u} C] {J : Precoverage C} {S : C} {E F : J.ZeroHypercover S} (e : E.toPreZeroHypercover ≅ F.toPreZeroHypercover) : E ≅ F

An isomorphism in 0-hypercovers is an isomorphism of the underlying pre-0-hypercovers.

@[simp]

theorem CategoryTheory.Precoverage.ZeroHypercover.isoMk_inv {C : Type u} [Category.{v, u} C] {J : Precoverage C} {S : C} {E F : J.ZeroHypercover S} (e : E.toPreZeroHypercover ≅ F.toPreZeroHypercover) : (isoMk e).inv = e.inv

@[simp]

theorem CategoryTheory.Precoverage.ZeroHypercover.isoMk_hom {C : Type u} [Category.{v, u} C] {J : Precoverage C} {S : C} {E F : J.ZeroHypercover S} (e : E.toPreZeroHypercover ≅ F.toPreZeroHypercover) : (isoMk e).hom = e.hom

def CategoryTheory.Precoverage.ZeroHypercover.map {C : Type u} [Category.{v, u} C] {J : Precoverage C} {S : C} {D : Type u_1} [Category.{v_1, u_1} D] {K : Precoverage D} (F : Functor C D) (E : J.ZeroHypercover S) (h : J ≤ comap F K) : K.ZeroHypercover (F.obj S)

The image of a 0-hypercover under a functor.

@[simp]

theorem CategoryTheory.Precoverage.ZeroHypercover.map_toPreZeroHypercover {C : Type u} [Category.{v, u} C] {J : Precoverage C} {S : C} {D : Type u_1} [Category.{v_1, u_1} D] {K : Precoverage D} (F : Functor C D) (E : J.ZeroHypercover S) (h : J ≤ comap F K) : (map F E h).toPreZeroHypercover = PreZeroHypercover.map F E.toPreZeroHypercover

theorem CategoryTheory.Precoverage.ZeroHypercover.presieve₀_mem_of_iso {C : Type u} [Category.{v, u} C] {J : Precoverage C} [J.RespectsIso] {S : C} {E : J.ZeroHypercover S} {F : PreZeroHypercover S} (e : E.toPreZeroHypercover ≅ F) : F.presieve₀ ∈ J.coverings S

class CategoryTheory.Precoverage.ZeroHypercover.Small {C : Type u} [Category.{v, u} C] {J : Precoverage C} {S : C} (E : J.ZeroHypercover S) : Prop

A w-0-hypercover E is w'-small if there exists an indexing type ι in Type w' and a restriction map ι → E.I₀ such that the restriction of E to ι is still covering.

Note: This is weaker than E.I₀ being w'-small. For example, every Zariski cover of X : Scheme.{u} is u-small, because X itself suffices as indexing type.

• exists_restrictIndex_mem : ∃ (ι : Type w') (f : ι → E.I₀), (E.restrictIndex f).presieve₀ ∈ J.coverings S

instance CategoryTheory.Precoverage.ZeroHypercover.instSmallOfSmallI₀ {C : Type u} [Category.{v, u} C] {J : Precoverage C} {S : C} (E : J.ZeroHypercover S) [_root_.Small.{w', w} E.I₀] : E.Small

def CategoryTheory.Precoverage.ZeroHypercover.Small.Index {C : Type u} [Category.{v, u} C] {J : Precoverage C} {S : C} (E : J.ZeroHypercover S) [E.Small] : Type w'

The w'-index type of a w'-small 0-hypercover.

noncomputable def CategoryTheory.Precoverage.ZeroHypercover.Small.restrictFun {C : Type u} [Category.{v, u} C] {J : Precoverage C} {S : C} (E : J.ZeroHypercover S) [E.Small] : Index E → E.I₀

The index restriction function of a small 0-hypercover.

theorem CategoryTheory.Precoverage.ZeroHypercover.Small.mem₀ {C : Type u} [Category.{v, u} C] {J : Precoverage C} {S : C} (E : J.ZeroHypercover S) [E.Small] : (E.restrictIndex (restrictFun E)).presieve₀ ∈ J.coverings S

instance CategoryTheory.Precoverage.ZeroHypercover.instSmall {C : Type u} [Category.{v, u} C] {J : Precoverage C} {S : C} (E : J.ZeroHypercover S) : E.Small

noncomputable def CategoryTheory.Precoverage.ZeroHypercover.restrictIndexOfSmall {C : Type u} [Category.{v, u} C] {J : Precoverage C} {S : C} (E : J.ZeroHypercover S) [E.Small] : J.ZeroHypercover S

Restrict a w'-small 0-hypercover to a w'-0-hypercover.

@[simp]

theorem CategoryTheory.Precoverage.ZeroHypercover.restrictIndexOfSmall_toPreZeroHypercover {C : Type u} [Category.{v, u} C] {J : Precoverage C} {S : C} (E : J.ZeroHypercover S) [E.Small] : E.restrictIndexOfSmall.toPreZeroHypercover = E.restrictIndex (Small.restrictFun E)

instance CategoryTheory.Precoverage.ZeroHypercover.instSmallPullback₁ {C : Type u} [Category.{v, u} C] {J : Precoverage C} {S : C} (E : J.ZeroHypercover S) [E.Small] {T : C} (f : T ⟶ S) [J.IsStableUnderBaseChange] [∀ (i : E.I₀), Limits.HasPullback f (E.f i)] : (pullback₁ f E).Small

theorem CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover {C : Type u} [Category.{v, u} C] {J : Precoverage C} {X : C} {R : Presieve X} : R ∈ J.coverings X ↔ ∃ (𝒰 : J.ZeroHypercover X), R = Presieve.ofArrows 𝒰.X 𝒰.f

theorem CategoryTheory.Precoverage.le_of_zeroHypercover {C : Type u} [Category.{v, u} C] {J K : Precoverage C} (h : ∀ ⦃X : C⦄ ⦃E : J.ZeroHypercover X⦄, E.presieve₀ ∈ K.coverings X) : J ≤ K

class CategoryTheory.Precoverage.Small {C : Type u} [Category.{v, u} C] (J : Precoverage C) : Prop

A precoverage is w-small, if every 0-hypercover is w-small.

• zeroHypercoverSmall {S : C} (E : J.ZeroHypercover S) : E.Small

instance CategoryTheory.Precoverage.instSmallOfSmall {C : Type u} [Category.{v, u} C] (J : Precoverage C) [J.Small] {S : C} (E : J.ZeroHypercover S) : E.Small

instance CategoryTheory.Precoverage.instSmallComap {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] {F : Functor C D} (J : Precoverage D) [J.Small] : (comap F J).Small

theorem CategoryTheory.Precoverage.Small.inf {C : Type u} [Category.{v, u} C] {J K : Precoverage C} [J.Small] (of_le : ∀ ⦃X : C⦄ ⦃R S : Presieve X⦄, R ≤ S → S ∈ K.coverings X → R ∈ K.coverings X) : (J ⊓ K).Small

instance CategoryTheory.Precoverage.instRespectsIsoOfIsStableUnderBaseChange {C : Type u} [Category.{v, u} C] {J : Precoverage C} [J.IsStableUnderBaseChange] : J.RespectsIso

noncomputable def CategoryTheory.Precoverage.ZeroHypercover.pullbackCoverOfLeft {C : Type u} [Category.{v, u} C] {J : Precoverage C} [J.IsStableUnderBaseChange] {X : C} (E : J.ZeroHypercover X) {Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [Limits.HasPullback f g] [∀ (i : E.I₀), Limits.HasPullback (E.f i) (Limits.pullback.fst f g)] : J.ZeroHypercover (Limits.pullback f g)

If {Uᵢ} covers X, this is the 0-hypercover of X ×[Z] Y given by {Uᵢ ×[Z] Y}.

@[simp]

theorem CategoryTheory.Precoverage.ZeroHypercover.pullbackCoverOfLeft_toPreZeroHypercover {C : Type u} [Category.{v, u} C] {J : Precoverage C} [J.IsStableUnderBaseChange] {X : C} (E : J.ZeroHypercover X) {Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [Limits.HasPullback f g] [∀ (i : E.I₀), Limits.HasPullback (E.f i) (Limits.pullback.fst f g)] : (E.pullbackCoverOfLeft f g).toPreZeroHypercover = E.pullbackCoverOfLeft f g

noncomputable def CategoryTheory.Precoverage.ZeroHypercover.pullbackCoverOfRight {C : Type u} [Category.{v, u} C] {J : Precoverage C} [J.IsStableUnderBaseChange] {Y : C} (E : J.ZeroHypercover Y) {X Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [Limits.HasPullback f g] [∀ (i : E.I₀), Limits.HasPullback (E.f i) (Limits.pullback.snd f g)] : J.ZeroHypercover (Limits.pullback f g)

If {Uᵢ} covers Y, this is the 0-hypercover of X ×[Z] Y given by {X ×[Z] Uᵢ}.

@[simp]

theorem CategoryTheory.Precoverage.ZeroHypercover.pullbackCoverOfRight_toPreZeroHypercover {C : Type u} [Category.{v, u} C] {J : Precoverage C} [J.IsStableUnderBaseChange] {Y : C} (E : J.ZeroHypercover Y) {X Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [Limits.HasPullback f g] [∀ (i : E.I₀), Limits.HasPullback (E.f i) (Limits.pullback.snd f g)] : (E.pullbackCoverOfRight f g).toPreZeroHypercover = E.pullbackCoverOfRight f g