Saturation of a `0`-hypercover #

Given a 0-hypercover E, we define a 1-hypercover E.saturate

structure CategoryTheory.PreZeroHypercover.Relation {C : Type u_1} [Category.{v_1, u_1} C] {S : C} (E : PreZeroHypercover S) (i j : E.I₀) :

Type (max u_1 v_1)

A relation on a pre-0-hypercover is a commutative diagram

obj ----> E.X i
 |         |
 |         |
 v         v
E.X j ---> S

obj : C
The object.
fst : self.obj ⟶ E.X i
The first projection.
snd : self.obj ⟶ E.X j
The second projection.
w : CategoryStruct.comp self.fst (E.f i) = CategoryStruct.comp self.snd (E.f j)

Instances For

source

def CategoryTheory.PreZeroHypercover.saturate {C : Type u_1} [Category.{v_1, u_1} C] {S : C} (E : PreZeroHypercover S) :

PreOneHypercover S

The maximal pre-1-hypercover containing E, where the 1-components are all relations on E.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.PreZeroHypercover.saturate_I₁ {C : Type u_1} [Category.{v_1, u_1} C] {S : C} (E : PreZeroHypercover S) (i j : E.I₀) :

E.saturate.I₁ i j = E.Relation i j

source

@[simp]

theorem CategoryTheory.PreZeroHypercover.saturate_p₂ {C : Type u_1} [Category.{v_1, u_1} C] {S : C} (E : PreZeroHypercover S) (x✝ x✝¹ : E.I₀) (r : E.Relation x✝ x✝¹) :

E.saturate.p₂ r = r.snd

source

@[simp]

theorem CategoryTheory.PreZeroHypercover.saturate_Y {C : Type u_1} [Category.{v_1, u_1} C] {S : C} (E : PreZeroHypercover S) (x✝ x✝¹ : E.I₀) (r : E.Relation x✝ x✝¹) :

E.saturate.Y r = r.obj

source

@[simp]

theorem CategoryTheory.PreZeroHypercover.saturate_toPreZeroHypercover {C : Type u_1} [Category.{v_1, u_1} C] {S : C} (E : PreZeroHypercover S) :

E.saturate.toPreZeroHypercover = E

source

@[simp]

theorem CategoryTheory.PreZeroHypercover.saturate_p₁ {C : Type u_1} [Category.{v_1, u_1} C] {S : C} (E : PreZeroHypercover S) (x✝ x✝¹ : E.I₀) (r : E.Relation x✝ x✝¹) :

E.saturate.p₁ r = r.fst

source

def CategoryTheory.PreZeroHypercover.sectionsSaturateEquiv {C : Type u_1} [Category.{v_1, u_1} C] {S : C} (E : PreZeroHypercover S) (F : Functor Cᵒᵖ (Type u_3)) :

(E.saturate.multicospanIndex F).sections ≃ Subtype (Presieve.Arrows.Compatible F E.f)

For a presheaf of types, sections over the multifork associated to E.saturate are equivalent to compatible families.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.PreZeroHypercover.sectionsSaturateEquiv_apply_coe {C : Type u_1} [Category.{v_1, u_1} C] {S : C} (E : PreZeroHypercover S) (F : Functor Cᵒᵖ (Type u_3)) (s : (E.saturate.multicospanIndex F).sections) (i : E.saturate.multicospanShape.L) :

↑((E.sectionsSaturateEquiv F) s) i = s.val i

source

@[simp]

theorem CategoryTheory.PreZeroHypercover.sectionsSaturateEquiv_symm_apply_val {C : Type u_1} [Category.{v_1, u_1} C] {S : C} (E : PreZeroHypercover S) (F : Functor Cᵒᵖ (Type u_3)) (s : Subtype (Presieve.Arrows.Compatible F E.f)) (i : E.I₀) :

((E.sectionsSaturateEquiv F).symm s).val i = ↑s i

source

theorem CategoryTheory.PreZeroHypercover.isLimit_saturate_type_iff {C : Type u_1} [Category.{v_1, u_1} C] {S : C} (E : PreZeroHypercover S) (F : Functor Cᵒᵖ (Type u_3)) :

Nonempty (Limits.IsLimit (E.saturate.multifork F)) ↔ Presieve.IsSheafFor F E.presieve₀

source

noncomputable def CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks {C : Type u_1} [Category.{v_1, u_1} C] {S : C} (E : PreZeroHypercover S) [E.HasPullbacks] :

E.toPreOneHypercover ⟶ E.saturate

If E has pairwise pullbacks, this is the canonical map from the minimal 1-hypercover to the saturation.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_h₁ {C : Type u_1} [Category.{v_1, u_1} C] {S : C} (E : PreZeroHypercover S) [E.HasPullbacks] {i j : E.toPreOneHypercover.I₀} (k : E.toPreOneHypercover.I₁ i j) :

E.toSaturateOfHasPullbacks.h₁ k = CategoryStruct.id (E.toPreOneHypercover.Y k)

source

@[simp]

theorem CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_s₀ {C : Type u_1} [Category.{v_1, u_1} C] {S : C} (E : PreZeroHypercover S) [E.HasPullbacks] (i : E.toPreOneHypercover.I₀) :

E.toSaturateOfHasPullbacks.s₀ i = i

source

@[simp]

theorem CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_s₁_fst {C : Type u_1} [Category.{v_1, u_1} C] {S : C} (E : PreZeroHypercover S) [E.HasPullbacks] {i j : E.toPreOneHypercover.I₀} (k : E.toPreOneHypercover.I₁ i j) :

(E.toSaturateOfHasPullbacks.s₁ k).fst = Limits.pullback.fst (E.f i) (E.f j)

source

@[simp]

theorem CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_s₁_snd {C : Type u_1} [Category.{v_1, u_1} C] {S : C} (E : PreZeroHypercover S) [E.HasPullbacks] {i j : E.toPreOneHypercover.I₀} (k : E.toPreOneHypercover.I₁ i j) :

(E.toSaturateOfHasPullbacks.s₁ k).snd = Limits.pullback.snd (E.f i) (E.f j)

source

@[simp]

theorem CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_h₀ {C : Type u_1} [Category.{v_1, u_1} C] {S : C} (E : PreZeroHypercover S) [E.HasPullbacks] (i : E.toPreOneHypercover.I₀) :

E.toSaturateOfHasPullbacks.h₀ i = CategoryStruct.id (E.toPreOneHypercover.X i)

source

@[simp]

theorem CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_s₁_obj {C : Type u_1} [Category.{v_1, u_1} C] {S : C} (E : PreZeroHypercover S) [E.HasPullbacks] {i j : E.toPreOneHypercover.I₀} (k : E.toPreOneHypercover.I₁ i j) :

(E.toSaturateOfHasPullbacks.s₁ k).obj = Limits.pullback (E.f i) (E.f j)

source

noncomputable def CategoryTheory.PreZeroHypercover.fromSaturateOfHasPullbacks {C : Type u_1} [Category.{v_1, u_1} C] {S : C} (E : PreZeroHypercover S) [E.HasPullbacks] :

E.saturate ⟶ E.toPreOneHypercover

If E has pairwise pullbacks, this is the canonical map to the minimal 1-hypercover from the saturation.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.PreZeroHypercover.fromSaturateOfHasPullbacks_h₀ {C : Type u_1} [Category.{v_1, u_1} C] {S : C} (E : PreZeroHypercover S) [E.HasPullbacks] (i : E.saturate.I₀) :

E.fromSaturateOfHasPullbacks.h₀ i = CategoryStruct.id (E.saturate.X i)

source

@[simp]

theorem CategoryTheory.PreZeroHypercover.fromSaturateOfHasPullbacks_h₁ {C : Type u_1} [Category.{v_1, u_1} C] {S : C} (E : PreZeroHypercover S) [E.HasPullbacks] {i j : E.saturate.I₀} (k : E.saturate.I₁ i j) :

E.fromSaturateOfHasPullbacks.h₁ k = Limits.pullback.lift k.fst k.snd ⋯

source

@[simp]

theorem CategoryTheory.PreZeroHypercover.fromSaturateOfHasPullbacks_s₁ {C : Type u_1} [Category.{v_1, u_1} C] {S : C} (E : PreZeroHypercover S) [E.HasPullbacks] {i j : E.saturate.I₀} (k : E.saturate.I₁ i j) :

E.fromSaturateOfHasPullbacks.s₁ k = PUnit.unit

source

@[simp]

theorem CategoryTheory.PreZeroHypercover.fromSaturateOfHasPullbacks_s₀ {C : Type u_1} [Category.{v_1, u_1} C] {S : C} (E : PreZeroHypercover S) [E.HasPullbacks] (i : E.saturate.I₀) :

E.fromSaturateOfHasPullbacks.s₀ i = i

source

noncomputable def CategoryTheory.PreZeroHypercover.toPreOneHypercoverHomotopy {C : Type u_1} [Category.{v_1, u_1} C] {S : C} (E : PreZeroHypercover S) [E.HasPullbacks] :

PreOneHypercover.Homotopy (PreOneHypercover.Hom.id E.toPreOneHypercover) (PreOneHypercover.Hom.id E.toPreOneHypercover)

The identity of the minimal pre-1-hypercover when E has pairwise pullbacks is homotopic to itself.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.PreZeroHypercover.toSaturateOfHasPullbacks_fromSaturateOfHasPullbacks {C : Type u_1} [Category.{v_1, u_1} C] {S : C} (E : PreZeroHypercover S) [E.HasPullbacks] :

PreOneHypercover.Hom.comp E.toSaturateOfHasPullbacks E.fromSaturateOfHasPullbacks = PreOneHypercover.Hom.id E.toPreOneHypercover

source

noncomputable def CategoryTheory.PreZeroHypercover.fromSaturateToSaturateHomotopy {C : Type u_1} [Category.{v_1, u_1} C] {S : C} (E : PreZeroHypercover S) [E.HasPullbacks] :

PreOneHypercover.Homotopy (PreOneHypercover.Hom.comp E.fromSaturateOfHasPullbacks E.toSaturateOfHasPullbacks) (PreOneHypercover.Hom.id E.saturate)

The composition E.saturate ⟶ E.toPreOneHypercover ⟶ E.saturate is homotopic to the identity.

Equations

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

Instances For

source

noncomputable def CategoryTheory.PreZeroHypercover.isLimitSaturateEquivOfHasPullbacks {C : Type u_1} [Category.{v_1, u_1} C] {A : Type u_2} [Category.{v_2, u_2} A] {S : C} (E : PreZeroHypercover S) [E.HasPullbacks] (F : Functor Cᵒᵖ A) :

Limits.IsLimit (E.saturate.multifork F) ≃ Limits.IsLimit (E.toPreOneHypercover.multifork F)

If the pre-0-hypercover E has pairwise pullbacks, then the multifork associated to the full saturated pre-1-hypercover is exact if and only if the minimal one given by taking the pairwise pullbacks is exact.

Equations

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

Instances For

Documentation

Mathlib.CategoryTheory.Sites.Hypercover.Saturate

Saturation of a `0`-hypercover #

Saturation of a 0-hypercover #

Saturation of a `0`-hypercover #