The span of a set of vectors, as a submodule #
Submodule.span sis defined to be the smallest submodule containing the sets.
Notations #
- We introduce the notation
R ∙ vfor the span of a singleton,Submodule.span R {v}. This is\span, not the same as the scalar multiplication•/\bub.
@[simp]
theorem
Submodule.span_coe_eq_restrictScalars
{R : Type u_1}
{M : Type u_4}
{S : Type u_7}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p : Submodule R M)
[Semiring S]
[SMul S R]
[Module S M]
[IsScalarTower S R M]
:
Submodule.span S ↑p = Submodule.restrictScalars S p
A version of Submodule.span_eq for when the span is by a smaller ring.
theorem
Submodule.image_span_subset
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[AddCommMonoid M₂]
[Module R₂ M₂]
{F : Type u_8}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
(f : F)
(s : Set M)
(N : Submodule R₂ M₂)
:
⇑f '' ↑(Submodule.span R s) ⊆ ↑N ↔ ∀ m ∈ s, f m ∈ N
A version of Submodule.map_span_le that does not require the RingHomSurjective
assumption.
theorem
Submodule.image_span_subset_span
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[AddCommMonoid M₂]
[Module R₂ M₂]
{F : Type u_8}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
(f : F)
(s : Set M)
:
⇑f '' ↑(Submodule.span R s) ⊆ ↑(Submodule.span R₂ (⇑f '' s))
theorem
Submodule.map_span
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[AddCommMonoid M₂]
[Module R₂ M₂]
{F : Type u_8}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
[RingHomSurjective σ₁₂]
(f : F)
(s : Set M)
:
Submodule.map f (Submodule.span R s) = Submodule.span R₂ (⇑f '' s)
theorem
LinearMap.map_span
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[AddCommMonoid M₂]
[Module R₂ M₂]
{F : Type u_8}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
[RingHomSurjective σ₁₂]
(f : F)
(s : Set M)
:
Submodule.map f (Submodule.span R s) = Submodule.span R₂ (⇑f '' s)
Alias of Submodule.map_span.
theorem
Submodule.map_span_le
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[AddCommMonoid M₂]
[Module R₂ M₂]
{F : Type u_8}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
[RingHomSurjective σ₁₂]
(f : F)
(s : Set M)
(N : Submodule R₂ M₂)
:
Submodule.map f (Submodule.span R s) ≤ N ↔ ∀ m ∈ s, f m ∈ N
theorem
LinearMap.map_span_le
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[AddCommMonoid M₂]
[Module R₂ M₂]
{F : Type u_8}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
[RingHomSurjective σ₁₂]
(f : F)
(s : Set M)
(N : Submodule R₂ M₂)
:
Submodule.map f (Submodule.span R s) ≤ N ↔ ∀ m ∈ s, f m ∈ N
Alias of Submodule.map_span_le.
theorem
Submodule.span_preimage_le
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[AddCommMonoid M₂]
[Module R₂ M₂]
{F : Type u_8}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
(f : F)
(s : Set M₂)
:
Submodule.span R (⇑f ⁻¹' s) ≤ Submodule.comap f (Submodule.span R₂ s)
theorem
LinearMap.span_preimage_le
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[AddCommMonoid M₂]
[Module R₂ M₂]
{F : Type u_8}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
(f : F)
(s : Set M₂)
:
Submodule.span R (⇑f ⁻¹' s) ≤ Submodule.comap f (Submodule.span R₂ s)
Alias of Submodule.span_preimage_le.
theorem
Submodule.linearMap_eq_iff_of_eq_span
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{N : Type u_9}
[AddCommMonoid N]
[Module R N]
{V : Submodule R M}
(f g : ↥V →ₗ[R] N)
{S : Set M}
(hV : V = Submodule.span R S)
:
theorem
Submodule.linearMap_eq_iff_of_span_eq_top
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{N : Type u_9}
[AddCommMonoid N]
[Module R N]
(f g : M →ₗ[R] N)
{S : Set M}
(hM : Submodule.span R S = ⊤)
:
theorem
Submodule.linearMap_eq_zero_iff_of_span_eq_top
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{N : Type u_9}
[AddCommMonoid N]
[Module R N]
(f : M →ₗ[R] N)
{S : Set M}
(hM : Submodule.span R S = ⊤)
:
theorem
Submodule.linearMap_eq_zero_iff_of_eq_span
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{N : Type u_9}
[AddCommMonoid N]
[Module R N]
{V : Submodule R M}
(f : ↥V →ₗ[R] N)
{S : Set M}
(hV : V = Submodule.span R S)
:
theorem
Submodule.span_smul_eq_of_isUnit
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(s : Set M)
(r : R)
(hr : IsUnit r)
:
Submodule.span R (r • s) = Submodule.span R s
See Submodule.span_smul_eq (in RingTheory.Ideal.Operations) for
span R (r • s) = r • span R s that holds for arbitrary r in a CommSemiring.
theorem
Submodule.coe_scott_continuous
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
OmegaCompletePartialOrder.ωScottContinuous SetLike.coe
We can regard coe_iSup_of_chain as the statement that (↑) : (Submodule R M) → Set M is
Scott continuous for the ω-complete partial order induced by the complete lattice structures.
theorem
Submodule.disjoint_span_singleton
{K : Type u_9}
{E : Type u_10}
[DivisionRing K]
[AddCommGroup E]
[Module K E]
{s : Submodule K E}
{x : E}
:
Disjoint s (Submodule.span K {x}) ↔ x ∈ s → x = 0
theorem
Submodule.disjoint_span_singleton'
{K : Type u_9}
{E : Type u_10}
[DivisionRing K]
[AddCommGroup E]
[Module K E]
{p : Submodule K E}
{x : E}
(x0 : x ≠ 0)
:
Disjoint p (Submodule.span K {x}) ↔ x ∉ p
theorem
Submodule.span_le_restrictScalars
(R : Type u_1)
{M : Type u_4}
(S : Type u_7)
[Semiring R]
[AddCommMonoid M]
[Module R M]
(s : Set M)
[Semiring S]
[SMul R S]
[Module S M]
[IsScalarTower R S M]
:
Submodule.span R s ≤ Submodule.restrictScalars R (Submodule.span S s)
If R is "smaller" ring than S then the span by R is smaller than the span by S.
@[simp]
theorem
Submodule.span_subset_span
(R : Type u_1)
{M : Type u_4}
(S : Type u_7)
[Semiring R]
[AddCommMonoid M]
[Module R M]
(s : Set M)
[Semiring S]
[SMul R S]
[Module S M]
[IsScalarTower R S M]
:
↑(Submodule.span R s) ⊆ ↑(Submodule.span S s)
A version of Submodule.span_le_restrictScalars with coercions.
theorem
Submodule.span_span_of_tower
(R : Type u_1)
{M : Type u_4}
(S : Type u_7)
[Semiring R]
[AddCommMonoid M]
[Module R M]
(s : Set M)
[Semiring S]
[SMul R S]
[Module S M]
[IsScalarTower R S M]
:
Submodule.span S ↑(Submodule.span R s) = Submodule.span S s
Taking the span by a large ring of the span by the small ring is the same as taking the span by just the large ring.
theorem
Submodule.span_singleton_eq_span_singleton
{R : Type u_9}
{M : Type u_10}
[Ring R]
[AddCommGroup M]
[Module R M]
[NoZeroSMulDivisors R M]
{x y : M}
:
Submodule.span R {x} = Submodule.span R {y} ↔ ∃ (z : Rˣ), z • x = y
theorem
Submodule.span_image
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[AddCommMonoid M₂]
[Module R₂ M₂]
{F : Type u_8}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
{s : Set M}
[RingHomSurjective σ₁₂]
(f : F)
:
Submodule.span R₂ (⇑f '' s) = Submodule.map f (Submodule.span R s)
@[simp]
theorem
Submodule.span_image'
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[AddCommMonoid M₂]
[Module R₂ M₂]
{s : Set M}
[RingHomSurjective σ₁₂]
(f : M →ₛₗ[σ₁₂] M₂)
:
Submodule.span R₂ (⇑f '' s) = Submodule.map f (Submodule.span R s)
theorem
Submodule.apply_mem_span_image_of_mem_span
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[AddCommMonoid M₂]
[Module R₂ M₂]
{F : Type u_8}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
[RingHomSurjective σ₁₂]
(f : F)
{x : M}
{s : Set M}
(h : x ∈ Submodule.span R s)
:
f x ∈ Submodule.span R₂ (⇑f '' s)
theorem
Submodule.apply_mem_span_image_iff_mem_span
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[AddCommMonoid M₂]
[Module R₂ M₂]
{F : Type u_8}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
[RingHomSurjective σ₁₂]
{f : F}
{x : M}
{s : Set M}
(hf : Function.Injective ⇑f)
:
f x ∈ Submodule.span R₂ (⇑f '' s) ↔ x ∈ Submodule.span R s
@[simp]
theorem
Submodule.map_subtype_span_singleton
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{p : Submodule R M}
(x : ↥p)
:
Submodule.map p.subtype (Submodule.span R {x}) = Submodule.span R {↑x}
theorem
Submodule.not_mem_span_of_apply_not_mem_span_image
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[AddCommMonoid M₂]
[Module R₂ M₂]
{F : Type u_8}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
[RingHomSurjective σ₁₂]
(f : F)
{x : M}
{s : Set M}
(h : f x ∉ Submodule.span R₂ (⇑f '' s))
:
x ∉ Submodule.span R s
f is an explicit argument so we can apply this theorem and obtain h as a new goal.
theorem
Submodule.iSup_toAddSubmonoid
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{ι : Sort u_9}
(p : ι → Submodule R M)
:
(⨆ (i : ι), p i).toAddSubmonoid = ⨆ (i : ι), (p i).toAddSubmonoid
theorem
Submodule.iSup_induction
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{ι : Sort u_9}
(p : ι → Submodule R M)
{C : M → Prop}
{x : M}
(hx : x ∈ ⨆ (i : ι), p i)
(hp : ∀ (i : ι), ∀ x ∈ p i, C x)
(h0 : C 0)
(hadd : ∀ (x y : M), C x → C y → C (x + y))
:
C x
An induction principle for elements of ⨆ i, p i.
If C holds for 0 and all elements of p i for all i, and is preserved under addition,
then it holds for all elements of the supremum of p.
theorem
Submodule.iSup_induction'
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{ι : Sort u_9}
(p : ι → Submodule R M)
{C : (x : M) → x ∈ ⨆ (i : ι), p i → Prop}
(mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), C x ⋯)
(zero : C 0 ⋯)
(add : ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), p i) (hy : y ∈ ⨆ (i : ι), p i), C x hx → C y hy → C (x + y) ⋯)
{x : M}
(hx : x ∈ ⨆ (i : ι), p i)
:
C x hx
A dependent version of submodule.iSup_induction.
theorem
Submodule.singleton_span_isCompactElement
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(x : M)
:
theorem
Submodule.finset_span_isCompactElement
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(S : Finset M)
:
The span of a finite subset is compact in the lattice of submodules.
theorem
Submodule.finite_span_isCompactElement
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(S : Set M)
(h : S.Finite)
:
The span of a finite subset is compact in the lattice of submodules.
instance
Submodule.instIsCompactlyGenerated
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
def
Submodule.prod
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p : Submodule R M)
{M' : Type u_9}
[AddCommMonoid M']
[Module R M']
(q₁ : Submodule R M')
:
The product of two submodules is a submodule.
Instances For
@[simp]
theorem
Submodule.prod_coe
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p : Submodule R M)
{M' : Type u_9}
[AddCommMonoid M']
[Module R M']
(q₁ : Submodule R M')
:
theorem
Submodule.span_prod_le
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{M' : Type u_9}
[AddCommMonoid M']
[Module R M']
(s : Set M)
(t : Set M')
:
Submodule.span R (s ×ˢ t) ≤ (Submodule.span R s).prod (Submodule.span R t)
@[simp]
theorem
Submodule.prod_top
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{M' : Type u_9}
[AddCommMonoid M']
[Module R M']
:
@[simp]
theorem
Submodule.prod_bot
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{M' : Type u_9}
[AddCommMonoid M']
[Module R M']
:
theorem
Submodule.prod_mono
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{M' : Type u_9}
[AddCommMonoid M']
[Module R M']
{p p' : Submodule R M}
{q q' : Submodule R M'}
:
@[simp]
theorem
Submodule.span_neg
{R : Type u_1}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
(s : Set M)
:
Submodule.span R (-s) = Submodule.span R s
instance
Submodule.instIsModularLattice
{R : Type u_1}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
:
IsModularLattice (Submodule R M)
theorem
Submodule.isCompl_comap_subtype_of_isCompl_of_le
{R : Type u_1}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{p q r : Submodule R M}
(h₁ : IsCompl q r)
(h₂ : q ≤ p)
:
IsCompl (Submodule.comap p.subtype q) (Submodule.comap p.subtype r)
theorem
Submodule.comap_map_eq
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[Semiring R₂]
[AddCommGroup M]
[Module R M]
[AddCommGroup M₂]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
[RingHomSurjective τ₁₂]
{F : Type u_8}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
(f : F)
(p : Submodule R M)
:
Submodule.comap f (Submodule.map f p) = p ⊔ LinearMap.ker f
theorem
Submodule.comap_map_eq_self
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[Semiring R₂]
[AddCommGroup M]
[Module R M]
[AddCommGroup M₂]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
[RingHomSurjective τ₁₂]
{F : Type u_8}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
{f : F}
{p : Submodule R M}
(h : LinearMap.ker f ≤ p)
:
Submodule.comap f (Submodule.map f p) = p
theorem
LinearMap.range_domRestrict_eq_range_iff
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[Semiring R₂]
[AddCommGroup M]
[Module R M]
[AddCommGroup M₂]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
[RingHomSurjective τ₁₂]
{f : M →ₛₗ[τ₁₂] M₂}
{S : Submodule R M}
:
LinearMap.range (f.domRestrict S) = LinearMap.range f ↔ S ⊔ LinearMap.ker f = ⊤
@[simp]
theorem
LinearMap.surjective_domRestrict_iff
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[Semiring R₂]
[AddCommGroup M]
[Module R M]
[AddCommGroup M₂]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
[RingHomSurjective τ₁₂]
{f : M →ₛₗ[τ₁₂] M₂}
{S : Submodule R M}
(hf : Function.Surjective ⇑f)
:
Function.Surjective ⇑(f.domRestrict S) ↔ S ⊔ LinearMap.ker f = ⊤
@[simp]
theorem
Submodule.biSup_comap_subtype_eq_top
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommGroup M]
[Module R M]
{ι : Type u_9}
(s : Set ι)
(p : ι → Submodule R M)
:
⨆ i ∈ s, Submodule.comap (⨆ i ∈ s, p i).subtype (p i) = ⊤
theorem
Submodule.biSup_comap_eq_top_of_surjective
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[Semiring R₂]
[AddCommGroup M]
[Module R M]
[AddCommGroup M₂]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
[RingHomSurjective τ₁₂]
{ι : Type u_9}
(s : Set ι)
(hs : s.Nonempty)
(p : ι → Submodule R₂ M₂)
(hp : ⨆ i ∈ s, p i = ⊤)
(f : M →ₛₗ[τ₁₂] M₂)
(hf : Function.Surjective ⇑f)
:
⨆ i ∈ s, Submodule.comap f (p i) = ⊤
theorem
Submodule.biSup_comap_eq_top_of_range_eq_biSup
{M : Type u_4}
{M₂ : Type u_5}
[AddCommGroup M]
[AddCommGroup M₂]
{R : Type u_9}
{R₂ : Type u_10}
[Ring R]
[Ring R₂]
{τ₁₂ : R →+* R₂}
[RingHomSurjective τ₁₂]
[Module R M]
[Module R₂ M₂]
{ι : Type u_11}
(s : Set ι)
(hs : s.Nonempty)
(p : ι → Submodule R₂ M₂)
(f : M →ₛₗ[τ₁₂] M₂)
(hf : LinearMap.range f = ⨆ i ∈ s, p i)
:
⨆ i ∈ s, Submodule.comap f (p i) = ⊤
theorem
Submodule.wcovBy_span_singleton_sup
{K : Type u_3}
{V : Type u_6}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
(x : V)
(p : Submodule K V)
:
p ⩿ Submodule.span K {x} ⊔ p
There is no vector subspace between p and (K ∙ x) ⊔ p, WCovBy version.
theorem
Submodule.covBy_span_singleton_sup
{K : Type u_3}
{V : Type u_6}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{x : V}
{p : Submodule K V}
(h : x ∉ p)
:
p ⋖ Submodule.span K {x} ⊔ p
There is no vector subspace between p and (K ∙ x) ⊔ p, CovBy version.
theorem
LinearMap.map_le_map_iff
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[Semiring R₂]
[AddCommGroup M]
[AddCommGroup M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
[RingHomSurjective τ₁₂]
{F : Type u_8}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
(f : F)
{p p' : Submodule R M}
:
Submodule.map f p ≤ Submodule.map f p' ↔ p ≤ p' ⊔ LinearMap.ker f
theorem
LinearMap.map_le_map_iff'
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[Semiring R₂]
[AddCommGroup M]
[AddCommGroup M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
[RingHomSurjective τ₁₂]
{F : Type u_8}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
{f : F}
(hf : LinearMap.ker f = ⊥)
{p p' : Submodule R M}
:
Submodule.map f p ≤ Submodule.map f p' ↔ p ≤ p'
theorem
LinearMap.map_injective
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[Semiring R₂]
[AddCommGroup M]
[AddCommGroup M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
[RingHomSurjective τ₁₂]
{F : Type u_8}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
{f : F}
(hf : LinearMap.ker f = ⊥)
:
theorem
LinearMap.map_eq_top_iff
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[Semiring R₂]
[AddCommGroup M]
[AddCommGroup M₂]
[Module R M]
[Module R₂ M₂]
{τ₁₂ : R →+* R₂}
[RingHomSurjective τ₁₂]
{F : Type u_8}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
{f : F}
(hf : LinearMap.range f = ⊤)
{p : Submodule R M}
:
Submodule.map f p = ⊤ ↔ p ⊔ LinearMap.ker f = ⊤
def
LinearMap.toSpanSingleton
(R : Type u_1)
(M : Type u_4)
[Semiring R]
[AddCommMonoid M]
[Module R M]
(x : M)
:
Given an element x of a module M over R, the natural map from
R to scalar multiples of x. See also LinearMap.ringLmapEquivSelf.
Equations
- LinearMap.toSpanSingleton R M x = LinearMap.id.smulRight x
Instances For
@[simp]
theorem
LinearMap.toSpanSingleton_apply
(R : Type u_1)
(M : Type u_4)
[Semiring R]
[AddCommMonoid M]
[Module R M]
(x : M)
(b : R)
:
(LinearMap.toSpanSingleton R M x) b = b • x
theorem
LinearMap.span_singleton_eq_range
(R : Type u_1)
(M : Type u_4)
[Semiring R]
[AddCommMonoid M]
[Module R M]
(x : M)
:
Submodule.span R {x} = LinearMap.range (LinearMap.toSpanSingleton R M x)
The range of toSpanSingleton x is the span of x.
theorem
LinearMap.toSpanSingleton_one
(R : Type u_1)
(M : Type u_4)
[Semiring R]
[AddCommMonoid M]
[Module R M]
(x : M)
:
(LinearMap.toSpanSingleton R M x) 1 = x
@[simp]
theorem
LinearMap.toSpanSingleton_zero
(R : Type u_1)
(M : Type u_4)
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
LinearMap.toSpanSingleton R M 0 = 0
theorem
LinearMap.isIdempotentElem_apply_one_iff
{R : Type u_1}
[Semiring R]
{f : Module.End R R}
:
IsIdempotentElem (f 1) ↔ IsIdempotentElem f
theorem
LinearMap.eqOn_span_iff
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Semiring R₂]
[AddCommMonoid M₂]
[Module R₂ M₂]
{F : Type u_8}
{σ₁₂ : R →+* R₂}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
{s : Set M}
{f g : F}
:
Set.EqOn ⇑f ⇑g ↑(Submodule.span R s) ↔ Set.EqOn (⇑f) (⇑g) s
Two linear maps are equal on Submodule.span s iff they are equal on s.
theorem
LinearMap.eqOn_span'
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Semiring R₂]
[AddCommMonoid M₂]
[Module R₂ M₂]
{F : Type u_8}
{σ₁₂ : R →+* R₂}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
{s : Set M}
{f g : F}
(H : Set.EqOn (⇑f) (⇑g) s)
:
Set.EqOn ⇑f ⇑g ↑(Submodule.span R s)
If two linear maps are equal on a set s, then they are equal on Submodule.span s.
This version uses Set.EqOn, and the hidden argument will expand to h : x ∈ (span R s : Set M).
See LinearMap.eqOn_span for a version that takes h : x ∈ span R s as an argument.
theorem
LinearMap.eqOn_span
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Semiring R₂]
[AddCommMonoid M₂]
[Module R₂ M₂]
{F : Type u_8}
{σ₁₂ : R →+* R₂}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
{s : Set M}
{f g : F}
(H : Set.EqOn (⇑f) (⇑g) s)
⦃x : M⦄
(h : x ∈ Submodule.span R s)
:
f x = g x
If two linear maps are equal on a set s, then they are equal on Submodule.span s.
See also LinearMap.eqOn_span' for a version using Set.EqOn.
theorem
LinearMap.ext_on
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Semiring R₂]
[AddCommMonoid M₂]
[Module R₂ M₂]
{F : Type u_8}
{σ₁₂ : R →+* R₂}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
{s : Set M}
{f g : F}
(hv : Submodule.span R s = ⊤)
(h : Set.EqOn (⇑f) (⇑g) s)
:
f = g
If s generates the whole module and linear maps f, g are equal on s, then they are
equal.
theorem
LinearMap.ext_on_range
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Semiring R₂]
[AddCommMonoid M₂]
[Module R₂ M₂]
{F : Type u_8}
{σ₁₂ : R →+* R₂}
[FunLike F M M₂]
[SemilinearMapClass F σ₁₂ M M₂]
{ι : Sort u_9}
{v : ι → M}
{f g : F}
(hv : Submodule.span R (Set.range v) = ⊤)
(h : ∀ (i : ι), f (v i) = g (v i))
:
f = g
If the range of v : ι → M generates the whole module and linear maps f, g are equal at
each v i, then they are equal.
theorem
LinearMap.ker_toSpanSingleton
(R : Type u_1)
(M : Type u_4)
[Ring R]
[AddCommGroup M]
[Module R M]
[NoZeroSMulDivisors R M]
{x : M}
(h : x ≠ 0)
:
LinearMap.ker (LinearMap.toSpanSingleton R M x) = ⊥
theorem
LinearMap.span_singleton_sup_ker_eq_top
{K : Type u_3}
{V : Type u_6}
[Field K]
[AddCommGroup V]
[Module K V]
(f : V →ₗ[K] K)
{x : V}
(hx : f x ≠ 0)
:
Submodule.span K {x} ⊔ LinearMap.ker f = ⊤
noncomputable def
LinearEquiv.toSpanNonzeroSingleton
(R : Type u_1)
(M : Type u_4)
[Ring R]
[AddCommGroup M]
[Module R M]
[NoZeroSMulDivisors R M]
(x : M)
(h : x ≠ 0)
:
R ≃ₗ[R] ↥(Submodule.span R {x})
Given a nonzero element x of a torsion-free module M over a ring R, the natural
isomorphism from R to the span of x given by $r \mapsto r \cdot x$.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
LinearEquiv.toSpanNonzeroSingleton_apply
(R : Type u_1)
(M : Type u_4)
[Ring R]
[AddCommGroup M]
[Module R M]
[NoZeroSMulDivisors R M]
(x : M)
(h : x ≠ 0)
(t : R)
:
(LinearEquiv.toSpanNonzeroSingleton R M x h) t = ⟨t • x, ⋯⟩
theorem
LinearEquiv.toSpanNonzeroSingleton_one
(R : Type u_1)
(M : Type u_4)
[Ring R]
[AddCommGroup M]
[Module R M]
[NoZeroSMulDivisors R M]
(x : M)
(h : x ≠ 0)
:
(LinearEquiv.toSpanNonzeroSingleton R M x h) 1 = ⟨x, ⋯⟩
@[reducible, inline]
noncomputable abbrev
LinearEquiv.coord
(R : Type u_1)
(M : Type u_4)
[Ring R]
[AddCommGroup M]
[Module R M]
[NoZeroSMulDivisors R M]
(x : M)
(h : x ≠ 0)
:
↥(Submodule.span R {x}) ≃ₗ[R] R
Given a nonzero element x of a torsion-free module M over a ring R, the natural
isomorphism from the span of x to R given by $r \cdot x \mapsto r$.
Equations
- LinearEquiv.coord R M x h = (LinearEquiv.toSpanNonzeroSingleton R M x h).symm
Instances For
theorem
LinearEquiv.coord_self
(R : Type u_1)
(M : Type u_4)
[Ring R]
[AddCommGroup M]
[Module R M]
[NoZeroSMulDivisors R M]
(x : M)
(h : x ≠ 0)
:
(LinearEquiv.coord R M x h) ⟨x, ⋯⟩ = 1
theorem
LinearEquiv.coord_apply_smul
(R : Type u_1)
(M : Type u_4)
[Ring R]
[AddCommGroup M]
[Module R M]
[NoZeroSMulDivisors R M]
(x : M)
(h : x ≠ 0)
(y : ↥(Submodule.span R {x}))
:
(LinearEquiv.coord R M x h) y • x = ↑y