arrowMap_ofCocone_to_top — Mathlib

English

For any i < j, the top-affecting map from i to the top is equal to the injection through the cocone's ι at i, composed with the isomorphism to the top membership and then the inverse of the top iso.

Русский

Для любого i < j отображение к верхней точке равно инъекции через ι кокона, сочетанной с изоморфизмом к верхнему элементу и обратным к верхнему изоморфизмом.

LaTeX

$$$\\text{map to top}_{i} = c.ι_{⟨i, \\_; \\rangle} \\circ \\mathrm{ofCoconeObjIsoPt}(i)^{-1}$$$

Lean4

theorem arrowMap_ofCocone_to_top (i : J) (hi : i < j) :
    arrowMap (ofCocone c) i j hi.le (by simp) = Arrow.mk (c.ι.app ⟨i, hi⟩) :=
  by
  rw [arrowMap, ofCocone_map_to_top _ _ hi]
  exact Arrow.ext (ofCocone_obj_eq _ _ _) (ofCocone_obj_eq_pt _) rfl

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