XIsoOfEq_inv_naturality — Mathlib

English

For any φ: K ⟶ L and h: n = n', the inverse naturality holds: φ.f n' ≫ (L.XIsoOfEq h).inv = (K.XIsoOfEq h).inv ≫ φ.f n.

Русский

Для любого φ: K ⟶ L и h: n = n' выполняется: φ.f n' ∘ (L.XIsoOfEq h).inv = (K.XIsoOfEq h).inv ∘ φ.f n.

LaTeX

$$$\\\\forall {K L} \\\\; (\\\\phi : K \\\\longrightarrow L) \\\\; {n n' : ι} \\\\; (h : n = n') \\\\Rightarrow \\\\; \\\\phi.f n' \\\\\\\\circ (L.XIsoOfEq h).inv = (K.XIsoOfEq h).inv \\\\\\\\circ \\\\phi.f n$$$

Lean4

@[reassoc]
theorem XIsoOfEq_inv_naturality {K L : HomologicalComplex V c} (φ : K ⟶ L) {n n' : ι} (h : n = n') :
    φ.f n' ≫ (L.XIsoOfEq h).inv = (K.XIsoOfEq h).inv ≫ φ.f n := by subst h; simp

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