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) :
      (map f p) = f '' p
      @[simp]
      theorem Submodule.map_coe_toLinearMap {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) :
      map (↑f) p = map 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) :
      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) :
      @[simp]
      @[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 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) :
      f r map f 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 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) :
      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) :
      map (g ∘ₛₗ f) p = map g (map f p)
      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 p' : Submodule R M} :
      p p'map f p map f p'
      @[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 σ₁₂] :
      map 0 p =
      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 g : M →ₛₗ[σ₁₂] M₂) :
      map (f + g) p map f pmap g p
      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 q : Submodule R M} :
      map f (pq) map f pmap f q
      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 q : Submodule R M} (hf : Function.Injective f) :
      map f (pq) = map f pmap f q
      theorem Submodule.map_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₂} [RingHomSurjective σ₁₂] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {ι : Type u_10} [Nonempty ι] {p : ιSubmodule R M} (f : F) (hf : Function.Injective f) :
      map f (⨅ (i : ι), p i) = ⨅ (i : ι), map f (p i)
      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₂) => 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 ≃ₛₗ[σ₁₂] (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) :
          ((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 : (map f p)) :
          f ((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₂) :
              (comap f p) = f ⁻¹' p
              @[simp]
              theorem Submodule.comap_coe_toLinearMap {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₂) :
              comap (↑f) p = comap f p
              @[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₂} :
              x comap f p f x p
              @[simp]
              theorem Submodule.comap_id {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) :
              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₃) :
              comap (g ∘ₛₗ f) p = comap f (comap g p)
              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 q' : Submodule R₂ M₂} :
              q q'comap f q comap f q'
              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 comap f p) (k : ) :
              p comap (f ^ k) p
              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₂} :
              map f p q p comap f q
              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 p' : Submodule R M) {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) :
              map f (pp') = map f pmap f p'
              @[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) :
              map f (⨆ (i : ι), p i) = ⨆ (i : ι), 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 q' : Submodule R₂ M₂) {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) :
              comap f (qq') = comap f qcomap f q'
              @[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₂) :
              comap f (⨅ (i : ι), p i) = ⨅ (i : ι), 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₂) :
              comap 0 q =
              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₂) :
              map f (comap f q) q
              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) :
              p comap f (map f p)
              def Submodule.submoduleOf {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (p q : Submodule R M) :
              Submodule R q

              For any R submodules p and q, p ⊓ q as a submodule of q.

              Equations
                Instances For
                  def Submodule.submoduleOfEquivOfLe {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {p q : Submodule R M} (h : p q) :
                  (p.submoduleOf q) ≃ₗ[R] p

                  If p ≤ q, then p as a subgroup of q is isomorphic to p.

                  Equations
                    Instances For
                      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₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Surjective f) :

                      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₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Surjective f) (p : Submodule R₂ M₂) :
                          map f (comap f p) = p
                          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₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Surjective f) :
                          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₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Surjective f) :
                          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₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Surjective f) (p q : Submodule R₂ M₂) :
                          map f (comap f pcomap f q) = pq
                          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₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Surjective f) {ι : Sort u_10} (S : ιSubmodule R₂ M₂) :
                          map f (⨆ (i : ι), 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₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Surjective f) (p q : Submodule R₂ M₂) :
                          map f (comap f pcomap f q) = pq
                          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₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Surjective f) {ι : Sort u_10} (S : ιSubmodule R₂ M₂) :
                          map f (⨅ (i : ι), 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₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Surjective f) {p q : Submodule R₂ M₂} :
                          comap f p comap f q p q
                          theorem Submodule.comap_lt_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₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Surjective f) {p q : Submodule R₂ M₂} :
                          comap f p < comap f q p < q
                          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₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Surjective f) :
                          theorem Submodule.le_map_of_comap_le_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₂} {p : Submodule R M} {q : Submodule R₂ M₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Surjective f) (h : comap f q p) :
                          q map f p
                          theorem Submodule.lt_map_of_comap_lt_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₂} {p : Submodule R M} {q : Submodule R₂ M₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} (hf : Function.Surjective f) (h : comap f q < p) :
                          q < map f p
                          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) :
                              comap f (map f p) = p
                              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 q : Submodule R M) :
                              comap f (map f pmap f q) = pq
                              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) :
                              comap f (⨅ (i : ι), 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 q : Submodule R M) :
                              comap f (map f pmap f q) = pq
                              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) :
                              comap f (⨆ (i : ι), 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 q : Submodule R M) :
                              map f p map f q p q
                              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) :
                              theorem Submodule.map_lt_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 q : Submodule R M} :
                              map f p < map f q p < q
                              theorem Submodule.comap_lt_of_lt_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₂} (h : q < map f p) :
                              comap f q < p
                              theorem Submodule.map_covBy_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 q : Submodule R M} (h : p q) :
                              map f p map f q
                              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.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.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
                                      @[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) :
                                      @[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.map_eq_bot_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₂} {p : Submodule R M} [RingHomSurjective σ₁₂] {F : Type u_9} [EquivLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {e : F} :
                                      map e p = p =
                                      @[simp]
                                      theorem Submodule.map_eq_top_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₂} {p : Submodule R M} [RingHomSurjective σ₁₂] {F : Type u_9} [EquivLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {e : F} :
                                      map e p = p =
                                      theorem Submodule.map_ne_bot_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₂} {p : Submodule R M} [RingHomSurjective σ₁₂] {F : Type u_9} [EquivLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {e : F} :
                                      theorem Submodule.map_ne_top_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₂} {p : Submodule R M} [RingHomSurjective σ₁₂] {F : Type u_9} [EquivLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {e : F} :
                                      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₂} :
                                      map f pp' = map f (pcomap f p')
                                      @[simp]
                                      theorem Submodule.map_comap_subtype {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (p p' : Submodule R M) :
                                      map p.subtype (comap p.subtype p') = pp'
                                      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 q : Submodule R M} :
                                      @[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₂) :
                                      map (-f) p = map f p
                                      @[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₂} :
                                      comap (-f) p = comap f p
                                      theorem Submodule.map_toAddSubgroup {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) :
                                      comap (a f) p = 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) (h : a 0) :
                                      map (a f) p = map f p
                                      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) :
                                      comap (a f) p = ⨅ (_ : a 0), 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) :
                                      map (a f) p = ⨆ (_ : a 0), map f p
                                      def Submodule.comapSubtypeEquivOfLe {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {p q : Submodule R M} (hpq : p q) :
                                      (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
                                        Instances For
                                          @[simp]
                                          theorem Submodule.comapSubtypeEquivOfLe_symm_apply {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {p q : Submodule R M} (hpq : p q) (x : p) :
                                          @[simp]
                                          theorem Submodule.comapSubtypeEquivOfLe_apply_coe {R : Type u_1} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {p q : Submodule R M} (hpq : p q) (x : (comap q.subtype p)) :
                                          ((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 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) :
                                          map (↑e) K = 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₂) :
                                          comap (↑e) K = 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₂} :
                                          map e.symm K = p 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₁ f₂ : M →ₛₗ[τ₁₂] M₂) :
                                          comap f₁ qcomap f₂ q comap (f₁ + f₂) q
                                          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) :
                                          comap fₗ qₗ 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
                                            Instances For
                                              def LinearMap.submoduleComap {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₁) (q : Submodule R M₁) :
                                              (Submodule.comap f q) →ₗ[R] q

                                              The LinearMap from the preimage of a submodule to itself.

                                              This is the linear version of AddMonoidHom.addSubmonoidComap and AddMonoidHom.addSubgroupComap.

                                              Equations
                                                Instances For
                                                  @[simp]
                                                  theorem LinearMap.submoduleComap_apply_coe {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₁) (q : Submodule R M₁) (c : (Submodule.comap f q)) :
                                                  ((f.submoduleComap q) c) = f c
                                                  theorem LinearMap.submoduleComap_surjective_of_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₁) (q : Submodule R M₁) (hf : Function.Surjective f) :
                                                  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
                                                    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) :
                                                      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} :
                                                      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
                                                        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