linearEquivIsoModuleIso — Mathlib

English

A linear equivalence between modules yields an isomorphism in ModuleCat.

Русский

Линейное эквивалентное отображение между модулями даёт изоморфизм в ModuleCat.

LaTeX

$$$ e: X \simeq_\mathrm{lin} Y \quad\Rightarrow\quad X \cong Y \text{ in ModuleCat}$$$

Lean4

/-- linear equivalences between `Module`s are the same as (isomorphic to) isomorphisms
in `ModuleCat` -/
@[simps]
def linearEquivIsoModuleIso {X Y : Type u} [AddCommGroup X] [AddCommGroup Y] [Module R X] [Module R Y] :
    (X ≃ₗ[R] Y) ≅ ModuleCat.of R X ≅ ModuleCat.of R Y
    where
  hom e := e.toModuleIso
  inv i := i.toLinearEquiv

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