splitEpiσ — Mathlib

English

The morphism σ_i is a split epimorphism with a section δ_i.castSucc and δ_i.castSucc ≫ σ_i = id.

Русский

Морфизм σ_i является разложимым эпиморфизмом с секцией δ_i.castSucc и δ_i.castSucc ≫ σ_i = id.

LaTeX

$$$\mathrm{SplitEpi}(\sigma_i)$ with $\delta_i^{\mathrm{castSucc}}$ as a section and $\delta_i^{\mathrm{castSucc}} \circ \sigma_i = \mathrm{id}$$$

Lean4

/-- `δ i` is a split epimorphism thanks to the simplicial identities. -/
def splitEpiσ {n : ℕ} (i : Fin (n + 1)) : SplitEpi (σ i)
    where
  section_ := δ i.castSucc
  id := δ_comp_σ_self

Похожие утверждения