Horns as colimits #

In this file, we express horns as colimits:

horns in Δ[2] are pushouts of two copies of Δ[1];
horns in Δ[n] are multicoequalizers of copies of the standard simplex of dimension n-1 (a dedicated API is provided for inner horns in Δ[3]).

source

theorem SSet.horn₂₀.sq :

(stdSimplex.face {0}).BicartSq (stdSimplex.face {0, 1}) (stdSimplex.face {0, 2}) (horn 2 0)

source

@[reducible, inline]

abbrev SSet.horn₂₀.ι₀₁ :

stdSimplex.obj { len := 1 } ⟶ (horn 2 0).toSSet

The inclusion Δ[1] ⟶ Λ[2, 0] which avoids 2.

Equations

SSet.horn₂₀.ι₀₁ = SSet.horn.ι 0 2 SSet.horn₂₀.ι₀₁._proof_1

Instances For

source

@[reducible, inline]

abbrev SSet.horn₂₀.ι₀₂ :

stdSimplex.obj { len := 1 } ⟶ (horn 2 0).toSSet

The inclusion Δ[1] ⟶ Λ[2, 0] which avoids 1.

Equations

SSet.horn₂₀.ι₀₂ = SSet.horn.ι 0 1 SSet.horn₂₀.ι₀₂._proof_1

Instances For

source

theorem SSet.horn₂₀.isPushout :

CategoryTheory.IsPushout (stdSimplex.δ 1) (stdSimplex.δ 1) ι₀₁ ι₀₂

source

theorem SSet.horn₂₁.sq :

(stdSimplex.face {1}).BicartSq (stdSimplex.face {0, 1}) (stdSimplex.face {1, 2}) (horn 2 1)

source

@[reducible, inline]

abbrev SSet.horn₂₁.ι₀₁ :

stdSimplex.obj { len := 1 } ⟶ (horn 2 1).toSSet

The inclusion Δ[1] ⟶ Λ[2, 1] which avoids 2.

Equations

SSet.horn₂₁.ι₀₁ = SSet.horn.ι 1 2 SSet.horn₂₁.ι₀₁._proof_1

Instances For

source

@[reducible, inline]

abbrev SSet.horn₂₁.ι₁₂ :

stdSimplex.obj { len := 1 } ⟶ (horn 2 1).toSSet

The inclusion Δ[1] ⟶ Λ[2, 1] which avoids 0.

Equations

SSet.horn₂₁.ι₁₂ = SSet.horn.ι 1 0 SSet.horn₂₁.ι₁₂._proof_1

Instances For

source

theorem SSet.horn₂₁.isPushout :

CategoryTheory.IsPushout (stdSimplex.δ 0) (stdSimplex.δ 1) ι₀₁ ι₁₂

source

theorem SSet.horn₂₂.sq :

(stdSimplex.face {2}).BicartSq (stdSimplex.face {0, 2}) (stdSimplex.face {1, 2}) (horn 2 2)

source

@[reducible, inline]

abbrev SSet.horn₂₂.ι₀₂ :

stdSimplex.obj { len := 1 } ⟶ (horn 2 2).toSSet

The inclusion Δ[1] ⟶ Λ[2, 2] which avoids 1.

Equations

SSet.horn₂₂.ι₀₂ = SSet.horn.ι 2 1 SSet.horn₂₂.ι₀₂._proof_1

Instances For

source

@[reducible, inline]

abbrev SSet.horn₂₂.ι₁₂ :

stdSimplex.obj { len := 1 } ⟶ (horn 2 2).toSSet

The inclusion Δ[1] ⟶ Λ[2, 2] which avoids 0.

Equations

SSet.horn₂₂.ι₁₂ = SSet.horn.ι 2 0 SSet.horn₂₂.ι₁₂._proof_1

Instances For

source

theorem SSet.horn₂₂.isPushout :

CategoryTheory.IsPushout (stdSimplex.δ 0) (stdSimplex.δ 0) ι₀₂ ι₁₂

source

theorem SSet.horn.multicoequalizerDiagram {n : ℕ} (i : Fin (n + 1)) :

(horn n i).MulticoequalizerDiagram (fun (j : ↑{i}ᶜ) => stdSimplex.face {↑j}ᶜ) fun (j k : ↑{i}ᶜ) => stdSimplex.face {↑j, ↑k}ᶜ

The multicoequalizer diagram which expresses Λ[n, i] as a gluing of all 1-codimensional faces of the standard simplex but one along suitable 2-codimensional faces.

source

noncomputable def SSet.horn.isColimit {n : ℕ} (i : Fin (n + 1)) :

CategoryTheory.Limits.IsColimit ((CompleteLattice.MulticoequalizerDiagram.multicofork ⋯).toLinearOrder.map Subcomplex.toSSetFunctor)

The horn is a multicoequalizer of all 1-codimensional faces of the standard simplex but one along suitable 2-codimensional faces.

Equations

SSet.horn.isColimit i = ⋯.isColimit'

Instances For

source

theorem SSet.horn.hom_ext' {n : ℕ} {X : SSet} {i : Fin (n + 2)} {f g : (horn (n + 1) i).toSSet ⟶ X} (h : ∀ (j : Fin (n + 2)) (hj : j ≠ i), CategoryTheory.CategoryStruct.comp (ι i j hj) f = CategoryTheory.CategoryStruct.comp (ι i j hj) g) :

f = g

source

def SSet.horn.IsCompatible {n : ℕ} {X : SSet} {i : Fin (n + 2)} (f : (j : Fin (n + 2)) → j ≠ i → (stdSimplex.obj { len := n } ⟶ X)) :

Prop

Let i : Fin (n + 2). This is the condition that a family of morphisms Δ[n] ⟶ X for j ≠ i are the "faces" of a morphism Λ[n + 1, i] ⟶ X.

Equations

One or more equations did not get rendered due to their size.
SSet.horn.IsCompatible f_2 = True

Instances For

source

@[simp]

theorem SSet.horn.isCompatible_zero_iff_true {X : SSet} {i : Fin 2} (f : (j : Fin 2) → j ≠ i → (stdSimplex.obj { len := 0 } ⟶ X)) :

horn.IsCompatible f ↔ True

source

@[simp]

theorem SSet.horn.isCompatible_iff {n : ℕ} {X : SSet} {i : Fin (n + 3)} (f : (j : Fin (n + 3)) → j ≠ i → (stdSimplex.obj { len := n + 1 } ⟶ X)) :

horn.IsCompatible f ↔ ∀ (j k : Fin (n + 3)) (hj : j ≠ i) (hk : k ≠ i) (hjk : j < k), CategoryTheory.CategoryStruct.comp (stdSimplex.δ (k.pred ⋯)) (f j hj) = CategoryTheory.CategoryStruct.comp (stdSimplex.δ (j.castPred ⋯)) (f k hk)

source

theorem SSet.horn.IsCompatible.of_hom {n : ℕ} {X : SSet} {i : Fin (n + 2)} (g : (horn (n + 1) i).toSSet ⟶ X) :

horn.IsCompatible fun (j : Fin (n + 2)) (hj : j ≠ i) => CategoryTheory.CategoryStruct.comp (ι i j hj) g

source

theorem SSet.horn.IsCompatible.δ_pred_comp {n : ℕ} {X : SSet} {i : Fin (n + 3)} {f : (j : Fin (n + 3)) → j ≠ i → (stdSimplex.obj { len := n + 1 } ⟶ X)} (hf : horn.IsCompatible f) (j k : Fin (n + 3)) (hj : j ≠ i := by grind) (hk : k ≠ i := by grind) (hjk : j < k := by grind) :

CategoryTheory.CategoryStruct.comp (stdSimplex.δ (k.pred ⋯)) (f j hj) = CategoryTheory.CategoryStruct.comp (stdSimplex.δ (j.castPred ⋯)) (f k hk)

source

theorem SSet.horn.IsCompatible.δ_pred_comp_assoc {n : ℕ} {X : SSet} {i : Fin (n + 3)} {f : (j : Fin (n + 3)) → j ≠ i → (stdSimplex.obj { len := n + 1 } ⟶ X)} (hf : horn.IsCompatible f) (j k : Fin (n + 3)) (hj : j ≠ i := by grind) (hk : k ≠ i := by grind) (hjk : j < k := by grind) {Z : SSet} (h : X ⟶ Z) :