def SSet.hornFaceIncl {n : ℕ} (i j : Fin (n + 2)) (h : j ≠ i) : stdSimplex.obj (SimplexCategory.mk n) ⟶ (horn (n + 1) i).toSSet

Equations

• SSet.hornFaceIncl i j h = SSet.yonedaEquiv.symm (SSet.horn.face i j h)

theorem SSet.horn_face_δ {n : ℕ} (i j : Fin (n + 2)) (h : j ≠ i) : CategoryTheory.CategoryStruct.comp (hornFaceIncl i j h) (horn (n + 1) i).ι = stdSimplex.δ j

Statements about the pushout Δ[0] → Δ[1] ↓ ↓ Δ[1] → Λ[2, 1] .

@[reducible, inline]

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

Equations

• SSet.horn₂₁.ι₀ = SSet.hornFaceIncl 1 0 SSet.horn₂₁.ι₀._proof_3

@[reducible, inline]

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

Equations

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

theorem SSet.horn₂₁.incl₀ : CategoryTheory.CategoryStruct.comp ι₀ (horn 2 1).ι = stdSimplex.δ 0

theorem SSet.horn₂₁.incl₂ : CategoryTheory.CategoryStruct.comp ι₂ (horn 2 1).ι = stdSimplex.δ 2

@[reducible, inline]

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

Equations

• SSet.horn₂₁.pt₀ = SSet.stdSimplex.map (SimplexCategory.δ 0)

@[reducible, inline]

abbrev SSet.horn₂₁.pt₁ : stdSimplex.obj (SimplexCategory.mk 0) ⟶ stdSimplex.obj (SimplexCategory.mk 1)

Equations

• SSet.horn₂₁.pt₁ = SSet.stdSimplex.map (SimplexCategory.δ 1)

theorem SSet.horn₂₁.sq_commutes : CategoryTheory.CategoryStruct.comp pt₁ ι₀ = CategoryTheory.CategoryStruct.comp pt₀ ι₂

def SSet.horn₂₁.pushout : CategoryTheory.Limits.PushoutCocone pt₁ pt₀

Equations

• SSet.horn₂₁.pushout = CategoryTheory.Limits.PushoutCocone.mk SSet.horn₂₁.ι₀ SSet.horn₂₁.ι₂ SSet.horn₂₁.sq_commutes

def SSet.horn₂₁.pushoutIsPushout : CategoryTheory.Limits.IsColimit pushout

Equations

• SSet.horn₂₁.pushoutIsPushout = sorry

Various constructions and statements about the (multi)coequalizer ⨿ Δ[1] ⇉ ⨿ Δ[2] → Λ[3, 1] (for more detail, see Goerss & Jardine Lemma 3.1)

@[reducible, inline]

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

Equations

• SSet.horn₃₁.ι₀ = SSet.hornFaceIncl 1 0 SSet.horn₃₁.ι₀._proof_3

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

theorem SSet.horn₃₁.incl₀ : CategoryTheory.CategoryStruct.comp ι₀ (horn 3 1).ι = stdSimplex.δ 0

theorem SSet.horn₃₁.incl₂ : CategoryTheory.CategoryStruct.comp ι₂ (horn 3 1).ι = stdSimplex.δ 2

theorem SSet.horn₃₁.incl₃ : CategoryTheory.CategoryStruct.comp ι₃ (horn 3 1).ι = stdSimplex.δ 3

inductive SSet.horn₃₁.L : Type

Index types for the left (indexed by the three edges attached to the vertex 1) and right (indexed by the three faces of Λ[3, 1]) coproducts in the coequalizer.

• e₀₁ : L
• e₁₂ : L
• e₁₃ : L

inductive SSet.horn₃₁.R : Type

• f₀ : R
• f₂ : R
• f₃ : R

def SSet.horn₃₁.J : CategoryTheory.Limits.MultispanShape

Equations

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

def SSet.horn₃₁.multispanIndex : CategoryTheory.Limits.MultispanIndex J SSet

The multispan is of the form ⨿ Δ[1] ⇉ ⨿ Δ[2] where the fst and snd maps Δ[1] ⟶ Δ[2] are chosen to be consistent to their layout in Λ[3, 1].

Equations

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

def SSet.horn₃₁.π : R → (stdSimplex.obj (SimplexCategory.mk 2) ⟶ (horn 3 1).toSSet)

Equations

• SSet.horn₃₁.π SSet.horn₃₁.R.f₀ = SSet.hornFaceIncl 1 0 SSet.horn₃₁.ι₀._proof_3
• SSet.horn₃₁.π SSet.horn₃₁.R.f₂ = SSet.hornFaceIncl 1 2 SSet.horn₃₁.π._proof_1
• SSet.horn₃₁.π SSet.horn₃₁.R.f₃ = SSet.hornFaceIncl 1 3 SSet.horn₃₁.π._proof_2

theorem SSet.horn₃₁.fork_comm (p : L) : CategoryTheory.CategoryStruct.comp (multispanIndex.fst p) (π (J.fst p)) = CategoryTheory.CategoryStruct.comp (multispanIndex.snd p) (π (J.snd p))

def SSet.horn₃₁.multicofork : CategoryTheory.Limits.Multicofork multispanIndex

Equations

• SSet.horn₃₁.multicofork = CategoryTheory.Limits.Multicofork.ofπ SSet.horn₃₁.multispanIndex (SSet.horn 3 1).toSSet SSet.horn₃₁.π SSet.horn₃₁.fork_comm

def SSet.horn₃₁.isMulticoeq : CategoryTheory.Limits.IsColimit multicofork

Equations

• SSet.horn₃₁.isMulticoeq = sorry

Various constructions and statements about the (multi)coequalizer ⨿ Δ[1] ⇉ ⨿ Δ[2] → Λ[3, 2] (for more detail, see Goerss & Jardine Lemma 3.1)

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

theorem SSet.horn₃₂.incl₀ : CategoryTheory.CategoryStruct.comp ι₀ (horn 3 2).ι = stdSimplex.δ 0

theorem SSet.horn₃₂.incl₁ : CategoryTheory.CategoryStruct.comp ι₁ (horn 3 2).ι = stdSimplex.δ 1

theorem SSet.horn₃₂.incl₃ : CategoryTheory.CategoryStruct.comp ι₃ (horn 3 2).ι = stdSimplex.δ 3

inductive SSet.horn₃₂.L : Type

Index types for the left (indexed by the three edges attached to the vertex 2) and right (indexed by the three faces of Λ[3, 2]) coproducts in the coequalizer.

• e₀₂ : L
• e₁₂ : L
• e₂₃ : L

inductive SSet.horn₃₂.R : Type

• f₀ : R
• f₁ : R
• f₃ : R

def SSet.horn₃₂.J : CategoryTheory.Limits.MultispanShape

Equations

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

def SSet.horn₃₂.multispanIndex : CategoryTheory.Limits.MultispanIndex J SSet

The multispan is of the form ⨿ Δ[1] ⇉ ⨿ Δ[2] where the fst and snd maps Δ[1] ⟶ Δ[2] are chosen to be consistent to their layout in Λ[3, 2].

Equations

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

def SSet.horn₃₂.π : R → (stdSimplex.obj (SimplexCategory.mk 2) ⟶ (horn 3 2).toSSet)

Equations

• SSet.horn₃₂.π SSet.horn₃₂.R.f₀ = SSet.hornFaceIncl 2 0 SSet.horn₃₂.π._proof_1
• SSet.horn₃₂.π SSet.horn₃₂.R.f₁ = SSet.hornFaceIncl 2 1 SSet.horn₃₂.π._proof_2
• SSet.horn₃₂.π SSet.horn₃₂.R.f₃ = SSet.hornFaceIncl 2 3 SSet.horn₃₂.π._proof_3

theorem SSet.horn₃₂.fork_comm (p : L) : CategoryTheory.CategoryStruct.comp (multispanIndex.fst p) (π (J.fst p)) = CategoryTheory.CategoryStruct.comp (multispanIndex.snd p) (π (J.snd p))

def SSet.horn₃₂.multicofork : CategoryTheory.Limits.Multicofork multispanIndex

Equations

• SSet.horn₃₂.multicofork = CategoryTheory.Limits.Multicofork.ofπ SSet.horn₃₂.multispanIndex (SSet.horn 3 2).toSSet SSet.horn₃₂.π SSet.horn₃₂.fork_comm

def SSet.horn₃₂.multicoforkIsMulticoeq : CategoryTheory.Limits.IsColimit multicofork

Equations

• SSet.horn₃₂.multicoforkIsMulticoeq = sorry