map_self_succ — Mathlib

English

The map at j with successor j is equal to the composition of objIso, the given τ, and its iso inverse.

Русский

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

LaTeX

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

Lean4

theorem map_self_succ :
    map hj F τ j (Order.succ j) (Order.le_succ j) (by rfl) =
      (objIso F X ⟨j, by simp⟩).hom ≫ τ ≫ (objSuccIso hj F X).inv :=
  by
  dsimp [map]
  rw [dif_neg (by simpa only [Order.succ_le_iff_isMax] using hj), dif_pos (by rfl), Functor.map_id, comp_id, id_comp]

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