toHom_comp — Mathlib

English

Composition of equivalences preserves the underlying Hom maps: (Equiv.comp g f).toHom = Hom.comp g.toHom f.toHom.

Русский

Композиция эквивалентностей сохраняет отображения Hom: (Equiv.comp g f).toHom = Hom.comp g.toHom f.toHom.

LaTeX

$$$(\mathrm{Equiv.comp}\; g\; f).toHom = \mathrm{Hom.comp}\; g.toHom\; f.toHom$$$

Lean4

@[simp]
theorem toHom_comp {ι₁ M₁ N₁ ι₂ M₂ N₂ : Type*} [AddCommGroup M₁] [Module R M₁] [AddCommGroup N₁] [Module R N₁]
    [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂] {P : RootPairing ι R M N}
    {P₁ : RootPairing ι₁ R M₁ N₁} {P₂ : RootPairing ι₂ R M₂ N₂} (g : RootPairing.Equiv P₁ P₂)
    (f : RootPairing.Equiv P P₁) : (Equiv.comp g f).toHom = Hom.comp g.toHom f.toHom := by rfl

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