# The span of a set of vectors, as a submodule #

- `Submodule.span s` is defined to be the smallest submodule containing the set `s`.

## Notation #

- We introduce the notation `R ∙ v` for the span of a singleton, `Submodule.span R {v}`. This is `\span`, not the same as the scalar multiplication `•`/`\bub`.

source
theorem AddSubmonoid.toNatSubmodule_closure {M : Type u_4} [AddCommMonoid M] (s : Set M) :
toNatSubmodule (closure s) = Submodule.span ℕ s
source
@[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.

source
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 '' ↑(span R s) ⊆ ↑N ↔ ∀ m ∈ s, f m ∈ N

A version of `Submodule.map_span_le` that does not require the `RingHomSurjective` assumption.

source
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 '' ↑(span R s) ⊆ ↑(span R₂ (⇑f '' s))
source
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) :
map f (span R s) = span R₂ (⇑f '' s)
source
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`.

source
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₂) :
map f (span R s) ≤ N ↔ ∀ m ∈ s, f m ∈ N
source
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`.

source
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₂) :
span R (⇑f ⁻¹' s) ≤ comap f (span R₂ s)

See also `Submodule.span_preimage_eq`.

source
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`.

See also `Submodule.span_preimage_eq`.

source
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)
source
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`.

source
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 = span R S) :
f = g ↔ ∀ (s : ↑S), f ⟨↑s, ⋯⟩ = g ⟨↑s, ⋯⟩
source
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 : span R S = ⊤) :
f = g ↔ ∀ (s : ↑S), f ↑s = g ↑s
source
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 : span R S = ⊤) :
f = 0 ↔ ∀ (s : ↑S), f ↑s = 0
source
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 = span R S) :
f = 0 ↔ ∀ (s : ↑S), f ⟨↑s, ⋯⟩ = 0
source
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) :
span R (r • s) = 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`.

source
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.

source
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) :
↥p →ₗ[R] ↥(span S ↑p)

The inclusion of an `R`-submodule into its `S`-span, as an `R`-linear map.

Equations

- Submodule.inclusionSpan S p = { toFun := fun (x : ↥p) => ⟨↑x, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source
@[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) :
↑((inclusionSpan S p) x) = ↑x
source
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)
source
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) :
span S (Set.range ⇑(inclusionSpan S p)) = ⊤
source
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`.

source
@[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] :
↑(span R s) ⊆ ↑(span S s)

A version of `Submodule.span_le_restrictScalars` with coercions.

source
@[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] :
span S ↑(span R s) = 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.

source
theorem Submodule.span_eq_top_of_span_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] (s : Set M) (hs : span R s = ⊤) :
span S s = ⊤
source
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) :
span S (Set.range ⇑(inclusion h₁)) = ⊤
source
@[simp]
theorem Submodule.span_range_inclusion_restrictScalars_eq_top (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 S (Set.range ⇑(inclusion ⋯)) = ⊤
source
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} :
span R {x} = span R {y} ↔ ∃ (z : R ˣ), z • x = y
source
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) :
span R₂ (⇑f '' s) = map f (span R s)
source
@[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₂) :
span R₂ (⇑f '' s) = map f (span R s)
source
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) :
f x ∈ span R₂ (⇑f '' s)
source
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 ∈ span R₂ (⇑f '' s) ↔ x ∈ span R s
source
@[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) :
map p.subtype (span R {x}) = span R {↑x}
source
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.

source
@[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.

source
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
source
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`.

source
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`.

source
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})
source
theorem Submodule.finset_span_isCompactElement {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (S : Finset M) :
CompleteLattice.IsCompactElement (span R ↑S)

The span of a finite subset is compact in the lattice of submodules.

source
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) :
CompleteLattice.IsCompactElement (span R S)

The span of a finite subset is compact in the lattice of submodules.

source
instance Submodule.instIsCompactlyGenerated {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] :
IsCompactlyGenerated (Submodule R M)
source
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') :
Submodule R (M × M')

The product of two submodules is a submodule.

Equations

- p.prod q₁ = { carrier := ↑p ×ˢ ↑q₁, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

Instances For

source
@[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') :
↑(p.prod q₁) = ↑p ×ˢ ↑q₁
source
@[simp]
theorem Submodule.mem_prod {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 : Submodule R M} {q : Submodule R M'} {x : M × M'} :
x ∈ p.prod q ↔ x.1 ∈ p ∧ x.2 ∈ q
source
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') :
span R (s ×ˢ t) ≤ (span R s).prod (span R t)
source
@[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'] :
⊤.prod ⊤ = ⊤
source
@[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'] :
⊥.prod ⊥ = ⊥
source
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'} :
p ≤ p' → q ≤ q' → p.prod q ≤ p'.prod q'
source
@[simp]
theorem Submodule.prod_inf_prod {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (p p' : Submodule R M) {M' : Type u_9} [AddCommMonoid M'] [Module R M'] (q₁ q₁' : Submodule R M') :
p.prod q₁ ⊓ p'.prod q₁' = (p ⊓ p').prod (q₁ ⊓ q₁')
source
@[simp]
theorem Submodule.prod_sup_prod {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (p p' : Submodule R M) {M' : Type u_9} [AddCommMonoid M'] [Module R M'] (q₁ q₁' : Submodule R M') :
p.prod q₁ ⊔ p'.prod q₁' = (p ⊔ p').prod (q₁ ⊔ q₁')
source
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) :
(B x) y ∈ P'

If a bilinear map takes values in a submodule along two sets, then the same is true along the span of these sets.

source
@[simp]
theorem Submodule.biSup_comap_subtype_eq_top {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_10} (s : Set ι) (p : ι → Submodule R M) :
⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i) = ⊤
source
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
source
theorem AddSubgroup.toIntSubmodule_closure {M : Type u_4} [AddCommGroup M] (s : Set M) :
toIntSubmodule (closure s) = Submodule.span ℤ s
source
@[simp]
theorem Submodule.span_neg {R : Type u_1} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] (s : Set M) :
span R (-s) = span R s
source
instance Submodule.instIsModularLattice {R : Type u_1} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] :
IsModularLattice (Submodule R M)
source
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 (comap p.subtype q) (comap p.subtype r)
source
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
source
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) :
map f p < map f p'
source
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) :
comap f (map f p) = p
source
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) :
comap f (map f p ⊔ q) = p
source
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) :
IsCoatom (comap f p) ∨ comap f p = ⊤
source
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₂} :
IsCoatom (comap f p) ↔ IsCoatom p
source
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) :
IsCoatom (map f p)
source
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) :
map f (⨅ (i : ι), p i) = ⨅ (i : ι), map f (p i)
source
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) :
comap f p ⋖ comap f q
source
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} :
range (f.domRestrict S) = range f ↔ S ⊔ ker f = ⊤
source
@[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 ⊔ ker f = ⊤
source
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, comap f (p i) = ⊤
source
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) :
⨆ i ∈ s, comap f (p i) = ⊤
source
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') :
map f p < map f p' ∨ LinearMap.ker f ⊓ p < LinearMap.ker f ⊓ p'
source
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') :
ker f ⊓ p < ker f ⊓ p'
source
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') :
map f p < map f p'
source
theorem Submodule.disjoint_span_singleton'' {R : Type u_1} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] {s : Submodule R M} {x : M} :
Disjoint s (span R {x}) ↔ ∀ (r : R), r • x ∈ s → r • x = 0

Version of `disjoint_span_singleton` that works when the scalars are not a field.

source
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) :
s ⩿ span K {x} ⊔ s

There is no vector subspace between `s` and `(K ∙ x) ⊔ s`, `WCovBy` version.

source
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) :
s ⋖ span K {x} ⊔ s

There is no vector subspace between `s` and `(K ∙ x) ⊔ s`, `CovBy` version.

source
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} :
Disjoint s (span K {x}) ↔ x ∈ s → x = 0
source
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} (hx : x ≠ 0) :
Disjoint s (span K {x}) ↔ x ∉ s
source
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) :
Disjoint s (span K {x})
source
@[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) :
Disjoint s (span K {x})

Alias of `Submodule.disjoint_span_singleton_of_notMem`.

source
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) :
IsCompl s (span K {x})
source
@[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) :
IsCompl s (span K {x})

Alias of `Submodule.isCompl_span_singleton_of_isCoatom_of_notMem`.

source
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
source
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'
source
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 = ⊥) :
Function.Injective (Submodule.map f)
source
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} :
Submodule.map f p = ⊤ ↔ p ⊔ ker f = ⊤
source
def LinearMap.toSpanSingleton (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] (x : M) :
R →ₗ[R] 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

source
@[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
source
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
source
theorem LinearMap.toSpanSingleton_injective (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] :
Function.Injective (toSpanSingleton R M)
source
@[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
source
theorem LinearMap.toSpanSingleton_eq_zero_iff (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] {x : M} :
toSpanSingleton R M x = 0 ↔ x = 0
source
theorem LinearMap.toSpanSingleton_add {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (x y : M) :
toSpanSingleton R M (x + y) = toSpanSingleton R M x + toSpanSingleton R M y
source
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) :
toSpanSingleton R M (r • x) = r • toSpanSingleton R M x
source
theorem LinearMap.toSpanSingleton_isIdempotentElem_iff {R : Type u_1} [Semiring R] {e : R} :
IsIdempotentElem (toSpanSingleton R R e) ↔ IsIdempotentElem e
source
theorem LinearMap.isIdempotentElem_apply_one_iff {R : Type u_1} [Semiring R] {f : Module.End R R} :
IsIdempotentElem (f 1) ↔ IsIdempotentElem f
source
theorem LinearMap.range_toSpanSingleton {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) :
range (toSpanSingleton R M x) = Submodule.span R {x}

The range of `toSpanSingleton x` is the span of `x`.

source
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)
source
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) :
f ∘ₗ toSpanSingleton R M x = toSpanSingleton R M₂ (f x)
source
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) :
(Submodule.span R {x}).submoduleOf N = Submodule.span R {⟨x, hx⟩}
source
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`.

source
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.

source
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`.

source
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.

source
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.

source
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) = ⊥
source
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 = ⊤
source
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

source
@[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, ⋯⟩
source
@[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
source
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, ⋯⟩
source
@[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

source
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) :
(coord R M x h) ⟨x, ⋯⟩ = 1
source
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})) :
(coord R M x h) y • x = ↑y