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

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

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

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_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.singleton_I₀ {C : Type u} [Category.{v, u} C] {S T : C} (f : S ⟶ T) : (singleton f).I₀ = PUnit.{w + 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).

@[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₂_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} [Limits.HasPullbacks C] (f : S ⟶ T) (E : PreZeroHypercover T) : (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.

@[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_X {C : Type u} [Category.{v, u} C] {T : C} (E : PreZeroHypercover T) (F : (i : E.I₀) → PreZeroHypercover (E.X i)) (x✝ : (i : E.I₀) × (F i).I₀) : (E.bind F).X x✝ = match x✝ with | ⟨i, j⟩ => (F i).X j

@[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)) (x✝ : (i : E.I₀) × (F i).I₀) : (E.bind F).f x✝ = match x✝ with | ⟨i, j⟩ => CategoryStruct.comp ((F i).f j) (E.f i)

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

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

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

structure CategoryTheory.Coverage.ZeroHypercover {C : Type u} [Category.{v, u} C] (J : Coverage 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.covering S

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

The 0-hypercover defined by a single covering morphism.

@[simp]

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

noncomputable def CategoryTheory.Coverage.ZeroHypercover.pullback₁ {C : Type u} [Category.{v, u} C] (J : Coverage C) {S T : C} [J.IsStableUnderBaseChange] [Limits.HasPullbacks C] (f : S ⟶ T) (E : J.ZeroHypercover T) : J.ZeroHypercover S

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

@[simp]

theorem CategoryTheory.Coverage.ZeroHypercover.pullback₁_toPreZeroHypercover {C : Type u} [Category.{v, u} C] (J : Coverage C) {S T : C} [J.IsStableUnderBaseChange] [Limits.HasPullbacks C] (f : S ⟶ T) (E : J.ZeroHypercover T) : (pullback₁ J f E).toPreZeroHypercover = PreZeroHypercover.pullback₁ f E.toPreZeroHypercover

noncomputable def CategoryTheory.Coverage.ZeroHypercover.pullback₂ {C : Type u} [Category.{v, u} C] (J : Coverage C) {S T : C} [J.IsStableUnderBaseChange] [Limits.HasPullbacks C] (f : S ⟶ T) (E : J.ZeroHypercover T) : J.ZeroHypercover S

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

@[simp]

theorem CategoryTheory.Coverage.ZeroHypercover.pullback₂_toPreZeroHypercover {C : Type u} [Category.{v, u} C] (J : Coverage C) {S T : C} [J.IsStableUnderBaseChange] [Limits.HasPullbacks C] (f : S ⟶ T) (E : J.ZeroHypercover T) : (pullback₂ J f E).toPreZeroHypercover = PreZeroHypercover.pullback₂ f E.toPreZeroHypercover

def CategoryTheory.Coverage.ZeroHypercover.bind {C : Type u} [Category.{v, u} C] (J : Coverage 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.

@[reducible, inline]

abbrev CategoryTheory.Coverage.ZeroHypercover.Hom {C : Type u} [Category.{v, u} C] (J : Coverage 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.Coverage.ZeroHypercover.instCategory {C : Type u} [Category.{v, u} C] (J : Coverage C) {S : C} : Category.{max v w, max (max (w + 1) u) v} (J.ZeroHypercover S)

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Coverage.ZeroHypercover.comp_s₀ {C : Type u} [Category.{v, u} C] (J : Coverage 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.Coverage.ZeroHypercover.comp_h₀ {C : Type u} [Category.{v, u} C] (J : Coverage 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))