ιIteration — Mathlib

English

The canonical morphism ιIteration : Φ.X0 → Φ.iteration J is defined as the inverse of the BotIso composed with the colimit inclusion at ⊥: ιIteration = (Φ.iterationFunctorObjBotIso J)^{-1} ∘ colim_⊥.

Русский

Каноническое отображение ιIteration: Φ.X0 → Φ.iteration J задаётся как композиция (Φ.iterationFunctorObjBotIso J)^{-1} с инклудом колимита на ⊥.

LaTeX

$$$\\iota_{Iteration} = (\\Phi.iterationFunctorObjBotIso\\; J)^{-1} \\circ \\mathrm{colim}_{\\perp}$$$

Lean4

/-- The canonical map `Φ.X₀ ⟶ Φ.iteration J` which is the `J`th-transfinite composition
of maps `Φ.toSucc`. -/
noncomputable def ιIteration : Φ.X₀ ⟶ Φ.iteration J :=
  (Φ.iterationFunctorObjBotIso J).inv ≫ colimit.ι _ ⊥

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