# map and comap for Submodules #

## Main declarations #

• Submodule.map: The pushforward of a submodule p ⊆ M by f : M → M₂
• Submodule.comap: The pullback of a submodule p ⊆ M₂ along f : M → M₂
• Submodule.giMapComap: map f and comap f form a GaloisInsertion when f is surjective.
• Submodule.gciMapComap: map f and comap f form a GaloisCoinsertion when f is injective.

## 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₂] [] [] [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 pushforward of a submodule p ⊆ M by f : M → M₂

Equations
• = { carrier := f '' p, add_mem' := , zero_mem' := , smul_mem' := }
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₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (p : ) :
(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₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] (f : M →ₛₗ[σ₁₂] M₂) (p : ) :
theorem Submodule.map_toAddSubmonoid' {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] (f : M →ₛₗ[σ₁₂] M₂) (p : ) :
@[simp]
theorem AddMonoidHom.coe_toIntLinearMap_map {A : Type u_10} {A₂ : Type u_11} [] [] (f : A →+ A₂) (s : ) :
@[simp]
theorem MonoidHom.coe_toAdditive_map {G : Type u_10} {G₂ : Type u_11} [] [Group G₂] (f : G →* G₂) (s : ) :
@[simp]
theorem AddMonoidHom.coe_toMultiplicative_map {G : Type u_10} {G₂ : Type u_11} [] [AddGroup G₂] (f : G →+ G₂) (s : ) :
@[simp]
theorem Submodule.mem_map {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {f : F} {p : } {x : M₂} :
x 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₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {f : F} {p : } {r : M} (h : r p) :
f r
theorem Submodule.apply_coe_mem_map {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) {p : } (r : { x : M // x p }) :
f r
@[simp]
theorem Submodule.map_id {R : Type u_1} {M : Type u_5} [] [] [Module R M] (p : ) :
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₃] [] [] [] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [] [] [] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (p : ) :
theorem Submodule.map_mono {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {f : F} {p : } {p' : } :
p p'
@[simp]
theorem Submodule.map_zero {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (p : ) [] :
theorem Submodule.map_add_le {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (p : ) [] (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₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) {p : } {q : } :
theorem Submodule.map_inf {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) {p : } {q : } (hf : ) :
theorem Submodule.range_map_nonempty {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] (N : ) :
(Set.range fun (ϕ : M →ₛₗ[σ₁₂] M₂) => ).Nonempty
noncomputable def Submodule.equivMapOfInjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [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 : ) (p : ) :
{ x : M // x p } ≃ₛₗ[σ₁₂] { x : M₂ // x }

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
• One or more equations did not get rendered due to their size.
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₂] [] [] [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 : ) (p : ) (x : { x : M // x 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₂] [] [] [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 : ) (p : ) (x : { x : M₂ // x }) :
f (.symm x) = x
def Submodule.comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [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
• = { carrier := f ⁻¹' p, add_mem' := , zero_mem' := , smul_mem' := }
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₂] [] [] [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} [] [] (f : A →+ A₂) (s : ) :
@[simp]
theorem Submodule.mem_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [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 f x p
@[simp]
theorem Submodule.comap_id {R : Type u_1} {M : Type u_5} [] [] [Module R M] (p : ) :
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₃] [] [] [] [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₃) :
Submodule.comap (g.comp f) p =
theorem Submodule.comap_mono {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [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₂} :
q q'
theorem Submodule.le_comap_pow_of_le_comap {R : Type u_1} {M : Type u_5} [] [] [Module R M] (p : ) {f : M →ₗ[R] M} (h : 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₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [] {f : F} {p : } {q : Submodule R₂ M₂} :
q p
theorem Submodule.gc_map_comap {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [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.map_bot {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [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.map_sup {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} (p : ) (p' : ) {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [] (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₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [] {ι : Sort u_10} (f : F) (p : ι) :
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₂] [] [] [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₂] [] [] [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₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [] {ι : 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₂] [] [] [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₂] [] [] [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₂) :
theorem Submodule.le_comap_map {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [] (f : F) (p : ) :
def Submodule.giMapComap {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [] {f : F} (hf : ) :

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

Equations
• = .toGaloisInsertion
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₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [] {f : F} (hf : ) (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₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [] {f : F} (hf : ) :
theorem Submodule.comap_injective_of_surjective {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [] {f : F} (hf : ) :
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₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [] {f : F} (hf : ) (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₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [] {f : F} (hf : ) {ι : 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₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [] {f : F} (hf : ) (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₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [] {f : F} (hf : ) {ι : 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₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [] {f : F} (hf : ) (p : Submodule R₂ M₂) (q : Submodule R₂ M₂) :
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₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [] {f : F} (hf : ) :
def Submodule.gciMapComap {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [] {f : F} (hf : ) :

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

Equations
• = .toGaloisCoinsertion
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₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [] {f : F} (hf : ) (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₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [] {f : F} (hf : ) :
theorem Submodule.map_injective_of_injective {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [] {f : F} (hf : ) :
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₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [] {f : F} (hf : ) (p : ) (q : ) :
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₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [] {f : F} (hf : ) {ι : Sort u_10} (S : ι) :
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₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [] {f : F} (hf : ) (p : ) (q : ) :
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₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [] {f : F} (hf : ) {ι : Sort u_10} (S : ι) :
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₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [] {f : F} (hf : ) (p : ) (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₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [] {f : F} (hf : ) :
@[simp]
theorem Submodule.orderIsoMapComapOfBijective_symm_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (hf : ) (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₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (hf : ) (p : ) :
=
def Submodule.orderIsoMapComapOfBijective {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (hf : ) :
≃o Submodule R₂ M₂

A linear isomorphism induces an order isomorphism of submodules.

Equations
• = { toFun := , invFun := , left_inv := , right_inv := , map_rel_iff' := }
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₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] {F : Type u_9} [EquivLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (p : ) :
=
@[simp]
theorem Submodule.orderIsoMapComap_symm_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] {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₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [] {F : Type u_9} [EquivLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) :
≃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₂] [] [] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {F : Type u_9} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [] {f : F} {p : } {p' : Submodule R₂ M₂} :
p' = Submodule.map f (p )
@[simp]
theorem Submodule.map_comap_subtype {R : Type u_1} {M : Type u_5} [] [] [Module R M] (p : ) (p' : ) :
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} [] [] [Module R M] (b : { x : M // x }) :
b = 0
theorem LinearMap.iInf_invariant {R : Type u_1} {M : Type u_5} [] [] [Module R M] {σ : R →+* R} {ι : Sort u_10} (f : M →ₛₗ[σ] M) {p : ι} (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} [] [] [Module R M] {p : } {q : } :
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] [] [Module R M] (p : ) [] [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] [] [Module R M] [] [Module R M₂] {f : M →ₗ[R] M₂} {p : Submodule R M₂} :
theorem Submodule.map_toAddSubgroup {R : Type u_1} {M : Type u_5} {M₂ : Type u_7} [Ring R] [] [Module R M] [] [Module R M₂] (f : M →ₗ[R] M₂) (p : ) :
theorem Submodule.comap_smul {K : Type u_9} {V : Type u_10} {V₂ : Type u_11} [] [] [Module K 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} [] [] [Module K V] [] [Module K V₂] (f : V →ₗ[K] V₂) (p : ) (a : K) (h : a 0) :
theorem Submodule.comap_smul' {K : Type u_9} {V : Type u_10} {V₂ : Type u_11} [] [] [Module K V] [] [Module K V₂] (f : V →ₗ[K] V₂) (p : Submodule K V₂) (a : K) :
Submodule.comap (a f) p = ⨅ (_ : a 0),
theorem Submodule.map_smul' {K : Type u_9} {V : Type u_10} {V₂ : Type u_11} [] [] [Module K V] [] [Module K V₂] (f : V →ₗ[K] V₂) (p : ) (a : K) :
Submodule.map (a f) p = ⨆ (_ : a 0),
@[simp]
theorem Submodule.comapSubtypeEquivOfLe_symm_apply {R : Type u_1} {M : Type u_5} [] [] [Module R M] {p : } {q : } (hpq : p q) (x : { x : M // x p }) :
.symm x = x, ,
def Submodule.comapSubtypeEquivOfLe {R : Type u_1} {M : Type u_5} [] [] [Module R M] {p : } {q : } (hpq : p q) :
{ x : { x : M // x q } // x Submodule.comap q.subtype p } ≃ₗ[R] { x : M // x 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} [] [] [Module R M] {p : } {q : } (hpq : p q) (x : { x : { x : M // x q } // x Submodule.comap q.subtype p }) :
( 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₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] (p : ) {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₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] (e : M ≃ₛₗ[τ₁₂] M₂) (K : ) :
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₂] [] [] [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₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] {p : } (e : M ≃ₛₗ[τ₁₂] M₂) {K : Submodule R₂ M₂} :
Submodule.map e.symm K = p = K
theorem Submodule.orderIsoMapComap_apply' {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] (e : M ≃ₛₗ[τ₁₂] M₂) (p : ) :
= Submodule.comap e.symm p
theorem Submodule.orderIsoMapComap_symm_apply' {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] (e : M ≃ₛₗ[τ₁₂] M₂) (p : Submodule R₂ M₂) :
.symm p = Submodule.map e.symm p
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₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} (q : Submodule R₂ M₂) (f₁ : M →ₛₗ[τ₁₂] M₂) (f₂ : M →ₛₗ[τ₁₂] M₂) :
Submodule.comap (f₁ + f₂) q
theorem Submodule.comap_le_comap_smul {R : Type u_1} {N : Type u_9} {N₂ : Type u_10} [] [] [] [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} [] [] [] [Module R N] [Module R N₂] (pₗ : ) (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} [] [] [] [Module R M] [Module R M₁] (f : M →ₗ[R] M₁) (p : ) :
{ x : M // x p } →ₗ[R] { x : M₁ // x }

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} [] [] [] [Module R M] [Module R M₁] (f : M →ₗ[R] M₁) {p : } (x : { x : 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} [] [] [] [Module R M] [Module R M₁] (f : M →ₗ[R] M₁) (p : ) :
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} [] [] [Module R M] [Semiring R₂] [] [Module R₂ M₂] {σ₂₁ : R₂ →+* R} [] (p : ) (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} [] [] [Module R M] [Semiring R₂] [] [Module R₂ M₂] {σ₂₁ : R₂ →+* R} (p : ) (f : M₂ →ₛₗ[σ₂₁] M) (hf : ∀ (c : M₂), f c p) (p' : Submodule R { x : M // x 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₂] [] [] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) {p : } :
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₂] [] [] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) (p : ) :
{ x : M // x p } ≃ₛₗ[σ₁₂] { x : M₂ // x 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₂] [] [] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) (p : ) (x : { x : 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₂] [] [] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂) (p : ) (x : { x : M₂ // x Submodule.map (↑e) p }) :
((e.submoduleMap p).symm x) = e.symm x