Theorems · Definition · linear algebra

LinearEquiv.submoduleMap

{R : Type u_1} →
  {R₂ : Type u_3} →
    {M : Type u_5} →
      {M₂ : Type u_7} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                {module_M : Module R M} →
                  {module_M₂ : Module R₂ M₂} →
                    {σ₁₂ : R →+* R₂} →
                      {σ₂₁ : R₂ →+* R} →
                        {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} →
                          {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} →
                            (e : M ≃ₛₗ[σ₁₂] M₂) → (p : Submodule R M) → ↥p ≃ₛₗ[σ₁₂] ↥(Submodule.map (↑e) p)

A linear equivalence of two modules restricts to a linear equivalence from any submodule p of the domain onto the image of that submodule. This is the linear version of AddEquiv.submonoidMap and AddEquiv.subgroupMap. This is LinearEquiv.ofSubmodule' but with map on the right instead of comap on the left.

Defined in

Mathlib.Algebra.Module.Submodule.Map

Cited by

10 results in Mathlib

Foundations

Depth 30 from the axioms · uses propext, Quot.sound

Assumes

SemiringSemiringAddCommMonoidAddCommMonoid