Documentation

Mathlib.Algebra.Module.Submodule.Map

map and comap for Submodules #

Main declarations #

Tags #

submodule, subspace, linear map, pushforward, pullback

def Submodule.map {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (p : Submodule R M) :
Submodule R₂ M₂

The pushforward of a submodule p ⊆ M by f : M → M₂

Equations
Instances For
    @[simp]
    theorem Submodule.map_coe {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (p : Submodule R M) :
    (Submodule.map f p) = f '' p
    theorem Submodule.map_toAddSubmonoid {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M) :
    (Submodule.map f p).toAddSubmonoid = AddSubmonoid.map (f) p.toAddSubmonoid
    theorem Submodule.map_toAddSubmonoid' {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (p : Submodule R M) :
    (Submodule.map f p).toAddSubmonoid = AddSubmonoid.map f p.toAddSubmonoid
    @[simp]
    theorem AddMonoidHom.coe_toIntLinearMap_map {A : Type u_10} {A₂ : Type u_11} [AddCommGroup A] [AddCommGroup A₂] (f : A →+ A₂) (s : AddSubgroup A) :
    Submodule.map f.toIntLinearMap (AddSubgroup.toIntSubmodule s) = AddSubgroup.toIntSubmodule (AddSubgroup.map f s)
    @[simp]
    theorem MonoidHom.coe_toAdditive_map {G : Type u_10} {G₂ : Type u_11} [Group G] [Group G₂] (f : G →* G₂) (s : Subgroup G) :
    AddSubgroup.map (MonoidHom.toAdditive f) (Subgroup.toAddSubgroup s) = Subgroup.toAddSubgroup (Subgroup.map f s)
    @[simp]
    theorem AddMonoidHom.coe_toMultiplicative_map {G : Type u_10} {G₂ : Type u_11} [AddGroup G] [AddGroup G₂] (f : G →+ G₂) (s : AddSubgroup G) :
    Subgroup.map (AddMonoidHom.toMultiplicative f) (AddSubgroup.toSubgroup s) = AddSubgroup.toSubgroup (AddSubgroup.map f s)
    @[simp]
    theorem Submodule.mem_map {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {f : F} {p : Submodule R M} {x : M₂} :
    x Submodule.map f p yp, f y = x
    theorem Submodule.mem_map_of_mem {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {f : F} {p : Submodule R M} {r : M} (h : r p) :
    theorem Submodule.apply_coe_mem_map {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) {p : Submodule R M} (r : p) :
    f r Submodule.map f p
    @[simp]
    theorem Submodule.map_id {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) :
    Submodule.map LinearMap.id p = p
    theorem Submodule.map_comp {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_5} {M₂ : Type u_7} {M₃ : Type u_8} [Semiring R] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomSurjective σ₁₂] [RingHomSurjective σ₂₃] [RingHomSurjective σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (p : Submodule R M) :
    theorem Submodule.map_mono {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {f : F} {p : Submodule R M} {p' : Submodule R M} :
    @[simp]
    theorem Submodule.map_zero {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (p : Submodule R M) [RingHomSurjective σ₁₂] :
    theorem Submodule.map_add_le {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (p : Submodule R M) [RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (g : M →ₛₗ[σ₁₂] M₂) :
    theorem Submodule.map_inf_le {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) {p : Submodule R M} {q : Submodule R M} :
    theorem Submodule.map_inf {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) {p : Submodule R M} {q : Submodule R M} (hf : Function.Injective f) :
    theorem Submodule.range_map_nonempty {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] (N : Submodule R M) :
    (Set.range fun (ϕ : M →ₛₗ[σ₁₂] M₂) => Submodule.map ϕ N).Nonempty
    noncomputable def Submodule.equivMapOfInjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (i : Function.Injective f) (p : Submodule R M) :
    p ≃ₛₗ[σ₁₂] (Submodule.map f p)

    The pushforward of a submodule by an injective linear map is linearly equivalent to the original submodule. See also LinearEquiv.submoduleMap for a computable version when f has an explicit inverse.

    Equations
    Instances For
      @[simp]
      theorem Submodule.coe_equivMapOfInjective_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (i : Function.Injective f) (p : Submodule R M) (x : p) :
      ((Submodule.equivMapOfInjective f i p) x) = f x
      @[simp]
      theorem Submodule.map_equivMapOfInjective_symm_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (i : Function.Injective f) (p : Submodule R M) (x : (Submodule.map f p)) :
      f ((Submodule.equivMapOfInjective f i p).symm x) = x
      def Submodule.comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (p : Submodule R₂ M₂) :

      The pullback of a submodule p ⊆ M₂ along f : M → M₂

      Equations
      Instances For
        @[simp]
        theorem Submodule.comap_coe {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (p : Submodule R₂ M₂) :
        (Submodule.comap f p) = f ⁻¹' p
        @[simp]
        theorem Submodule.AddMonoidHom.coe_toIntLinearMap_comap {A : Type u_10} {A₂ : Type u_11} [AddCommGroup A] [AddCommGroup A₂] (f : A →+ A₂) (s : AddSubgroup A₂) :
        Submodule.comap f.toIntLinearMap (AddSubgroup.toIntSubmodule s) = AddSubgroup.toIntSubmodule (AddSubgroup.comap f s)
        @[simp]
        theorem Submodule.mem_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {x : M} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {f : F} {p : Submodule R₂ M₂} :
        @[simp]
        theorem Submodule.comap_id {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) :
        Submodule.comap LinearMap.id p = p
        theorem Submodule.comap_comp {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_5} {M₂ : Type u_7} {M₃ : Type u_8} [Semiring R] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (p : Submodule R₃ M₃) :
        theorem Submodule.comap_mono {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {f : F} {q : Submodule R₂ M₂} {q' : Submodule R₂ M₂} :
        theorem Submodule.le_comap_pow_of_le_comap {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) {f : M →ₗ[R] M} (h : p Submodule.comap f p) (k : ) :
        theorem Submodule.map_le_iff_le_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} {p : Submodule R M} {q : Submodule R₂ M₂} :
        theorem Submodule.gc_map_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) :
        @[simp]
        theorem Submodule.map_bot {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) :
        @[simp]
        theorem Submodule.map_sup {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (p : Submodule R M) (p' : Submodule R M) {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) :
        @[simp]
        theorem Submodule.map_iSup {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {ι : Sort u_10} (f : F) (p : ιSubmodule R M) :
        Submodule.map f (⨆ (i : ι), p i) = ⨆ (i : ι), Submodule.map f (p i)
        @[simp]
        theorem Submodule.comap_top {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) :
        @[simp]
        theorem Submodule.comap_inf {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (q : Submodule R₂ M₂) (q' : Submodule R₂ M₂) {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) :
        @[simp]
        theorem Submodule.comap_iInf {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {ι : Sort u_10} (f : F) (p : ιSubmodule R₂ M₂) :
        Submodule.comap f (⨅ (i : ι), p i) = ⨅ (i : ι), Submodule.comap f (p i)
        @[simp]
        theorem Submodule.comap_zero {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (q : Submodule R₂ M₂) :
        theorem Submodule.map_comap_le {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) (q : Submodule R₂ M₂) :
        theorem Submodule.le_comap_map {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) (p : Submodule R M) :
        def Submodule.giMapComap {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {f : F} (hf : Function.Surjective f) [RingHomSurjective σ₁₂] :

        map f and comap f form a GaloisInsertion when f is surjective.

        Equations
        Instances For
          theorem Submodule.map_comap_eq_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {f : F} (hf : Function.Surjective f) [RingHomSurjective σ₁₂] (p : Submodule R₂ M₂) :
          theorem Submodule.map_surjective_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {f : F} (hf : Function.Surjective f) [RingHomSurjective σ₁₂] :
          theorem Submodule.comap_injective_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {f : F} (hf : Function.Surjective f) [RingHomSurjective σ₁₂] :
          theorem Submodule.map_sup_comap_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {f : F} (hf : Function.Surjective f) [RingHomSurjective σ₁₂] (p : Submodule R₂ M₂) (q : Submodule R₂ M₂) :
          theorem Submodule.map_iSup_comap_of_sujective {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {f : F} (hf : Function.Surjective f) [RingHomSurjective σ₁₂] {ι : Sort u_10} (S : ιSubmodule R₂ M₂) :
          Submodule.map f (⨆ (i : ι), Submodule.comap f (S i)) = iSup S
          theorem Submodule.map_inf_comap_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {f : F} (hf : Function.Surjective f) [RingHomSurjective σ₁₂] (p : Submodule R₂ M₂) (q : Submodule R₂ M₂) :
          theorem Submodule.map_iInf_comap_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {f : F} (hf : Function.Surjective f) [RingHomSurjective σ₁₂] {ι : Sort u_10} (S : ιSubmodule R₂ M₂) :
          Submodule.map f (⨅ (i : ι), Submodule.comap f (S i)) = iInf S
          theorem Submodule.comap_le_comap_iff_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {f : F} (hf : Function.Surjective f) [RingHomSurjective σ₁₂] (p : Submodule R₂ M₂) (q : Submodule R₂ M₂) :
          theorem Submodule.comap_strictMono_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {f : F} (hf : Function.Surjective f) [RingHomSurjective σ₁₂] :
          def Submodule.gciMapComap {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective f) :

          map f and comap f form a GaloisCoinsertion when f is injective.

          Equations
          Instances For
            theorem Submodule.comap_map_eq_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective f) (p : Submodule R M) :
            theorem Submodule.comap_surjective_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective f) :
            theorem Submodule.map_injective_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective f) :
            theorem Submodule.comap_inf_map_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective f) (p : Submodule R M) (q : Submodule R M) :
            theorem Submodule.comap_iInf_map_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective f) {ι : Sort u_10} (S : ιSubmodule R M) :
            Submodule.comap f (⨅ (i : ι), Submodule.map f (S i)) = iInf S
            theorem Submodule.comap_sup_map_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective f) (p : Submodule R M) (q : Submodule R M) :
            theorem Submodule.comap_iSup_map_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective f) {ι : Sort u_10} (S : ιSubmodule R M) :
            Submodule.comap f (⨆ (i : ι), Submodule.map f (S i)) = iSup S
            theorem Submodule.map_le_map_iff_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective f) (p : Submodule R M) (q : Submodule R M) :
            theorem Submodule.map_strictMono_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Injective f) :
            @[simp]
            theorem Submodule.orderIsoMapComapOfBijective_symm_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (hf : Function.Bijective f) (p : Submodule R₂ M₂) :
            @[simp]
            theorem Submodule.orderIsoMapComapOfBijective_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (hf : Function.Bijective f) (p : Submodule R M) :
            def Submodule.orderIsoMapComapOfBijective {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (hf : Function.Bijective f) :
            Submodule R M ≃o Submodule R₂ M₂

            A linear isomorphism induces an order isomorphism of submodules.

            Equations
            Instances For
              @[simp]
              theorem Submodule.orderIsoMapComap_symm_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] {F : Type u_9} [EquivLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (p : Submodule R₂ M₂) :
              @[simp]
              theorem Submodule.orderIsoMapComap_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] {F : Type u_9} [EquivLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (p : Submodule R M) :
              def Submodule.orderIsoMapComap {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [RingHomSurjective σ₁₂] {F : Type u_9} [EquivLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) :
              Submodule R M ≃o Submodule R₂ M₂

              A linear isomorphism induces an order isomorphism of submodules.

              Equations
              Instances For
                theorem Submodule.map_inf_eq_map_inf_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} {p : Submodule R M} {p' : Submodule R₂ M₂} :
                @[simp]
                theorem Submodule.map_comap_subtype {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (p' : Submodule R M) :
                Submodule.map p.subtype (Submodule.comap p.subtype p') = p p'
                theorem Submodule.eq_zero_of_bot_submodule {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (b : ) :
                b = 0
                theorem LinearMap.iInf_invariant {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {σ : R →+* R} [RingHomSurjective σ] {ι : Sort u_10} (f : M →ₛₗ[σ] M) {p : ιSubmodule R M} (hf : ∀ (i : ι), vp i, f v p i) (v : M) :
                v iInf pf v iInf p

                The infimum of a family of invariant submodule of an endomorphism is also an invariant submodule.

                theorem Submodule.disjoint_iff_comap_eq_bot {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R M} :
                Disjoint p q Submodule.comap p.subtype q =
                @[simp]
                theorem Submodule.map_neg {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) [AddCommGroup M₂] [Module R M₂] (f : M →ₗ[R] M₂) :
                @[simp]
                theorem Submodule.comap_neg {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R M₂] {f : M →ₗ[R] M₂} {p : Submodule R M₂} :
                theorem Submodule.comap_smul {K : Type u_9} {V : Type u_10} {V₂ : Type u_11} [Semifield K] [AddCommMonoid V] [Module K V] [AddCommMonoid V₂] [Module K V₂] (f : V →ₗ[K] V₂) (p : Submodule K V₂) (a : K) (h : a 0) :
                theorem Submodule.map_smul {K : Type u_9} {V : Type u_10} {V₂ : Type u_11} [Semifield K] [AddCommMonoid V] [Module K V] [AddCommMonoid V₂] [Module K V₂] (f : V →ₗ[K] V₂) (p : Submodule K V) (a : K) (h : a 0) :
                theorem Submodule.comap_smul' {K : Type u_9} {V : Type u_10} {V₂ : Type u_11} [Semifield K] [AddCommMonoid V] [Module K V] [AddCommMonoid V₂] [Module K V₂] (f : V →ₗ[K] V₂) (p : Submodule K V₂) (a : K) :
                Submodule.comap (a f) p = ⨅ (_ : a 0), Submodule.comap f p
                theorem Submodule.map_smul' {K : Type u_9} {V : Type u_10} {V₂ : Type u_11} [Semifield K] [AddCommMonoid V] [Module K V] [AddCommMonoid V₂] [Module K V₂] (f : V →ₗ[K] V₂) (p : Submodule K V) (a : K) :
                Submodule.map (a f) p = ⨆ (_ : a 0), Submodule.map f p
                @[simp]
                theorem Submodule.comapSubtypeEquivOfLe_symm_apply {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R M} (hpq : p q) (x : p) :
                (Submodule.comapSubtypeEquivOfLe hpq).symm x = x, ,
                def Submodule.comapSubtypeEquivOfLe {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R M} (hpq : p q) :
                (Submodule.comap q.subtype p) ≃ₗ[R] p

                If s ≤ t, then we can view s as a submodule of t by taking the comap of t.subtype.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem Submodule.comapSubtypeEquivOfLe_apply_coe {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R M} (hpq : p q) (x : (Submodule.comap q.subtype p)) :
                  ((Submodule.comapSubtypeEquivOfLe hpq) x) = x
                  @[simp]
                  theorem Submodule.mem_map_equiv {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] (p : Submodule R M) {e : M ≃ₛₗ[τ₁₂] M₂} {x : M₂} :
                  x Submodule.map (e) p e.symm x p
                  theorem Submodule.map_equiv_eq_comap_symm {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] (e : M ≃ₛₗ[τ₁₂] M₂) (K : Submodule R M) :
                  Submodule.map (e) K = Submodule.comap (e.symm) K
                  theorem Submodule.comap_equiv_eq_map_symm {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] (e : M ≃ₛₗ[τ₁₂] M₂) (K : Submodule R₂ M₂) :
                  Submodule.comap (e) K = Submodule.map (e.symm) K
                  theorem Submodule.map_symm_eq_iff {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] {p : Submodule R M} (e : M ≃ₛₗ[τ₁₂] M₂) {K : Submodule R₂ M₂} :
                  Submodule.map e.symm K = p Submodule.map e p = K
                  theorem Submodule.orderIsoMapComap_apply' {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] (e : M ≃ₛₗ[τ₁₂] M₂) (p : Submodule R M) :
                  theorem Submodule.orderIsoMapComap_symm_apply' {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] (e : M ≃ₛₗ[τ₁₂] M₂) (p : Submodule R₂ M₂) :
                  theorem Submodule.inf_comap_le_comap_add {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (q : Submodule R₂ M₂) (f₁ : M →ₛₗ[τ₁₂] M₂) (f₂ : M →ₛₗ[τ₁₂] M₂) :
                  theorem Submodule.comap_le_comap_smul {R : Type u_1} {N : Type u_9} {N₂ : Type u_10} [CommSemiring R] [AddCommMonoid N] [AddCommMonoid N₂] [Module R N] [Module R N₂] (qₗ : Submodule R N₂) (fₗ : N →ₗ[R] N₂) (c : R) :
                  Submodule.comap fₗ qₗ Submodule.comap (c fₗ) qₗ
                  def Submodule.compatibleMaps {R : Type u_1} {N : Type u_9} {N₂ : Type u_10} [CommSemiring R] [AddCommMonoid N] [AddCommMonoid N₂] [Module R N] [Module R N₂] (pₗ : Submodule R N) (qₗ : Submodule R N₂) :
                  Submodule R (N →ₗ[R] N₂)

                  Given modules M, M₂ over a commutative ring, together with submodules p ⊆ M, q ⊆ M₂, the set of maps $\{f ∈ Hom(M, M₂) | f(p) ⊆ q \}$ is a submodule of Hom(M, M₂).

                  Equations
                  • pₗ.compatibleMaps qₗ = { carrier := {fₗ : N →ₗ[R] N₂ | pₗ Submodule.comap fₗ qₗ}, add_mem' := , zero_mem' := , smul_mem' := }
                  Instances For
                    def LinearMap.submoduleMap {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] (f : M →ₗ[R] M₁) (p : Submodule R M) :
                    p →ₗ[R] (Submodule.map f p)

                    A linear map between two modules restricts to a linear map from any submodule p of the domain onto the image of that submodule.

                    This is the linear version of AddMonoidHom.addSubmonoidMap and AddMonoidHom.addSubgroupMap.

                    Equations
                    • f.submoduleMap p = f.restrict
                    Instances For
                      @[simp]
                      theorem LinearMap.submoduleMap_coe_apply {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] (f : M →ₗ[R] M₁) {p : Submodule R M} (x : p) :
                      ((f.submoduleMap p) x) = f x
                      theorem LinearMap.submoduleMap_surjective {R : Type u_1} {M : Type u_5} {M₁ : Type u_6} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₁] [Module R M] [Module R M₁] (f : M →ₗ[R] M₁) (p : Submodule R M) :
                      Function.Surjective (f.submoduleMap p)
                      theorem LinearMap.map_codRestrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {σ₂₁ : R₂ →+* R} [RingHomSurjective σ₂₁] (p : Submodule R M) (f : M₂ →ₛₗ[σ₂₁] M) (h : ∀ (c : M₂), f c p) (p' : Submodule R₂ M₂) :
                      theorem LinearMap.comap_codRestrict {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {σ₂₁ : R₂ →+* R} (p : Submodule R M) (f : M₂ →ₛₗ[σ₂₁] M) (hf : ∀ (c : M₂), f c p) (p' : Submodule R p) :

                      Linear equivalences #

                      theorem LinearEquiv.map_eq_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [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} :
                      Submodule.map (e) p = Submodule.comap (e.symm) p
                      def LinearEquiv.submoduleMap {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [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.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]
                        theorem LinearEquiv.submoduleMap_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [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) (x : p) :
                        ((e.submoduleMap p) x) = e x
                        @[simp]
                        theorem LinearEquiv.submoduleMap_symm_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [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) (x : (Submodule.map (e) p)) :
                        ((e.submoduleMap p).symm x) = e.symm x