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.

Equations

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

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

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.

Equations

• SSet.horn.isColimit i = ⋯.isColimit'

@[reducible, inline]

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

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

Equations

• SSet.horn₃₁.ι₀ = SSet.horn.ι 1 0 SSet.horn₃₁.ι₀._proof_1

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

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

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

Equations

• SSet.horn₃₁.ι₃ = SSet.horn.ι 1 3 SSet.horn₃₁.ι₃._proof_1

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.

Equations

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

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

Equations

• SSet.horn₃₁.desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = (SSet.horn.isColimit 1).desc (SSet.horn₃₁.desc.multicofork f₀ f₂ f₃ h₁₂ h₁₃ 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

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

Equations

• SSet.horn₃₂.ι₀ = SSet.horn.ι 2 0 SSet.horn₃₂.ι₀._proof_1

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

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

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

Equations

• SSet.horn₃₂.ι₃ = SSet.horn.ι 2 3 SSet.horn₃₂.ι₃._proof_1

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.

Equations

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

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

Equations

• SSet.horn₃₂.desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = (SSet.horn.isColimit 2).desc (SSet.horn₃₂.desc.multicofork f₀ f₁ f₃ h₀₂ h₁₂ 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

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