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_6}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_11}
[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
- LinearMap.range f = Submodule.copy (Submodule.map f ⊤) (Set.range ⇑f) ⋯
Instances For
theorem
LinearMap.range_coe
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_6}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_11}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
[RingHomSurjective τ₁₂]
(f : F)
:
↑(LinearMap.range f) = Set.range ⇑f
theorem
LinearMap.range_toAddSubmonoid
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_6}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
[RingHomSurjective τ₁₂]
(f : M →ₛₗ[τ₁₂] M₂)
:
(LinearMap.range f).toAddSubmonoid = AddMonoidHom.mrange f
@[simp]
theorem
LinearMap.mem_range
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_6}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_11}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
[RingHomSurjective τ₁₂]
{f : F}
{x : M₂}
:
x ∈ LinearMap.range f ↔ ∃ (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]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_11}
[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_6}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_11}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
[RingHomSurjective τ₁₂]
(f : F)
(x : M)
:
f x ∈ LinearMap.range f
@[simp]
theorem
LinearMap.range_id
{R : Type u_1}
{M : Type u_6}
[Semiring R]
[AddCommMonoid M]
[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₂]
[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₃)
:
LinearMap.range (LinearMap.comp g f) = Submodule.map g (LinearMap.range 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₂]
[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_6}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_11}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
[RingHomSurjective τ₁₂]
{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]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_11}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
[RingHomSurjective τ₁₂]
{f : F}
{p : Submodule R₂ M₂}
:
LinearMap.range f ≤ p ↔ Submodule.comap f p = ⊤
theorem
LinearMap.map_le_range
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_6}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_11}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
[RingHomSurjective τ₁₂]
{f : F}
{p : Submodule R M}
:
Submodule.map f p ≤ LinearMap.range f
@[simp]
theorem
LinearMap.range_neg
{R : Type u_12}
{R₂ : Type u_13}
{M : Type u_14}
{M₂ : Type u_15}
[Semiring R]
[Ring R₂]
[AddCommMonoid M]
[AddCommGroup M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
[RingHomSurjective τ₁₂]
(f : M →ₛₗ[τ₁₂] M₂)
:
LinearMap.range (-f) = LinearMap.range f
theorem
LinearMap.range_domRestrict_le_range
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_6}
{M₂ : Type u_7}
[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_12}
{M₂ : Type u_13}
[AddCommGroup M]
[AddCommGroup M₂]
(f : M →+ M₂)
:
LinearMap.range (AddMonoidHom.toIntLinearMap f) = AddSubgroup.toIntSubmodule (AddMonoidHom.range f)
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]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_11}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
[RingHomSurjective τ₁₂]
{f : F}
{p : Submodule R₂ M₂}
(h : p ≤ LinearMap.range f)
:
Submodule.map f (Submodule.comap f p) = p
@[simp]
theorem
LinearMap.iterateRange_coe
{R : Type u_1}
{M : Type u_6}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(f : M →ₗ[R] M)
(n : ℕ)
:
(LinearMap.iterateRange f) n = LinearMap.range (f ^ n)
def
LinearMap.iterateRange
{R : Type u_1}
{M : Type u_6}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(f : M →ₗ[R] M)
:
The decreasing sequence of submodules consisting of the ranges of the iterates of a linear map.
Equations
- LinearMap.iterateRange f = { toFun := fun (n : ℕ) => LinearMap.range (f ^ n), monotone' := ⋯ }
Instances For
@[reducible]
def
LinearMap.rangeRestrict
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_6}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
[RingHomSurjective τ₁₂]
(f : M →ₛₗ[τ₁₂] M₂)
:
M →ₛₗ[τ₁₂] ↥(LinearMap.range f)
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_6}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
[Fintype M]
[DecidableEq M₂]
[RingHomSurjective τ₁₂]
(f : M →ₛₗ[τ₁₂] M₂)
:
Fintype ↥(LinearMap.range f)
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_6}
{M₂ : Type u_7}
[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)
:
LinearMap.range (LinearMap.codRestrict p f hf) = Submodule.comap (Submodule.subtype p) (LinearMap.range f)
theorem
Submodule.map_comap_eq
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_6}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_11}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
[RingHomSurjective τ₁₂]
(f : F)
(q : Submodule R₂ M₂)
:
Submodule.map f (Submodule.comap f q) = LinearMap.range f ⊓ q
theorem
Submodule.map_comap_eq_self
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_6}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_11}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
[RingHomSurjective τ₁₂]
{f : F}
{q : Submodule R₂ M₂}
(h : q ≤ LinearMap.range f)
:
Submodule.map f (Submodule.comap f q) = q
@[simp]
theorem
LinearMap.range_zero
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_6}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
[RingHomSurjective τ₁₂]
:
theorem
LinearMap.range_le_bot_iff
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_6}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
[RingHomSurjective τ₁₂]
(f : M →ₛₗ[τ₁₂] M₂)
:
LinearMap.range f ≤ ⊥ ↔ 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]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
[RingHomSurjective τ₁₂]
{f : M →ₛₗ[τ₁₂] M₂}
:
LinearMap.range f = ⊥ ↔ 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₂]
[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₃}
:
LinearMap.range f ≤ LinearMap.ker g ↔ LinearMap.comp g 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]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_11}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
[RingHomSurjective τ₁₂]
{f : F}
(hf : LinearMap.range f = ⊤)
{p : Submodule R₂ M₂}
{p' : Submodule R₂ M₂}
:
Submodule.comap f p ≤ Submodule.comap f p' ↔ p ≤ p'
theorem
LinearMap.comap_injective
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_6}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_11}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
[RingHomSurjective τ₁₂]
{f : F}
(hf : LinearMap.range f = ⊤)
:
theorem
LinearMap.range_toAddSubgroup
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_6}
{M₂ : Type u_7}
[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_6}
{M₂ : Type u_7}
[Ring R]
[Ring R₂]
[AddCommGroup M]
[AddCommGroup M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_11}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
{f : F}
[RingHomSurjective τ₁₂]
{p : Submodule R M}
:
LinearMap.ker f ≤ p ↔ ∃ y ∈ LinearMap.range f, ⇑f ⁻¹' {y} ⊆ ↑p
theorem
LinearMap.range_smul
{K : Type u_4}
{V : Type u_9}
{V₂ : Type u_10}
[Semifield K]
[AddCommMonoid V]
[Module K V]
[AddCommMonoid V₂]
[Module K V₂]
(f : V →ₗ[K] V₂)
(a : K)
(h : a ≠ 0)
:
LinearMap.range (a • f) = LinearMap.range f
theorem
LinearMap.range_smul'
{K : Type u_4}
{V : Type u_9}
{V₂ : Type u_10}
[Semifield K]
[AddCommMonoid V]
[Module K V]
[AddCommMonoid V₂]
[Module K V₂]
(f : V →ₗ[K] V₂)
(a : K)
:
LinearMap.range (a • f) = ⨆ (_ : a ≠ 0), LinearMap.range f
@[simp]
theorem
Submodule.map_top
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_6}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{F : Type u_11}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
[RingHomSurjective τ₁₂]
(f : F)
:
@[simp]
theorem
Submodule.range_subtype
{R : Type u_1}
{M : Type u_6}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p : Submodule R M)
:
theorem
Submodule.map_subtype_le
{R : Type u_1}
{M : Type u_6}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p : Submodule R M)
(p' : Submodule R ↥p)
:
Submodule.map (Submodule.subtype p) p' ≤ p
theorem
Submodule.map_subtype_top
{R : Type u_1}
{M : Type u_6}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p : Submodule R M)
:
Submodule.map (Submodule.subtype p) ⊤ = 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}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{p : Submodule R M}
{p' : Submodule R M}
:
Submodule.comap (Submodule.subtype p) p' = ⊤ ↔ p ≤ p'
@[simp]
theorem
Submodule.comap_subtype_self
{R : Type u_1}
{M : Type u_6}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p : Submodule R M)
:
Submodule.comap (Submodule.subtype p) p = ⊤
theorem
Submodule.range_inclusion
{R : Type u_1}
{M : Type u_6}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p : Submodule R M)
(q : Submodule R M)
(h : p ≤ q)
:
@[simp]
theorem
Submodule.map_subtype_range_inclusion
{R : Type u_1}
{M : Type u_6}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{p : Submodule R M}
{p' : Submodule R M}
(h : p ≤ p')
:
Submodule.map (Submodule.subtype p') (LinearMap.range (Submodule.inclusion h)) = p
def
Submodule.MapSubtype.relIso
{R : Type u_1}
{M : Type u_6}
[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
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}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p : Submodule R M)
:
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}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p : Submodule R M)
(p' : Submodule R ↥p)
:
(Submodule.MapSubtype.orderEmbedding p) p' = Submodule.map (Submodule.subtype p) p'
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]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
{f : M →ₛₗ[τ₁₂] M₂}
(h : ∀ (u v : ↥(LinearMap.ker f) →ₗ[R] M), LinearMap.comp f u = LinearMap.comp f v → u = v)
:
LinearMap.ker f = ⊥
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₂]
[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 : LinearMap.range f = ⊤)
:
def
LinearMap.submoduleImage
{R : Type u_1}
{M : Type u_6}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{M' : Type u_11}
[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
- LinearMap.submoduleImage ϕ N = Submodule.map ϕ (Submodule.comap (Submodule.subtype O) N)
Instances For
@[simp]
theorem
LinearMap.mem_submoduleImage
{R : Type u_1}
{M : Type u_6}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{M' : Type u_11}
[AddCommMonoid M']
[Module R M']
{O : Submodule R M}
{ϕ : ↥O →ₗ[R] M'}
{N : Submodule R M}
{x : M'}
:
theorem
LinearMap.mem_submoduleImage_of_le
{R : Type u_1}
{M : Type u_6}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{M' : Type u_11}
[AddCommMonoid M']
[Module R M']
{O : Submodule R M}
{ϕ : ↥O →ₗ[R] M'}
{N : Submodule R M}
(hNO : N ≤ O)
{x : M'}
:
x ∈ LinearMap.submoduleImage ϕ N ↔ ∃ (y : M) (yN : y ∈ N), ϕ { val := y, property := ⋯ } = x
theorem
LinearMap.submoduleImage_apply_of_le
{R : Type u_1}
{M : Type u_6}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{M' : Type u_11}
[AddCommGroup M']
[Module R M']
{O : Submodule R M}
(ϕ : ↥O →ₗ[R] M')
(N : Submodule R M)
(hNO : N ≤ O)
:
LinearMap.submoduleImage ϕ N = LinearMap.range (ϕ ∘ₗ Submodule.inclusion hNO)
@[simp]
theorem
LinearMap.range_rangeRestrict
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_6}
{M₂ : Type u_7}
[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_6}
{M₂ : Type u_7}
[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_6}
{M₂ : Type u_7}
[Semiring R]
[Semiring R₂]
[AddCommMonoid M]
[AddCommMonoid M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
[RingHomSurjective τ₁₂]
(f : M →ₛₗ[τ₁₂] M₂)
: