extendToSuccObjIso_hom_naturality

English

The map from j to successor j reduces to the composed isomorphism and τ.

Русский

Отображение от j к successor j равно композиции из изоморфизма и τ.

LaTeX

$$$\\text{map}\\; hj\\; F\\; τ\\; j\\; (Order.succ j) = (\\text{objIso}\\; F\\; X \\⟨j, \\_⟩).hom \\circ τ \\circ (\\text{objSuccIso}\\; hj\\; F\\; X)^{-1}$$$

Lean4

@[reassoc]
theorem extendToSuccObjIso_hom_naturality (i₁ i₂ : J) (hi : i₁ ≤ i₂) (hi₂ : i₂ ≤ j) :
    (extendToSucc hj F τ).map
          (homOfLE hi : ⟨i₁, hi.trans (hi₂.trans (Order.le_succ j))⟩ ⟶ ⟨i₂, hi₂.trans (Order.le_succ j)⟩) ≫
        (extendToSuccObjIso hj F τ i₂ hi₂).hom =
      (extendToSuccObjIso hj F τ i₁ (hi.trans hi₂)).hom ≫ F.map (homOfLE hi) :=
  by
  dsimp [extendToSucc, extendToSuccObjIso]
  rw [extendToSucc.map_eq _ _ _ _ _ _ hi₂, assoc, assoc, Iso.inv_hom_id, comp_id]

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