XIsoOfEq_hom_naturality — Mathlib

English

For any φ: K ⟶ L and h: n = n', the equality holds: φ_f(n) ≫ (L.XIsoOfEq h).hom = (K.XIsoOfEq h).hom ≫ φ_f(n').

Русский

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

LaTeX

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

Lean4

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

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