ιIterationFunctor — Mathlib

English

For j not maximal, the object at Order.succ j is isomorphic to the successor of the previous stage: (Φ.iterationFunctor J).obj (Order.succ j) ≅ Φ.succ ((Φ.iterationFunctor J).obj j).

Русский

Для не максимального j объект в Order.succ j изоморфен предшествующей стадии: (Φ.iterationFunctor J).obj (Order.succ j) ≅ Φ.succ ((Φ.iterationFunctor J).obj j).

LaTeX

$$$(Φ.iterationFunctor J).obj (Order.succ j) \\cong Φ.succ ((Φ.iterationFunctor J).obj j)$$$

Lean4

/-- The natural map `Φ.X₀ ⟶ (Φ.iterationFunctor J).obj j`. -/
noncomputable def ιIterationFunctor : (Functor.const _).obj Φ.X₀ ⟶ Φ.iterationFunctor J
    where
  app j := (Φ.iterationFunctorObjBotIso J).inv ≫ (Φ.iterationFunctor J).map (homOfLE bot_le : ⊥ ⟶ j)
  naturality _ _
    f := by
    dsimp
    rw [id_comp, assoc, ← Functor.map_comp]
    rfl

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