# Range of linear maps #

The range LinearMap.range of a (semi)linear map f : M → M₂ is a submodule of M₂.

More specifically, LinearMap.range applies to any SemilinearMapClass over a RingHomSurjective ring homomorphism.

Note that this also means that dot notation (i.e. f.range for a linear map f) does not work.

## Notations #

• We continue to use the notations M →ₛₗ[σ] M₂ and M →ₗ[R] M₂ for the type of semilinear (resp. linear) maps from M to M₂ over the ring homomorphism σ (resp. over the ring R).

## Tags #

linear algebra, vector space, module, range

def LinearMap.range {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [] (f : F) :
Submodule R₂ M₂

The range of a linear map f : M → M₂ is a submodule of M₂. See Note [range copy pattern].

Equations
Instances For
theorem LinearMap.range_coe {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [] (f : F) :
=
theorem LinearMap.range_toAddSubmonoid {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [] (f : M →ₛₗ[τ₁₂] M₂) :
@[simp]
theorem LinearMap.mem_range {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [] {f : F} {x : M₂} :
∃ (y : M), f y = x
theorem LinearMap.range_eq_map {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [] (f : F) :
theorem LinearMap.mem_range_self {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [] (f : F) (x : M) :
f x
@[simp]
theorem LinearMap.range_id {R : Type u_1} {M : Type u_6} [] [] [Module R M] :
LinearMap.range LinearMap.id =
theorem LinearMap.range_comp {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {M : Type u_6} {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₃) :
LinearMap.range (g.comp f) =
theorem LinearMap.range_comp_le_range {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {M : Type u_6} {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₃) :
LinearMap.range (g.comp f)
theorem LinearMap.range_eq_top {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [] {f : F} :
theorem LinearMap.range_le_iff_comap {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [] {f : F} {p : Submodule R₂ M₂} :
theorem LinearMap.map_le_range {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [] {f : F} {p : } :
@[simp]
theorem LinearMap.range_neg {R : Type u_12} {R₂ : Type u_13} {M : Type u_14} {M₂ : Type u_15} [] [Ring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [] (f : M →ₛₗ[τ₁₂] M₂) :
theorem LinearMap.range_domRestrict_le_range {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [] (f : M →ₛₗ[τ₁₂] M₂) (S : ) :
LinearMap.range (f.domRestrict S)
@[simp]
theorem AddMonoidHom.coe_toIntLinearMap_range {M : Type u_12} {M₂ : Type u_13} [] [] (f : M →+ M₂) :
theorem Submodule.map_comap_eq_of_le {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [] {f : F} {p : Submodule R₂ M₂} (h : ) :
@[simp]
theorem LinearMap.iterateRange_coe {R : Type u_1} {M : Type u_6} [] [] [Module R M] (f : M →ₗ[R] M) (n : ) :
f.iterateRange n = LinearMap.range (f ^ n)
def LinearMap.iterateRange {R : Type u_1} {M : Type u_6} [] [] [Module R M] (f : M →ₗ[R] M) :

The decreasing sequence of submodules consisting of the ranges of the iterates of a linear map.

Equations
Instances For
@[reducible, inline]
abbrev LinearMap.rangeRestrict {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [] (f : M →ₛₗ[τ₁₂] M₂) :
M →ₛₗ[τ₁₂] { x : M₂ // }

Restrict the codomain of a linear map f to f.range.

This is the bundled version of Set.rangeFactorization.

Equations
• f.rangeRestrict =
Instances For
instance LinearMap.fintypeRange {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [] [] [] (f : M →ₛₗ[τ₁₂] M₂) :
Fintype { x : M₂ // }

The range of a linear map is finite if the domain is finite. Note: this instance can form a diamond with Subtype.fintype in the presence of Fintype M₂.

Equations
• f.fintypeRange =
theorem LinearMap.range_codRestrict {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₂₁ : R₂ →+* R} [] (p : ) (f : M₂ →ₛₗ[τ₂₁] M) (hf : ∀ (c : M₂), f c p) :
theorem Submodule.map_comap_eq {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [] (f : F) (q : Submodule R₂ M₂) :
theorem Submodule.map_comap_eq_self {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [] {f : F} {q : Submodule R₂ M₂} (h : ) :
@[simp]
theorem LinearMap.range_zero {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [] :
theorem LinearMap.range_le_bot_iff {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [] (f : M →ₛₗ[τ₁₂] M₂) :
f = 0
theorem LinearMap.range_eq_bot {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [] {f : M →ₛₗ[τ₁₂] M₂} :
f = 0
theorem LinearMap.range_le_ker_iff {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {M : Type u_6} {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₃} :
g.comp f = 0
theorem LinearMap.comap_le_comap_iff {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [] {f : F} (hf : ) {p : Submodule R₂ M₂} {p' : Submodule R₂ M₂} :
p p'
theorem LinearMap.comap_injective {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [] {f : F} (hf : ) :
theorem LinearMap.range_toAddSubgroup {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [Ring R] [Ring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [] (f : M →ₛₗ[τ₁₂] M₂) :
theorem LinearMap.ker_le_iff {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [Ring R] [Ring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} [] {p : } :
y, f ⁻¹' {y} p
theorem LinearMap.range_smul {K : Type u_4} {V : Type u_9} {V₂ : Type u_10} [] [] [Module K V] [] [Module K V₂] (f : V →ₗ[K] V₂) (a : K) (h : a 0) :
theorem LinearMap.range_smul' {K : Type u_4} {V : Type u_9} {V₂ : Type u_10} [] [] [Module K V] [] [Module K V₂] (f : V →ₗ[K] V₂) (a : K) :
LinearMap.range (a f) = ⨆ (_ : a 0),
@[simp]
theorem Submodule.map_top {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [] (f : F) :
@[simp]
theorem Submodule.range_subtype {R : Type u_1} {M : Type u_6} [] [] [Module R M] (p : ) :
LinearMap.range p.subtype = p
theorem Submodule.map_subtype_le {R : Type u_1} {M : Type u_6} [] [] [Module R M] (p : ) (p' : Submodule R { x : M // x p }) :
Submodule.map p.subtype p' p
theorem Submodule.map_subtype_top {R : Type u_1} {M : Type u_6} [] [] [Module R M] (p : ) :
Submodule.map p.subtype = p

Under the canonical linear map from a submodule p to the ambient space M, the image of the maximal submodule of p is just p.

@[simp]
theorem Submodule.comap_subtype_eq_top {R : Type u_1} {M : Type u_6} [] [] [Module R M] {p : } {p' : } :
Submodule.comap p.subtype p' = p p'
@[simp]
theorem Submodule.comap_subtype_self {R : Type u_1} {M : Type u_6} [] [] [Module R M] (p : ) :
Submodule.comap p.subtype p =
theorem Submodule.range_inclusion {R : Type u_1} {M : Type u_6} [] [] [Module R M] (p : ) (q : ) (h : p q) :
= Submodule.comap q.subtype p
@[simp]
theorem Submodule.map_subtype_range_inclusion {R : Type u_1} {M : Type u_6} [] [] [Module R M] {p : } {p' : } (h : p p') :
Submodule.map p'.subtype = p
def Submodule.MapSubtype.relIso {R : Type u_1} {M : Type u_6} [] [] [Module R M] (p : ) :
Submodule R { x : M // x p } ≃o { p' : // p' p }

If N ⊆ M then submodules of N are the same as submodules of M contained in N.

See also Submodule.mapIic.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Submodule.MapSubtype.orderEmbedding {R : Type u_1} {M : Type u_6} [] [] [Module R M] (p : ) :
Submodule R { x : M // x p } ↪o

If p ⊆ M is a submodule, the ordering of submodules of p is embedded in the ordering of submodules of M.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Submodule.map_subtype_embedding_eq {R : Type u_1} {M : Type u_6} [] [] [Module R M] (p : ) (p' : Submodule R { x : M // x p }) :
= Submodule.map p.subtype p'
def Submodule.mapIic {R : Type u_1} {M : Type u_6} [] [] [Module R M] (p : ) :
Submodule R { x : M // x p } ≃o (Set.Iic p)

If N ⊆ M then submodules of N are the same as submodules of M contained in N.

Equations
• p.mapIic =
Instances For
@[simp]
theorem Submodule.coe_mapIic_apply {R : Type u_1} {M : Type u_6} [] [] [Module R M] (p : ) (q : Submodule R { x : M // x p }) :
(p.mapIic q) = Submodule.map p.subtype q
theorem LinearMap.ker_eq_bot_of_cancel {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} (h : ∀ (u v : { x : M // } →ₗ[R] M), f.comp u = f.comp vu = v) :

A monomorphism is injective.

theorem LinearMap.range_comp_of_range_eq_top {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {M : Type u_6} {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₃) (hf : ) :
LinearMap.range (g.comp f) =
def LinearMap.submoduleImage {R : Type u_1} {M : Type u_6} [] [] [Module R M] {M' : Type u_11} [] [Module R M'] {O : } (ϕ : { x : M // x O } →ₗ[R] M') (N : ) :

If O is a submodule of M, and Φ : O →ₗ M' is a linear map, then (ϕ : O →ₗ M').submoduleImage N is ϕ(N) as a submodule of M'

Equations
Instances For
@[simp]
theorem LinearMap.mem_submoduleImage {R : Type u_1} {M : Type u_6} [] [] [Module R M] {M' : Type u_11} [] [Module R M'] {O : } {ϕ : { x : M // x O } →ₗ[R] M'} {N : } {x : M'} :
x ϕ.submoduleImage N ∃ (y : M) (yO : y O), y N ϕ y, yO = x
theorem LinearMap.mem_submoduleImage_of_le {R : Type u_1} {M : Type u_6} [] [] [Module R M] {M' : Type u_11} [] [Module R M'] {O : } {ϕ : { x : M // x O } →ₗ[R] M'} {N : } (hNO : N O) {x : M'} :
x ϕ.submoduleImage N ∃ (y : M) (yN : y N), ϕ y, = x
theorem LinearMap.submoduleImage_apply_of_le {R : Type u_1} {M : Type u_6} [] [] [Module R M] {M' : Type u_11} [] [Module R M'] {O : } (ϕ : { x : M // x O } →ₗ[R] M') (N : ) (hNO : N O) :
ϕ.submoduleImage N = LinearMap.range (ϕ ∘ₗ )
@[simp]
theorem LinearMap.range_rangeRestrict {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [] (f : M →ₛₗ[τ₁₂] M₂) :
LinearMap.range f.rangeRestrict =
theorem LinearMap.surjective_rangeRestrict {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [] (f : M →ₛₗ[τ₁₂] M₂) :
Function.Surjective f.rangeRestrict
@[simp]
theorem LinearMap.ker_rangeRestrict {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [] [Semiring R₂] [] [] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [] (f : M →ₛₗ[τ₁₂] M₂) :
LinearMap.ker f.rangeRestrict =