toLinearEquiv — Mathlib

English

An isomorphism in ModuleCat R induces a linear equivalence between the underlying modules.

Русский

Изоморфизм в ModuleCat R индуцирует линейное эквивалентное отображение между основанными модулями.

LaTeX

$$$ \text{Iso}_{\mathrm{ModuleCat}}(X,Y) \to \mathrm{Equiv}_R(X,Y) $$$

Lean4

/-- Build a `LinearEquiv` from an isomorphism in the category `ModuleCat R`. -/
def toLinearEquiv {X Y : ModuleCat R} (i : X ≅ Y) : X ≃ₗ[R] Y :=
  LinearEquiv.ofLinear i.hom.hom i.inv.hom (by aesop) (by aesop)

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