isoToLinearEquiv — Mathlib

English

Isomorphisms in FGModuleCat correspond to linear isomorphisms between the underlying modules.

Русский

Изоморфизмы в FGModuleCat соответствуют линейным изоморфизмам между соответствующими модулевыми носителями.

LaTeX

$$$i: V\\cong W \\Rightarrow (i)_{\\mathrm{linear}}: V\\simeq_{R} W$$$

Lean4

/-- Converts an isomorphism in the category `FGModuleCat R` to
a `LinearEquiv` between the underlying modules. -/
def isoToLinearEquiv {V W : FGModuleCat.{v} R} (i : V ≅ W) : V ≃ₗ[R] W :=
  ((forget₂ (FGModuleCat.{v} R) (ModuleCat.{v} R)).mapIso i).toLinearEquiv

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