arrowι — Mathlib

English

For F : Set.Iio i ⥤ C with i a limit element, and k < i, the arrowι F hi k hk is the canonical cocone arrow from the colimit to F at ⟨k, hk⟩, i.e., Arrow.mk (colimit.ι F ⟨k, hk⟩).

Русский

Для F : Set.Iio i ⥤ C, где i предельный элемент, и k < i, стрелкаι F hi k hk является канонической стрелкой конуса к колимиту к F(⟨k, hk⟩).

LaTeX

$$$ \\text{arrowι } F hi k hk = \\operatorname{Arrow.mk}(\\operatorname{colimit.ι} F ⟨k, hk⟩) $$$

Lean4

/-- Given `F : Set.Iio i ⥤ C`, with `i` a limit element, and `k` such that `hk : k < i`,
this is the map `colimit.ι F ⟨k, hk⟩`, as an element in `Arrow C`. -/
noncomputable def arrowι : Arrow C :=
  letI := hasColimitsOfShape_of_isSuccLimit C i hi
  Arrow.mk (colimit.ι F ⟨k, hk⟩)

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