The span of a set of vectors, as a submodule #
Submodule.span sis defined to be the smallest submodule containing the sets.
Notation #
- 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]
:
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)
:
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₂)
:
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₂)
:
See also Submodule.span_preimage_eq.
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₂)
:
Alias of Submodule.span_preimage_le.
See also Submodule.span_preimage_eq.
theorem
Submodule.mapsTo_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}
{t : Set M₂}
(h : Set.MapsTo (⇑f) s t)
:
Set.MapsTo ⇑f ↑(span R s) ↑(span R₂ t)
theorem
Set.MapsTo.submoduleSpan
{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}
{t : Set M₂}
(h : MapsTo (⇑f) s t)
:
MapsTo ⇑f ↑(Submodule.span R s) ↑(Submodule.span R₂ t)
Alias of Submodule.mapsTo_span.
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.
def
Submodule.inclusionSpan
{R : Type u_1}
{M : Type u_4}
(S : Type u_7)
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Semiring S]
[SMul R S]
[Module S M]
[IsScalarTower R S M]
(p : Submodule R M)
:
The inclusion of an R-submodule into its S-span, as an R-linear map.
Equations
Instances For
@[simp]
theorem
Submodule.inclusionSpan_apply_coe
{R : Type u_1}
{M : Type u_4}
(S : Type u_7)
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Semiring S]
[SMul R S]
[Module S M]
[IsScalarTower R S M]
(p : Submodule R M)
(x : ↥p)
:
theorem
Submodule.injective_inclusionSpan
{R : Type u_1}
{M : Type u_4}
(S : Type u_7)
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Semiring S]
[SMul R S]
[Module S M]
[IsScalarTower R S M]
(p : Submodule R M)
:
Function.Injective ⇑(inclusionSpan S p)
theorem
Submodule.span_range_inclusionSpan
{R : Type u_1}
{M : Type u_4}
(S : Type u_7)
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Semiring S]
[SMul R S]
[Module S M]
[IsScalarTower R S M]
(p : Submodule R M)
:
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]
:
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.
@[simp]
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_range_inclusion_eq_top
{R : Type u_1}
{M : Type u_4}
{S : Type u_7}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[Semiring S]
[SMul R S]
[Module S M]
[IsScalarTower R S M]
(p : Submodule R M)
(q : Submodule S M)
(h₁ : p ≤ restrictScalars R q)
(h₂ : q ≤ span S ↑p)
:
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.notMem_span_of_apply_notMem_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.
@[deprecated Submodule.notMem_span_of_apply_notMem_span_image (since := "2025-05-23")]
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
Alias of Submodule.notMem_span_of_apply_notMem_span_image.
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)
:
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)
{motive : M → Prop}
{x : M}
(hx : x ∈ ⨆ (i : ι), p i)
(mem : ∀ (i : ι), ∀ x ∈ p i, motive x)
(zero : motive 0)
(add : ∀ (x y : M), motive x → motive y → motive (x + y))
:
motive 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)
{motive : (x : M) → x ∈ ⨆ (i : ι), p i → Prop}
(mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), motive x ⋯)
(zero : motive 0 ⋯)
(add : ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), p i) (hy : y ∈ ⨆ (i : ι), p i), motive x hx → motive y hy → motive (x + y) ⋯)
{x : M}
(hx : x ∈ ⨆ (i : ι), p i)
:
motive 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')
:
@[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
LinearMap.BilinMap.apply_apply_mem_of_mem_span
{R : Type u_10}
{M : Type u_11}
{N : Type u_12}
{P : Type u_13}
[CommSemiring R]
[AddCommMonoid M]
[AddCommMonoid N]
[AddCommMonoid P]
[Module R M]
[Module R N]
[Module R P]
(P' : Submodule R P)
(s : Set M)
(t : Set N)
(B : M →ₗ[R] N →ₗ[R] P)
(hB : ∀ x ∈ s, ∀ y ∈ t, (B x) y ∈ P')
(x : M)
(y : N)
(hx : x ∈ Submodule.span R s)
(hy : y ∈ Submodule.span R t)
:
If a bilinear map takes values in a submodule along two sets, then the same is true along the span of these sets.
theorem
LinearMap.exists_ne_zero_of_sSup_eq
{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₂]
{N : Submodule R M}
{f : ↥N →ₛₗ[σ₁₂] M₂}
(h : f ≠ 0)
(s : Set (Submodule R M))
(hs : sSup s = N)
:
∃ (m : Submodule R M) (h : m ∈ s), f ∘ₛₗ Submodule.inclusion ⋯ ≠ 0
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)
:
theorem
Submodule.map_lt_map_of_le_of_sup_lt_sup
{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₂]
{p p' : Submodule R M}
{f : F}
(hab : p ≤ p')
(h : p ⊔ LinearMap.ker f < 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
Submodule.comap_map_sup_of_comap_le
{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}
{q : Submodule R₂ M₂}
(le : comap f q ≤ p)
:
theorem
Submodule.isCoatom_comap_or_eq_top
{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₂}
(hp : IsCoatom p)
:
theorem
Submodule.isCoatom_comap_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 : Type u_8}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
{f : F}
(hf : Function.Surjective ⇑f)
{p : Submodule R₂ M₂}
:
theorem
Submodule.isCoatom_map_of_ker_le
{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}
(hf : Function.Surjective ⇑f)
{p : Submodule R M}
(le : LinearMap.ker f ≤ p)
(hp : IsCoatom p)
:
theorem
Submodule.map_iInf_of_ker_le
{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}
(hf : Function.Surjective ⇑f)
{ι : Sort u_9}
{p : ι → Submodule R M}
(h : LinearMap.ker f ≤ ⨅ (i : ι), p i)
:
theorem
Submodule.comap_covBy_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 τ₁₂]
{F : Type u_8}
[FunLike F M M₂]
[SemilinearMapClass F τ₁₂ M M₂]
{f : F}
(hf : Function.Surjective ⇑f)
{p q : Submodule R₂ M₂}
(h : p ⋖ q)
:
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}
[Semiring 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.map_strict_mono_or_ker_sup_lt_ker_sup
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[Ring 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₂]
{p p' : Submodule R M}
(f : F)
(hab : p < p')
:
theorem
LinearMap.ker_inf_lt_ker_inf_of_map_eq_of_lt
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[Ring 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₂]
{p p' : Submodule R M}
{f : F}
(hab : p < p')
(q : Submodule.map f p = Submodule.map f p')
:
theorem
Submodule.map_strict_mono_of_ker_inf_eq
{R : Type u_1}
{R₂ : Type u_2}
{M : Type u_4}
{M₂ : Type u_5}
[Ring 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₂]
{p p' : Submodule R M}
{f : F}
(hab : p < p')
(q : LinearMap.ker f ⊓ p = LinearMap.ker f ⊓ p')
:
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_notMem
{K : Type u_3}
{V : Type u_6}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
{s : Submodule K V}
{x : V}
(hx : x ∉ s)
:
@[deprecated Submodule.disjoint_span_singleton_of_notMem (since := "2025-05-23")]
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_notMem
{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)
:
@[deprecated Submodule.isCompl_span_singleton_of_isCoatom_of_notMem (since := "2025-05-23")]
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)
:
Alias of Submodule.isCompl_span_singleton_of_isCoatom_of_notMem.
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}
:
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}
:
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
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)
:
theorem
LinearMap.toSpanSingleton_one
(R : Type u_1)
(M : Type u_4)
[Semiring R]
[AddCommMonoid M]
[Module R M]
(x : M)
:
theorem
LinearMap.toSpanSingleton_injective
(R : Type u_1)
(M : Type u_4)
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
@[simp]
theorem
LinearMap.toSpanSingleton_zero
(R : Type u_1)
(M : Type u_4)
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
theorem
LinearMap.toSpanSingleton_eq_zero_iff
(R : Type u_1)
(M : Type u_4)
[Semiring R]
[AddCommMonoid M]
[Module R M]
{x : M}
:
theorem
LinearMap.toSpanSingleton_add
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(x y : M)
:
theorem
LinearMap.toSpanSingleton_smul
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{S : Type u_8}
[Monoid S]
[DistribMulAction S M]
[SMulCommClass R S M]
(r : S)
(x : M)
:
theorem
LinearMap.range_toSpanSingleton
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(x : M)
:
The range of toSpanSingleton x is the span of x.
theorem
LinearMap.span_singleton_eq_range
(R : Type u_1)
(M : Type u_4)
[Semiring R]
[AddCommMonoid M]
[Module R M]
(x : M)
:
theorem
LinearMap.comp_toSpanSingleton
{R : Type u_1}
{M : Type u_4}
{M₂ : Type u_5}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[AddCommMonoid M₂]
[Module R M₂]
(f : M →ₗ[R] M₂)
(x : M)
:
theorem
LinearMap.submoduleOf_span_singleton_of_mem
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(N : Submodule R M)
{x : M}
(hx : x ∈ N)
:
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}
:
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)
:
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)
:
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))
:
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)
:
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)
:
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)
:
@[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}))
:
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)
:
@[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)
:
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}))
: