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]
:
span S ↑p = 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₂)
:
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)
:
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)
:
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₂)
:
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₂)
:
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.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)
:
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]
:
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.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]
:
span R s ≤ restrictScalars R (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]
:
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]
:
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}
:
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)
:
@[simp]
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 ∈ span R 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)
:
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 ∉ span R₂ (⇑f '' s))
:
x ∉ 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)
:
CompleteLattice.IsCompactElement (span R {x})
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')
:
@[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'}
:
instance
Submodule.instIsModularLattice
{R : Type u_1}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
:
IsModularLattice (Submodule R M)
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)
:
comap f (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)
:
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}
:
@[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)
:
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)
:
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)
:
theorem
Submodule.wcovBy_span_singleton_sup
{K : Type u_3}
{V : Type u_6}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
(x : V)
(s : Submodule K V)
:
There is no vector subspace between s and (K ∙ x) ⊔ s, 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}
{s : Submodule K V}
(h : x ∉ s)
:
There is no vector subspace between s and (K ∙ x) ⊔ s, CovBy version.
theorem
Submodule.disjoint_span_singleton
{K : Type u_3}
{V : Type u_6}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Submodule K V}
{x : V}
:
theorem
Submodule.disjoint_span_singleton'
{K : Type u_3}
{V : Type u_6}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Submodule K V}
{x : V}
(x0 : x ≠ 0)
:
theorem
Submodule.disjoint_span_singleton_of_not_mem
{K : Type u_3}
{V : Type u_6}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Submodule K V}
{x : V}
(hx : x ∉ s)
:
theorem
Submodule.isCompl_span_singleton_of_isCoatom_of_not_mem
{K : Type u_3}
{V : Type u_6}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Submodule K V}
{x : V}
(hs : IsCoatom s)
(hx : x ∉ s)
:
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' ⊔ 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 : 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 : 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 : range f = ⊤)
{p : Submodule R M}
:
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)
:
(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} = range (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)
:
(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]
:
toSpanSingleton R M 0 = 0
theorem
LinearMap.toSpanSingleton_isIdempotentElem_iff
{R : Type u_1}
[Semiring R]
{e : R}
:
IsIdempotentElem (toSpanSingleton R R e) ↔ IsIdempotentElem e
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)
:
ker (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} ⊔ 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)
:
(toSpanNonzeroSingleton R M x h) t = ⟨t • x, ⋯⟩
@[simp]
theorem
LinearEquiv.toSpanNonzeroSingleton_symm_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)
(m : ↥(Submodule.span R {x}))
:
(toSpanNonzeroSingleton R M x h).symm m • x = ↑m
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)
:
(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)
:
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}))
: