0-hypercovers

Given a coverage J on a category C, we define the type of 0-hypercovers of an object S : C. They consists 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₂.

Equations

• E.HasPullbacks = ∀ (i₁ i₂ : E.I₀), CategoryTheory.Limits.HasPullback (E.f i₁) (E.f 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.

Equations

• E.presieve₀ = CategoryTheory.Presieve.ofArrows E.X E.f

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

Equations

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

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.

Equations

• CategoryTheory.PreZeroHypercover.singleton f = { I₀ := PUnit.{?u.11 + 1}, X := fun (x : PUnit.{?u.11 + 1}) => S, f := fun (x : PUnit.{?u.11 + 1}) => 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.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.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₀

Equations

• CategoryTheory.PreZeroHypercover.instUniqueI₀Singleton f = inferInstanceAs (Unique PUnit.{?u.27 + 1})

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

Equations

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

@[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₁_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)

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

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.

Equations

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

@[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₂_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₀

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

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₀

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.

Equations

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

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

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

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₀.

Equations

• E.restrictIndex f = { I₀ := ι, X := E.X ∘ f, f := fun (i : ι) => E.f (f 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_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.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.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₀

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.

Equations

• E.reindex e = E.restrictIndex ⇑e

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

Equations

• E.inter F = (E.bind fun (i : E.I₀) => CategoryTheory.PreZeroHypercover.pullback₁ (E.f i) F).reindex (Equiv.sigmaEquivProd E.I₀ F.1).symm

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

Equations

• E.sum F = { I₀ := E.I₀ ⊕ F.I₀, X := Sum.elim E.X F.X, f := fun (x : E.I₀ ⊕ F.I₀) => match x with | Sum.inl i => E.f i | Sum.inr i => F.f i }

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

Equations

• E.add f = (E.sum (CategoryTheory.PreZeroHypercover.singleton f)).reindex (Equiv.optionEquivSumPUnit E.I₀)

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

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.

Equations

• CategoryTheory.PreZeroHypercover.Hom.id E = { s₀ := id, h₀ := fun (x : E.I₀) => CategoryTheory.CategoryStruct.id (E.X x), w₀ := ⋯ }

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

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

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.

Equations

• f.comp g = { s₀ := g.s₀ ∘ f.s₀, h₀ := fun (i : E.I₀) => CategoryTheory.CategoryStruct.comp (f.h₀ i) (g.h₀ (f.s₀ i)), w₀ := ⋯ }

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

Equations

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

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

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

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.

Equations

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

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

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

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

Equations

• CategoryTheory.PreZeroHypercover.map F E = { I₀ := E.I₀, X := fun (i : E.I₀) => F.obj (E.X i), f := fun (i : E.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.{u_2, u_1} D] (F : Functor C D) (E : PreZeroHypercover S) : (map F E).I₀ = E.I₀

@[simp]

theorem CategoryTheory.PreZeroHypercover.map_f {C : Type u} [Category.{v, u} C] {S : C} {D : Type u_1} [Category.{u_2, 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_X {C : Type u} [Category.{v, u} C] {S : C} {D : Type u_1} [Category.{u_2, 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.{u_2, 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.

Equations

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

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

Equations

• E.sumInl F = { s₀ := Sum.inl, h₀ := fun (x : E.I₀) => CategoryTheory.CategoryStruct.id (E.X x), w₀ := ⋯ }

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

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

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.

Equations

• E.sumInr F = { s₀ := Sum.inr, h₀ := fun (x : F.I₀) => CategoryTheory.CategoryStruct.id (F.X x), w₀ := ⋯ }

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

Equations

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

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

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

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.

Equations

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

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

Equations

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

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

Equations

• CategoryTheory.PreZeroHypercover.interLift f g = { s₀ := fun (i : G.I₀) => (f.s₀ i, g.s₀ i), h₀ := fun (i : G.I₀) => CategoryTheory.Limits.pullback.lift (f.h₀ i) (g.h₀ i) ⋯, w₀ := ⋯ }

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

Equations

• R.preZeroHypercover = { I₀ := ↑R.uncurry, X := fun (i : ↑R.uncurry) => (↑i).fst, f := fun (i : ↑R.uncurry) => (↑i).snd }

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.

Equations

• E.shrink = E.presieve₀.preZeroHypercover

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

Equations

• E.toShrink = { s₀ := fun (i : E.I₀) => ⟨⟨E.X i, E.f i⟩, ⋯⟩, h₀ := fun (i : E.I₀) => CategoryTheory.CategoryStruct.id (E.X i), w₀ := ⋯ }

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.

Equations

• E.fromShrink = { s₀ := fun (i : E.shrink.I₀) => ⋯.choose, h₀ := fun (i : E.shrink.I₀) => CategoryTheory.eqToHom ⋯, w₀ := ⋯ }

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.

Equations

• CategoryTheory.Precoverage.ZeroHypercover.singleton f hf = { toPreZeroHypercover := CategoryTheory.PreZeroHypercover.singleton f, mem₀ := ⋯ }

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

Equations

• CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f E = { toPreZeroHypercover := CategoryTheory.PreZeroHypercover.pullback₁ f E.toPreZeroHypercover, mem₀ := ⋯ }

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

Equations

• CategoryTheory.Precoverage.ZeroHypercover.pullback₂ f E = { toPreZeroHypercover := CategoryTheory.PreZeroHypercover.pullback₂ f E.toPreZeroHypercover, mem₀ := ⋯ }

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

Equations

• E.bind F = { toPreZeroHypercover := E.bind fun (i : E.I₀) => (F i).toPreZeroHypercover, mem₀ := ⋯ }

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• E.add f hf = { toPreZeroHypercover := E.add f, mem₀ := ⋯ }

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

Equations

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

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

Equations

• CategoryTheory.Precoverage.ZeroHypercover.Hom J E F = E.Hom F.toPreZeroHypercover

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)

Equations

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

@[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✝¹)

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

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.

Equations

• CategoryTheory.Precoverage.ZeroHypercover.isoMk e = { hom := e.hom, inv := e.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

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

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

def CategoryTheory.Precoverage.ZeroHypercover.map {C : Type u} [Category.{v, u} C] {J : Precoverage C} {S : C} {D : Type u_1} [Category.{u_2, 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.

Equations

• CategoryTheory.Precoverage.ZeroHypercover.map F E h = { toPreZeroHypercover := CategoryTheory.PreZeroHypercover.map F E.toPreZeroHypercover, mem₀ := ⋯ }

@[simp]

theorem CategoryTheory.Precoverage.ZeroHypercover.map_toPreZeroHypercover {C : Type u} [Category.{v, u} C] {J : Precoverage C} {S : C} {D : Type u_1} [Category.{u_2, 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

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.

Equations

• CategoryTheory.Precoverage.ZeroHypercover.Small.Index E = ⋯.choose

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.

Equations

• CategoryTheory.Precoverage.ZeroHypercover.Small.restrictFun E = ⋯.choose

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.

Equations

• E.restrictIndexOfSmall = { toPreZeroHypercover := E.restrictIndex (CategoryTheory.Precoverage.ZeroHypercover.Small.restrictFun E), mem₀ := ⋯ }

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