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

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.

@[reducible, inline]

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

The inclusion Δ[1] ⟶ Λ[2, 0] which avoids 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.

@[reducible, inline]

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

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

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.

@[reducible, inline]

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

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

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

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.

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.

@[reducible, inline]

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

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

def SSet.horn₃₁.desc.multicofork {X : SSet} (f₀ f₂ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₁₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₂) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₂ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₃) : CategoryTheory.Limits.Multicofork ((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor)

Auxiliary definition for desc.

@[simp]

theorem SSet.horn₃₁.desc.multicofork_pt {X : SSet} (f₀ f₂ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₁₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₂) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₂ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₃) : (multicofork f₀ f₂ f₃ h₁₂ h₁₃ h₂₃).pt = X

@[simp]

theorem SSet.horn₃₁.desc.multicofork_π_zero {X : SSet} (f₀ f₂ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₁₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₂) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₂ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₃) : (multicofork f₀ f₂ f₃ h₁₂ h₁₃ h₂₃).π ⟨0, multicofork_π_zero._proof_1⟩ = CategoryTheory.CategoryStruct.comp (stdSimplex.faceSingletonComplIso 0).inv f₀

theorem SSet.horn₃₁.desc.multicofork_π_zero_assoc {X : SSet} (f₀ f₂ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₁₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₂) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₂ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₃) {Z : SSet} (h : (multicofork f₀ f₂ f₃ h₁₂ h₁₃ h₂₃).pt ⟶ Z) : CategoryTheory.CategoryStruct.comp ((multicofork f₀ f₂ f₃ h₁₂ h₁₃ h₂₃).π ⟨0, multicofork_π_zero._proof_1⟩) h = CategoryTheory.CategoryStruct.comp (stdSimplex.faceSingletonComplIso 0).inv (CategoryTheory.CategoryStruct.comp f₀ h)

@[simp]

theorem SSet.horn₃₁.desc.multicofork_π_two {X : SSet} (f₀ f₂ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₁₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₂) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₂ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₃) : (multicofork f₀ f₂ f₃ h₁₂ h₁₃ h₂₃).π ⟨2, multicofork_π_two._proof_1⟩ = CategoryTheory.CategoryStruct.comp (stdSimplex.faceSingletonComplIso 2).inv f₂

theorem SSet.horn₃₁.desc.multicofork_π_two_assoc {X : SSet} (f₀ f₂ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₁₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₂) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₂ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₃) {Z : SSet} (h : (multicofork f₀ f₂ f₃ h₁₂ h₁₃ h₂₃).pt ⟶ Z) : CategoryTheory.CategoryStruct.comp ((multicofork f₀ f₂ f₃ h₁₂ h₁₃ h₂₃).π ⟨2, multicofork_π_two._proof_1⟩) h = CategoryTheory.CategoryStruct.comp (stdSimplex.faceSingletonComplIso 2).inv (CategoryTheory.CategoryStruct.comp f₂ h)

@[simp]

theorem SSet.horn₃₁.desc.multicofork_π_three {X : SSet} (f₀ f₂ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₁₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₂) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₂ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₃) : (multicofork f₀ f₂ f₃ h₁₂ h₁₃ h₂₃).π ⟨3, multicofork_π_three._proof_1⟩ = CategoryTheory.CategoryStruct.comp (stdSimplex.faceSingletonComplIso 3).inv f₃

theorem SSet.horn₃₁.desc.multicofork_π_three_assoc {X : SSet} (f₀ f₂ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₁₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₂) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₂ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₃) {Z : SSet} (h : (multicofork f₀ f₂ f₃ h₁₂ h₁₃ h₂₃).pt ⟶ Z) : CategoryTheory.CategoryStruct.comp ((multicofork f₀ f₂ f₃ h₁₂ h₁₃ h₂₃).π ⟨3, multicofork_π_three._proof_1⟩) h = CategoryTheory.CategoryStruct.comp (stdSimplex.faceSingletonComplIso 3).inv (CategoryTheory.CategoryStruct.comp f₃ h)

noncomputable def SSet.horn₃₁.desc {X : SSet} (f₀ f₂ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₁₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₂) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₂ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₃) : (horn 3 1).toSSet ⟶ X

The morphism Λ[3, 1] ⟶ X which is obtained by gluing three morphisms Δ[2] ⟶ X.

@[simp]

theorem SSet.horn₃₁.ι₀_desc {X : SSet} (f₀ f₂ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₁₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₂) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₂ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₃) : CategoryTheory.CategoryStruct.comp ι₀ (desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃) = f₀

@[simp]

theorem SSet.horn₃₁.ι₀_desc_assoc {X : SSet} (f₀ f₂ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₁₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₂) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₂ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₃) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp ι₀ (CategoryTheory.CategoryStruct.comp (desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃) h) = CategoryTheory.CategoryStruct.comp f₀ h

@[simp]

theorem SSet.horn₃₁.ι₂_desc {X : SSet} (f₀ f₂ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₁₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₂) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₂ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₃) : CategoryTheory.CategoryStruct.comp ι₂ (desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃) = f₂

@[simp]

theorem SSet.horn₃₁.ι₂_desc_assoc {X : SSet} (f₀ f₂ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₁₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₂) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₂ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₃) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp ι₂ (CategoryTheory.CategoryStruct.comp (desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃) h) = CategoryTheory.CategoryStruct.comp f₂ h

@[simp]

theorem SSet.horn₃₁.ι₃_desc {X : SSet} (f₀ f₂ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₁₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₂) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₂ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₃) : CategoryTheory.CategoryStruct.comp ι₃ (desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃) = f₃

@[simp]

theorem SSet.horn₃₁.ι₃_desc_assoc {X : SSet} (f₀ f₂ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₁₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₂) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₂ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₃) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp ι₃ (CategoryTheory.CategoryStruct.comp (desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃) h) = CategoryTheory.CategoryStruct.comp f₃ h

theorem SSet.horn₃₁.exists_desc {X : SSet} (f₀ f₂ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₁₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₂) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₂ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₃) : ∃ (φ : (horn 3 1).toSSet ⟶ X), CategoryTheory.CategoryStruct.comp ι₀ φ = f₀ ∧ CategoryTheory.CategoryStruct.comp ι₂ φ = f₂ ∧ CategoryTheory.CategoryStruct.comp ι₃ φ = f₃

@[reducible, inline]

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

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

@[reducible, inline]

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

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

@[reducible, inline]

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

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

def SSet.horn₃₂.desc.multicofork {X : SSet} (f₀ f₁ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₀₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₁ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₃) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₁) : CategoryTheory.Limits.Multicofork ((CompleteLattice.MulticoequalizerDiagram.multispanIndex ⋯).toLinearOrder.map Subcomplex.toSSetFunctor)

Auxiliary definition for desc.

@[simp]

theorem SSet.horn₃₂.desc.multicofork_pt {X : SSet} (f₀ f₁ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₀₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₁ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₃) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₁) : (multicofork f₀ f₁ f₃ h₀₂ h₁₂ h₂₃).pt = X

@[simp]

theorem SSet.horn₃₂.desc.multicofork_π_zero {X : SSet} (f₀ f₁ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₀₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₁ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₃) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₁) : (multicofork f₀ f₁ f₃ h₀₂ h₁₂ h₂₃).π ⟨0, multicofork_π_zero._proof_1⟩ = CategoryTheory.CategoryStruct.comp (stdSimplex.faceSingletonComplIso 0).inv f₀

theorem SSet.horn₃₂.desc.multicofork_π_zero_assoc {X : SSet} (f₀ f₁ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₀₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₁ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₃) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₁) {Z : SSet} (h : (multicofork f₀ f₁ f₃ h₀₂ h₁₂ h₂₃).pt ⟶ Z) : CategoryTheory.CategoryStruct.comp ((multicofork f₀ f₁ f₃ h₀₂ h₁₂ h₂₃).π ⟨0, multicofork_π_zero._proof_1⟩) h = CategoryTheory.CategoryStruct.comp (stdSimplex.faceSingletonComplIso 0).inv (CategoryTheory.CategoryStruct.comp f₀ h)

@[simp]

theorem SSet.horn₃₂.desc.multicofork_π_one {X : SSet} (f₀ f₁ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₀₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₁ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₃) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₁) : (multicofork f₀ f₁ f₃ h₀₂ h₁₂ h₂₃).π ⟨1, multicofork_π_one._proof_1⟩ = CategoryTheory.CategoryStruct.comp (stdSimplex.faceSingletonComplIso 1).inv f₁

theorem SSet.horn₃₂.desc.multicofork_π_one_assoc {X : SSet} (f₀ f₁ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₀₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₁ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₃) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₁) {Z : SSet} (h : (multicofork f₀ f₁ f₃ h₀₂ h₁₂ h₂₃).pt ⟶ Z) : CategoryTheory.CategoryStruct.comp ((multicofork f₀ f₁ f₃ h₀₂ h₁₂ h₂₃).π ⟨1, multicofork_π_one._proof_1⟩) h = CategoryTheory.CategoryStruct.comp (stdSimplex.faceSingletonComplIso 1).inv (CategoryTheory.CategoryStruct.comp f₁ h)

@[simp]

theorem SSet.horn₃₂.desc.multicofork_π_three {X : SSet} (f₀ f₁ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₀₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₁ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₃) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₁) : (multicofork f₀ f₁ f₃ h₀₂ h₁₂ h₂₃).π ⟨3, multicofork_π_three._proof_1⟩ = CategoryTheory.CategoryStruct.comp (stdSimplex.faceSingletonComplIso 3).inv f₃

theorem SSet.horn₃₂.desc.multicofork_π_three_assoc {X : SSet} (f₀ f₁ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₀₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₁ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₃) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₁) {Z : SSet} (h : (multicofork f₀ f₁ f₃ h₀₂ h₁₂ h₂₃).pt ⟶ Z) : CategoryTheory.CategoryStruct.comp ((multicofork f₀ f₁ f₃ h₀₂ h₁₂ h₂₃).π ⟨3, multicofork_π_three._proof_1⟩) h = CategoryTheory.CategoryStruct.comp (stdSimplex.faceSingletonComplIso 3).inv (CategoryTheory.CategoryStruct.comp f₃ h)

noncomputable def SSet.horn₃₂.desc {X : SSet} (f₀ f₁ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₀₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₁ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₃) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₁) : (horn 3 2).toSSet ⟶ X

The morphism Λ[3, 2] ⟶ X which is obtained by gluing three morphisms Δ[2] ⟶ X.

@[simp]

theorem SSet.horn₃₂.ι₀_desc {X : SSet} (f₀ f₁ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₀₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₁ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₃) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₁) : CategoryTheory.CategoryStruct.comp ι₀ (desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃) = f₀

@[simp]

theorem SSet.horn₃₂.ι₀_desc_assoc {X : SSet} (f₀ f₁ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₀₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₁ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₃) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₁) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp ι₀ (CategoryTheory.CategoryStruct.comp (desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃) h) = CategoryTheory.CategoryStruct.comp f₀ h

@[simp]

theorem SSet.horn₃₂.ι₁_desc {X : SSet} (f₀ f₁ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₀₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₁ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₃) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₁) : CategoryTheory.CategoryStruct.comp ι₁ (desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃) = f₁

@[simp]

theorem SSet.horn₃₂.ι₁_desc_assoc {X : SSet} (f₀ f₁ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₀₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₁ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₃) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₁) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp ι₁ (CategoryTheory.CategoryStruct.comp (desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃) h) = CategoryTheory.CategoryStruct.comp f₁ h

@[simp]

theorem SSet.horn₃₂.ι₃_desc {X : SSet} (f₀ f₁ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₀₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₁ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₃) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₁) : CategoryTheory.CategoryStruct.comp ι₃ (desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃) = f₃

@[simp]

theorem SSet.horn₃₂.ι₃_desc_assoc {X : SSet} (f₀ f₁ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₀₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₁ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₃) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₁) {Z : SSet} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp ι₃ (CategoryTheory.CategoryStruct.comp (desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃) h) = CategoryTheory.CategoryStruct.comp f₃ h

theorem SSet.horn₃₂.exists_desc {X : SSet} (f₀ f₁ f₃ : stdSimplex.obj (SimplexCategory.mk 2) ⟶ X) (h₀₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₁ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 1) f₃) (h₁₂ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 2) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₃) (h₂₃ : CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₀ = CategoryTheory.CategoryStruct.comp (stdSimplex.δ 0) f₁) : ∃ (φ : (horn 3 2).toSSet ⟶ X), CategoryTheory.CategoryStruct.comp ι₀ φ = f₀ ∧ CategoryTheory.CategoryStruct.comp ι₁ φ = f₁ ∧ CategoryTheory.CategoryStruct.comp ι₃ φ = f₃