toModuleIso — Mathlib

English

For X,Y in ModuleCat R and f: X ⟶ Y, forget₂.map f = AddCommGrpCat.ofHom f.hom.

Русский

Для X,Y в ModuleCat R и f: X ⟶ Y, forget₂.map f = AddCommGrpCat.ofHom f.hom.

LaTeX

$$$ (\mathsf{forget}_2\;\mathrm{ModuleCat}\; R).map f = \mathrm{AddCommGrpCat}.ofHom (f.hom) $$$

Lean4

/-- Build an isomorphism in the category `Module R` from a `LinearEquiv` between `Module`s. -/
@[simps]
def toModuleIso {g₁ : AddCommGroup X₁} {g₂ : AddCommGroup X₂} {m₁ : Module R X₁} {m₂ : Module R X₂} (e : X₁ ≃ₗ[R] X₂) :
    ModuleCat.of R X₁ ≅ ModuleCat.of R X₂
    where
  hom := ofHom (e : X₁ →ₗ[R] X₂)
  inv := ofHom (e.symm : X₂ →ₗ[R] X₁)
  hom_inv_id := by ext; apply e.left_inv
  inv_hom_id := by ext; apply e.right_inv

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