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₂andM →ₗ[R] M₂for the type of semilinear (resp. linear) maps fromMtoM₂over the ring homomorphismσ(resp. over the ringR).
Tags #
linear algebra, vector space, module, range
def
LinearMap.range
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_5}
{M₂ : Type u_6}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_10}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
[RingHomSurjective τ₁₂]
(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_5}
{M₂ : Type u_6}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_10}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
[RingHomSurjective τ₁₂]
(f : F)
:
theorem
LinearMap.range_toAddSubmonoid
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_5}
{M₂ : Type u_6}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
[RingHomSurjective τ₁₂]
(f : M →ₛₗ[τ₁₂] M₂)
:
@[simp]
theorem
LinearMap.mem_range
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_5}
{M₂ : Type u_6}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_10}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
[RingHomSurjective τ₁₂]
{f : F}
{x : M₂}
:
theorem
LinearMap.range_eq_map
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_5}
{M₂ : Type u_6}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_10}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
[RingHomSurjective τ₁₂]
(f : F)
:
theorem
LinearMap.mem_range_self
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_5}
{M₂ : Type u_6}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_10}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
[RingHomSurjective τ₁₂]
(f : F)
(x : M)
:
theorem
LinearMap.range_comp
{R : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
{M : Type u_5}
{M₂ : Type u_6}
{M₃ : Type u_7}
[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₃)
:
theorem
LinearMap.range_comp_le_range
{R : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
{M : Type u_5}
{M₂ : Type u_6}
{M₃ : Type u_7}
[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 τ₁₃]
(f : M →ₛₗ[τ₁₂] M₂)
(g : M₂ →ₛₗ[τ₂₃] M₃)
:
theorem
LinearMap.range_eq_top
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_5}
{M₂ : Type u_6}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_10}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
[RingHomSurjective τ₁₂]
{f : F}
:
theorem
LinearMap.range_eq_top_of_surjective
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_5}
{M₂ : Type u_6}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_10}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
[RingHomSurjective τ₁₂]
(f : F)
(hf : Function.Surjective ⇑f)
:
theorem
LinearMap.range_le_iff_comap
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_5}
{M₂ : Type u_6}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_10}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
[RingHomSurjective τ₁₂]
{f : F}
{p : Submodule R₂ M₂}
:
theorem
LinearMap.map_le_range
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_5}
{M₂ : Type u_6}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_10}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
[RingHomSurjective τ₁₂]
{f : F}
{p : Submodule R M}
:
@[simp]
theorem
LinearMap.range_neg
{R : Type u_11}
{R₂ : Type u_12}
{M : Type u_13}
{M₂ : Type u_14}
[Semiring R]
[Ring R₂]
[AddCommMonoid M]
[AddCommGroup M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
[RingHomSurjective τ₁₂]
(f : M →ₛₗ[τ₁₂] M₂)
:
@[simp]
theorem
LinearMap.range_domRestrict
{R : Type u_1}
{M : Type u_5}
{M₂ : Type u_6}
[Semiring R]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R M₂]
(K : Submodule R M)
(f : M →ₗ[R] M₂)
:
theorem
LinearMap.range_domRestrict_le_range
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_5}
{M₂ : Type u_6}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
[RingHomSurjective τ₁₂]
(f : M →ₛₗ[τ₁₂] M₂)
(S : Submodule R M)
:
@[simp]
theorem
AddMonoidHom.coe_toIntLinearMap_range
{M : Type u_11}
{M₂ : Type u_12}
[AddCommGroup M]
[AddCommGroup M₂]
(f : M →+ M₂)
:
theorem
Submodule.map_comap_eq_of_le
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_5}
{M₂ : Type u_6}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_10}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
[RingHomSurjective τ₁₂]
{f : F}
{p : Submodule R₂ M₂}
(h : p ≤ LinearMap.range f)
:
theorem
LinearMap.range_restrictScalars
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_5}
{M₂ : Type u_6}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
[SMul R R₂]
[Module R₂ M]
[Module R M₂]
[CompatibleSMul M M₂ R R₂]
[IsScalarTower R R₂ M₂]
(f : M →ₗ[R₂] M₂)
:
@[simp]
theorem
LinearMap.iterateRange_coe
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(f : M →ₗ[R] M)
(n : ℕ)
:
@[reducible, inline]
abbrev
LinearMap.rangeRestrict
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_5}
{M₂ : Type u_6}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
[RingHomSurjective τ₁₂]
(f : M →ₛₗ[τ₁₂] M₂)
:
Restrict the codomain of a linear map f to f.range.
This is the bundled version of Set.rangeFactorization.
Equations
Instances For
instance
LinearMap.fintypeRange
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_5}
{M₂ : Type u_6}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
[Fintype M]
[DecidableEq M₂]
[RingHomSurjective τ₁₂]
(f : M →ₛₗ[τ₁₂] 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
theorem
LinearMap.range_codRestrict
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_5}
{M₂ : Type u_6}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₂₁ : R₂ →+* R}
[RingHomSurjective τ₂₁]
(p : Submodule R M)
(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_5}
{M₂ : Type u_6}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_10}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
[RingHomSurjective τ₁₂]
(f : F)
(q : Submodule R₂ M₂)
:
theorem
Submodule.map_comap_eq_self
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_5}
{M₂ : Type u_6}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_10}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
[RingHomSurjective τ₁₂]
{f : F}
{q : Submodule R₂ M₂}
(h : q ≤ LinearMap.range f)
:
@[simp]
theorem
LinearMap.range_zero
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_5}
{M₂ : Type u_6}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
[RingHomSurjective τ₁₂]
:
theorem
LinearMap.range_le_ker_iff
{R : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
{M : Type u_5}
{M₂ : Type u_6}
{M₃ : Type u_7}
[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 τ₁₂]
{f : M →ₛₗ[τ₁₂] M₂}
{g : M₂ →ₛₗ[τ₂₃] M₃}
:
theorem
LinearMap.comap_le_comap_iff
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_5}
{M₂ : Type u_6}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_10}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
[RingHomSurjective τ₁₂]
{f : F}
(hf : range f = ⊤)
{p p' : Submodule R₂ M₂}
:
theorem
LinearMap.comap_injective
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_5}
{M₂ : Type u_6}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_10}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
[RingHomSurjective τ₁₂]
{f : F}
(hf : range f = ⊤)
:
theorem
LinearMap.range_toAddSubgroup
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_5}
{M₂ : Type u_6}
[Ring R]
[Ring R₂]
[AddCommGroup M]
[AddCommGroup M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
[RingHomSurjective τ₁₂]
(f : M →ₛₗ[τ₁₂] M₂)
:
theorem
LinearMap.ker_le_iff
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_5}
{M₂ : Type u_6}
[Ring R]
[Ring R₂]
[AddCommGroup M]
[AddCommGroup M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_10}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
{f : F}
[RingHomSurjective τ₁₂]
{p : Submodule R M}
:
@[simp]
theorem
Submodule.map_top
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_5}
{M₂ : Type u_6}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_10}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
[RingHomSurjective τ₁₂]
(f : F)
:
@[simp]
theorem
Submodule.range_subtype
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p : Submodule R M)
:
theorem
Submodule.submoduleOf_self
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(N : Submodule R M)
:
theorem
Submodule.submoduleOf_sup_of_le
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{N₁ N₂ N : Submodule R M}
(h₁ : N₁ ≤ N)
(h₂ : N₂ ≤ N)
:
theorem
Submodule.range_inclusion
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p q : Submodule R M)
(h : p ≤ q)
:
@[simp]
theorem
Submodule.map_subtype_range_inclusion
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{p p' : Submodule R M}
(h : p ≤ p')
:
theorem
Submodule.restrictScalars_map
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_5}
{M₂ : Type u_6}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
[SMul R R₂]
[Module R₂ M]
[Module R M₂]
[IsScalarTower R R₂ M]
[IsScalarTower R R₂ M₂]
(f : M →ₗ[R₂] M₂)
(M' : Submodule R₂ M)
:
def
Submodule.MapSubtype.relIso
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p : Submodule R M)
:
If N ⊆ M then submodules of N are the same as submodules of M contained in N.
See also Submodule.mapIic.
Equations
Instances For
@[simp]
theorem
Submodule.map_subtype_embedding_eq
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p : Submodule R M)
(p' : Submodule R ↥p)
:
theorem
LinearMap.ker_eq_bot_of_cancel
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_5}
{M₂ : Type u_6}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{f : M →ₛₗ[τ₁₂] M₂}
(h : ∀ (u v : ↥(ker f) →ₗ[R] M), f ∘ₛₗ u = f ∘ₛₗ v → u = 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_5}
{M₂ : Type u_6}
{M₃ : Type u_7}
[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₃)
(hf : range f = ⊤)
:
def
LinearMap.submoduleImage
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{M' : Type u_10}
[AddCommMonoid M']
[Module R M']
{O : Submodule R M}
(ϕ : ↥O →ₗ[R] M')
(N : Submodule R M)
:
Submodule R M'
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_of_le
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{M' : Type u_10}
[AddCommMonoid M']
[Module R M']
{O : Submodule R M}
{ϕ : ↥O →ₗ[R] M'}
{N : Submodule R M}
(hNO : N ≤ O)
{x : M'}
:
theorem
LinearMap.submoduleImage_apply_of_le
{R : Type u_1}
{M : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{M' : Type u_10}
[AddCommMonoid M']
[Module R M']
{O : Submodule R M}
(ϕ : ↥O →ₗ[R] M')
(N : Submodule R M)
(hNO : N ≤ O)
:
@[simp]
theorem
LinearMap.range_rangeRestrict
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_5}
{M₂ : Type u_6}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
[RingHomSurjective τ₁₂]
(f : M →ₛₗ[τ₁₂] M₂)
:
theorem
LinearMap.surjective_rangeRestrict
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_5}
{M₂ : Type u_6}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
[RingHomSurjective τ₁₂]
(f : M →ₛₗ[τ₁₂] M₂)
:
@[simp]
theorem
LinearMap.ker_rangeRestrict
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_5}
{M₂ : Type u_6}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
[RingHomSurjective τ₁₂]
(f : M →ₛₗ[τ₁₂] M₂)
:
@[simp]
theorem
LinearMap.injective_rangeRestrict_iff
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_5}
{M₂ : Type u_6}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
[RingHomSurjective τ₁₂]
(f : M →ₛₗ[τ₁₂] M₂)
: