Horns as colimits

In this file, we express horns as colimits:

• horns in Δ[2] are pushouts of two copies of Δ[1].

theorem SSet.horn₂₀.sq : (stdSimplex.face {0}).BicartSq (stdSimplex.face {0, 1}) (stdSimplex.face {0, 2}) (horn 2 0)

@[reducible, inline]

abbrev SSet.horn₂₀.ι₀₁ : stdSimplex.obj (SimplexCategory.mk 1) ⟶ (horn 2 0).toSSet

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

Equations

• SSet.horn₂₀.ι₀₁ = SSet.horn.ι 0 2 SSet.horn₂₀.ι₀₁._proof_3

@[reducible, inline]

abbrev SSet.horn₂₀.ι₀₂ : stdSimplex.obj (SimplexCategory.mk 1) ⟶ (horn 2 0).toSSet

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

Equations

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

theorem SSet.horn₂₀.isPushout : CategoryTheory.IsPushout (stdSimplex.δ 1) (stdSimplex.δ 1) ι₀₁ ι₀₂

theorem SSet.horn₂₁.sq : (stdSimplex.face {1}).BicartSq (stdSimplex.face {0, 1}) (stdSimplex.face {1, 2}) (horn 2 1)

@[reducible, inline]

abbrev SSet.horn₂₁.ι₀₁ : stdSimplex.obj (SimplexCategory.mk 1) ⟶ (horn 2 1).toSSet

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

Equations

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

@[reducible, inline]

abbrev SSet.horn₂₁.ι₁₂ : stdSimplex.obj (SimplexCategory.mk 1) ⟶ (horn 2 1).toSSet

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

Equations

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

theorem SSet.horn₂₁.isPushout : CategoryTheory.IsPushout (stdSimplex.δ 0) (stdSimplex.δ 1) ι₀₁ ι₁₂

theorem SSet.horn₂₂.sq : (stdSimplex.face {2}).BicartSq (stdSimplex.face {0, 2}) (stdSimplex.face {1, 2}) (horn 2 2)

@[reducible, inline]

abbrev SSet.horn₂₂.ι₀₂ : stdSimplex.obj (SimplexCategory.mk 1) ⟶ (horn 2 2).toSSet

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

Equations

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

@[reducible, inline]

abbrev SSet.horn₂₂.ι₁₂ : stdSimplex.obj (SimplexCategory.mk 1) ⟶ (horn 2 2).toSSet

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

Equations

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

theorem SSet.horn₂₂.isPushout : CategoryTheory.IsPushout (stdSimplex.δ 0) (stdSimplex.δ 0) ι₀₂ ι₁₂