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.

source

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

Instances For

source

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

source

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

source

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

Instances For

source

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

Instances For

source

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

source

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

Instances For

source

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)

source

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 }

Instances For

source

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

source

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

source

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

source

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

source

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.

Instances For

source

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

source

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

source

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

source

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.

Instances For

source

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

source

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

source

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

source

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₀

source

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.

Instances For

source

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

source

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

source

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

source

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

Instances For

source

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

source

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

source

@[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₀ = ι

source

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

source

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

Instances For

source

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

source

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

source

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

source

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

source

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 }

Instances For

source

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

source

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✝

source

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

source

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

source

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

source

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

source

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

source

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

source

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

Instances For

source

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

source

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

source

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

source

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

source

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

source

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

source

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

Instances For

source

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

source

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₀

source

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

source

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₀ := ⋯ }

Instances For

source

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

source

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

source

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₀ := ⋯ }

Instances For

source

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

source

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

source

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.

source

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

source

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

source

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

source

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

source

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 = { s₀ := Sum.inl, h₀ := fun (x : E.I₀) => CategoryTheory.CategoryStruct.id (E.X x), w₀ := ⋯ }

Instances For

source

@[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.h₀ x✝ = CategoryStruct.id (E.X x✝)

source

@[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.s₀ val = Sum.inl val

source

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 = { s₀ := Sum.inr, h₀ := fun (x : F.I₀) => CategoryTheory.CategoryStruct.id (F.X x), w₀ := ⋯ }

Instances For

source

@[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.s₀ val = Sum.inr val

source

@[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.h₀ x✝ = CategoryStruct.id (F.X x✝)

source

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

E.sumLift f g = { s₀ := Sum.elim f.s₀ g.s₀, h₀ := fun (x : (E.sum F).I₀) => match x with | Sum.inl i => f.h₀ i | Sum.inr i => g.h₀ i, w₀ := ⋯ }

Instances For

source

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

(E.sumLift f g).s₀ a✝ = Sum.elim f.s₀ g.s₀ a✝

source

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

(E.sumLift f g).h₀ x✝ = match x✝ with | Sum.inl i => f.h₀ i | Sum.inr i => g.h₀ i

source

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

Instances For

source

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₀ := ⋯ }

Instances For

source

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

source

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₀ := ⋯ }

Instances For

source

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

source

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₀ := ⋯ }

Instances For

source

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

source

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₀ := ⋯ }

Instances For

source

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

source

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₀ := ⋯ }

Instances For

source

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

source

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₀ := ⋯ }

Instances For

source

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

source

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₀ := ⋯ }

Instances For

source

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

source

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₀ := ⋯ }

Instances For

source

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

source

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

Instances For

source

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.

source

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

source

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

source

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

source

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

source

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

Documentation

Mathlib.CategoryTheory.Sites.ZeroHypercover

0-hypercovers #