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\., not the same as the scalar multiplication•/\bub.
def
Submodule.span
(R : Type u_1)
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(s : Set M)
:
Submodule R M
The span of a set s ⊆ M is the smallest submodule of M that contains s.
Equations
- Submodule.span R s = sInf {p : Submodule R M | s ⊆ ↑p}
Instances For
theorem
Submodule.isPrincipal_iff
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(S : Submodule R M)
:
Submodule.IsPrincipal S ↔ ∃ (a : M), S = Submodule.span R {a}
class
Submodule.IsPrincipal
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(S : Submodule R M)
:
An R-submodule of M is principal if it is generated by one element.
- principal' : ∃ (a : M), S = Submodule.span R {a}
Instances
theorem
Submodule.IsPrincipal.principal
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(S : Submodule R M)
[Submodule.IsPrincipal S]
:
∃ (a : M), S = Submodule.span R {a}
theorem
Submodule.mem_span
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{x : M}
{s : Set M}
:
theorem
Submodule.subset_span
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Set M}
:
s ⊆ ↑(Submodule.span R s)
theorem
Submodule.span_le
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Set M}
{p : Submodule R M}
:
Submodule.span R s ≤ p ↔ s ⊆ ↑p
theorem
Submodule.span_mono
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Set M}
{t : Set M}
(h : s ⊆ t)
:
Submodule.span R s ≤ Submodule.span R t
theorem
Submodule.span_monotone
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
theorem
Submodule.span_eq_of_le
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p : Submodule R M)
{s : Set M}
(h₁ : s ⊆ ↑p)
(h₂ : p ≤ Submodule.span R s)
:
Submodule.span R s = p
theorem
Submodule.span_eq
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p : Submodule R M)
:
Submodule.span R ↑p = p
theorem
Submodule.span_eq_span
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Set M}
{t : Set M}
(hs : s ⊆ ↑(Submodule.span R t))
(ht : t ⊆ ↑(Submodule.span R s))
:
Submodule.span R s = Submodule.span R t
@[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.
@[simp]
theorem
Submodule.span_insert_zero
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Set M}
:
Submodule.span R (insert 0 s) = Submodule.span R s
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.closure_subset_span
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Set M}
:
↑(AddSubmonoid.closure s) ⊆ ↑(Submodule.span R s)
theorem
Submodule.closure_le_toAddSubmonoid_span
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Set M}
:
AddSubmonoid.closure s ≤ (Submodule.span R s).toAddSubmonoid
@[simp]
theorem
Submodule.span_closure
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Set M}
:
Submodule.span R ↑(AddSubmonoid.closure s) = Submodule.span R s
theorem
Submodule.span_induction
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{x : M}
{s : Set M}
{p : M → Prop}
(h : x ∈ Submodule.span R s)
(mem : ∀ x ∈ s, p x)
(zero : p 0)
(add : ∀ (x y : M), p x → p y → p (x + y))
(smul : ∀ (a : R) (x : M), p x → p (a • x))
:
p x
An induction principle for span membership. If p holds for 0 and all elements of s, and is
preserved under addition and scalar multiplication, then p holds for all elements of the span of
s.
theorem
Submodule.span_induction₂
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Set M}
{p : M → M → Prop}
{a : M}
{b : M}
(ha : a ∈ Submodule.span R s)
(hb : b ∈ Submodule.span R s)
(mem_mem : ∀ x ∈ s, ∀ y ∈ s, p x y)
(zero_left : ∀ (y : M), p 0 y)
(zero_right : ∀ (x : M), p x 0)
(add_left : ∀ (x₁ x₂ y : M), p x₁ y → p x₂ y → p (x₁ + x₂) y)
(add_right : ∀ (x y₁ y₂ : M), p x y₁ → p x y₂ → p x (y₁ + y₂))
(smul_left : ∀ (r : R) (x y : M), p x y → p (r • x) y)
(smul_right : ∀ (r : R) (x y : M), p x y → p x (r • y))
:
p a b
An induction principle for span membership. This is a version of Submodule.span_induction
for binary predicates.
theorem
Submodule.span_induction'
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Set M}
{p : (x : M) → x ∈ Submodule.span R s → Prop}
(mem : ∀ (x : M) (h : x ∈ s), p x ⋯)
(zero : p 0 ⋯)
(add : ∀ (x : M) (hx : x ∈ Submodule.span R s) (y : M) (hy : y ∈ Submodule.span R s), p x hx → p y hy → p (x + y) ⋯)
(smul : ∀ (a : R) (x : M) (hx : x ∈ Submodule.span R s), p x hx → p (a • x) ⋯)
{x : M}
(hx : x ∈ Submodule.span R s)
:
p x hx
A dependent version of Submodule.span_induction.
theorem
Submodule.span_eq_closure
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Set M}
:
(Submodule.span R s).toAddSubmonoid = AddSubmonoid.closure (Set.univ • s)
theorem
Submodule.closure_induction
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{x : M}
{s : Set M}
{p : M → Prop}
(h : x ∈ Submodule.span R s)
(zero : p 0)
(add : ∀ (x y : M), p x → p y → p (x + y))
(smul_mem : ∀ (r : R), ∀ x ∈ s, p (r • x))
:
p x
A variant of span_induction that combines ∀ x ∈ s, p x and ∀ r x, p x → p (r • x)
into a single condition ∀ r, ∀ x ∈ s, p (r • x), which can be easier to verify.
theorem
Submodule.closure_induction'
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Set M}
{p : (x : M) → x ∈ Submodule.span R s → Prop}
(zero : p 0 ⋯)
(add : ∀ (x : M) (hx : x ∈ Submodule.span R s) (y : M) (hy : y ∈ Submodule.span R s), p x hx → p y hy → p (x + y) ⋯)
(smul_mem : ∀ (r : R) (x : M) (h : x ∈ s), p (r • x) ⋯)
{x : M}
(hx : x ∈ Submodule.span R s)
:
p x hx
A dependent version of Submodule.closure_induction.
@[simp]
theorem
Submodule.span_span_coe_preimage
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Set M}
:
Submodule.span R (Subtype.val ⁻¹' s) = ⊤
@[simp]
theorem
Submodule.span_setOf_mem_eq_top
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Set M}
:
Submodule.span R {x : ↥(Submodule.span R s) | ↑x ∈ s} = ⊤
theorem
Submodule.span_nat_eq_addSubmonoid_closure
{M : Type u_4}
[AddCommMonoid M]
(s : Set M)
:
(Submodule.span ℕ s).toAddSubmonoid = AddSubmonoid.closure s
@[simp]
theorem
Submodule.span_nat_eq
{M : Type u_4}
[AddCommMonoid M]
(s : AddSubmonoid M)
:
(Submodule.span ℕ ↑s).toAddSubmonoid = s
@[simp]
theorem
Submodule.span_int_eq
{M : Type u_9}
[AddCommGroup M]
(s : AddSubgroup M)
:
Submodule.toAddSubgroup (Submodule.span ℤ ↑s) = s
def
Submodule.gi
(R : Type u_1)
(M : Type u_4)
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
GaloisInsertion (Submodule.span R) SetLike.coe
span forms a Galois insertion with the coercion from submodule to set.
Equations
- Submodule.gi R M = { choice := fun (s : Set M) (x : ↑(Submodule.span R s) ≤ s) => Submodule.span R s, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }
Instances For
@[simp]
theorem
Submodule.span_empty
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
Submodule.span R ∅ = ⊥
@[simp]
theorem
Submodule.span_univ
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
Submodule.span R Set.univ = ⊤
theorem
Submodule.span_union
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(s : Set M)
(t : Set M)
:
Submodule.span R (s ∪ t) = Submodule.span R s ⊔ Submodule.span R t
theorem
Submodule.span_iUnion
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{ι : Sort u_9}
(s : ι → Set M)
:
Submodule.span R (⋃ (i : ι), s i) = ⨆ (i : ι), Submodule.span R (s i)
theorem
Submodule.span_iUnion₂
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{ι : Sort u_10}
{κ : ι → Sort u_9}
(s : (i : ι) → κ i → Set M)
:
Submodule.span R (⋃ (i : ι), ⋃ (j : κ i), s i j) = ⨆ (i : ι), ⨆ (j : κ i), Submodule.span R (s i j)
theorem
Submodule.span_attach_biUnion
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
[DecidableEq M]
{α : Type u_9}
(s : Finset α)
(f : { x : α // x ∈ s } → Finset M)
:
Submodule.span R ↑(Finset.biUnion (Finset.attach s) f) = ⨆ (x : { x : α // x ∈ s }), Submodule.span R ↑(f x)
theorem
Submodule.sup_span
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p : Submodule R M)
{s : Set M}
:
p ⊔ Submodule.span R s = Submodule.span R (↑p ∪ s)
theorem
Submodule.span_sup
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p : Submodule R M)
{s : Set M}
:
Submodule.span R s ⊔ p = Submodule.span R (s ∪ ↑p)
Equations
- Submodule.«term_∙_» = Lean.ParserDescr.trailingNode `Submodule.term_∙_ 1000 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∙ ") (Lean.ParserDescr.cat `term 0))
Instances For
theorem
Submodule.span_eq_iSup_of_singleton_spans
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(s : Set M)
:
Submodule.span R s = ⨆ x ∈ s, Submodule.span R {x}
theorem
Submodule.span_range_eq_iSup
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{ι : Sort u_9}
{v : ι → M}
:
Submodule.span R (Set.range v) = ⨆ (i : ι), Submodule.span R {v i}
theorem
Submodule.span_smul_le
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(s : Set M)
(r : R)
:
Submodule.span R (r • s) ≤ Submodule.span R s
theorem
Submodule.subset_span_trans
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{U : Set M}
{V : Set M}
{W : Set M}
(hUV : U ⊆ ↑(Submodule.span R V))
(hVW : V ⊆ ↑(Submodule.span R W))
:
U ⊆ ↑(Submodule.span R W)
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.mem_sSup_of_directed
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Set (Submodule R M)}
{z : M}
(hs : Set.Nonempty s)
(hdir : DirectedOn (fun (x x_1 : Submodule R M) => x ≤ x_1) s)
:
theorem
Submodule.coe_scott_continuous
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
OmegaCompletePartialOrder.Continuous' 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.exists_add_eq_of_codisjoint
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{p : Submodule R M}
{p' : Submodule R M}
(h : Codisjoint p p')
(x : M)
:
theorem
Submodule.sup_toAddSubgroup
{R : Type u_9}
{M : Type u_10}
[Ring R]
[AddCommGroup M]
[Module R M]
(p : Submodule R M)
(p' : Submodule R M)
:
theorem
Submodule.mem_span_singleton_self
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(x : M)
:
x ∈ Submodule.span R {x}
theorem
Submodule.nontrivial_span_singleton
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{x : M}
(h : x ≠ 0)
:
Nontrivial ↥(Submodule.span R {x})
theorem
Submodule.mem_span_singleton
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{x : M}
{y : M}
:
x ∈ Submodule.span R {y} ↔ ∃ (a : R), a • y = x
theorem
Submodule.le_span_singleton_iff
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Submodule R M}
{v₀ : M}
:
s ≤ Submodule.span R {v₀} ↔ ∀ v ∈ s, ∃ (r : R), r • v₀ = v
theorem
Submodule.span_singleton_eq_top_iff
(R : Type u_1)
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(x : M)
:
@[simp]
theorem
Submodule.span_zero_singleton
(R : Type u_1)
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
Submodule.span R {0} = ⊥
theorem
Submodule.span_singleton_eq_range
(R : Type u_1)
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(y : M)
:
↑(Submodule.span R {y}) = Set.range fun (x : R) => x • y
theorem
Submodule.span_singleton_smul_le
(R : Type u_1)
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{S : Type u_9}
[Monoid S]
[SMul S R]
[MulAction S M]
[IsScalarTower S R M]
(r : S)
(x : M)
:
Submodule.span R {r • x} ≤ Submodule.span R {x}
theorem
Submodule.span_singleton_group_smul_eq
(R : Type u_1)
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{G : Type u_9}
[Group G]
[SMul G R]
[MulAction G M]
[IsScalarTower G R M]
(g : G)
(x : M)
:
Submodule.span R {g • x} = Submodule.span R {x}
theorem
Submodule.span_singleton_smul_eq
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{r : R}
(hr : IsUnit r)
(x : M)
:
Submodule.span R {r • x} = Submodule.span R {x}
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.mem_span_singleton_trans
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{x : M}
{y : M}
{z : M}
(hxy : x ∈ Submodule.span R {y})
(hyz : y ∈ Submodule.span R {z})
:
x ∈ Submodule.span R {z}
theorem
Submodule.span_insert
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(x : M)
(s : Set M)
:
Submodule.span R (insert x s) = Submodule.span R {x} ⊔ Submodule.span R s
theorem
Submodule.span_insert_eq_span
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{x : M}
{s : Set M}
(h : x ∈ Submodule.span R s)
:
Submodule.span R (insert x s) = Submodule.span R s
theorem
Submodule.span_span
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Set M}
:
Submodule.span R ↑(Submodule.span R s) = Submodule.span R s
theorem
Submodule.mem_span_insert
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{x : M}
{s : Set M}
{y : M}
:
x ∈ Submodule.span R (insert y s) ↔ ∃ (a : R), ∃ z ∈ Submodule.span R s, x = a • y + z
theorem
Submodule.mem_span_pair
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{x : M}
{y : M}
{z : 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]
:
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_eq_bot
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{s : Set M}
:
Submodule.span R s = ⊥ ↔ ∀ x ∈ s, x = 0
@[simp]
theorem
Submodule.span_singleton_eq_bot
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{x : M}
:
Submodule.span R {x} = ⊥ ↔ x = 0
@[simp]
theorem
Submodule.span_zero
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
Submodule.span R 0 = ⊥
@[simp]
theorem
Submodule.span_singleton_le_iff_mem
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(m : M)
(p : Submodule R M)
:
Submodule.span R {m} ≤ p ↔ m ∈ p
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 : M}
{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 (Submodule.subtype p) (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_span
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{ι : Sort u_9}
(p : ι → Set M)
:
⨆ (i : ι), Submodule.span R (p i) = Submodule.span R (⋃ (i : ι), p i)
theorem
Submodule.iSup_eq_span
{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 = Submodule.span R (⋃ (i : ι), ↑(p i))
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 : Set.Finite S)
:
The span of a finite subset is compact in the lattice of submodules.
instance
Submodule.instIsCompactlyGeneratedSubmoduleCompleteLattice
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
:
Equations
- ⋯ = ⋯
theorem
Submodule.submodule_eq_sSup_le_nonzero_spans
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p : Submodule R M)
:
A submodule is equal to the supremum of the spans of the submodule's nonzero elements.
theorem
Submodule.lt_sup_iff_not_mem
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{I : Submodule R M}
{a : M}
:
I < I ⊔ Submodule.span R {a} ↔ a ∉ I
theorem
Submodule.mem_span_finite_of_mem_span
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{S : Set M}
{x : M}
(hx : x ∈ Submodule.span R S)
:
∃ (T : Finset M), ↑T ⊆ S ∧ x ∈ Submodule.span R ↑T
For every element in the span of a set, there exists a finite subset of the set such that the element is contained in the span of the subset.
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.
Equations
- One or more equations did not get rendered due to their size.
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')
:
↑(Submodule.prod p q₁) = ↑p ×ˢ ↑q₁
@[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'}
:
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.prod (Submodule.span R s) (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 : Submodule R M}
{p' : Submodule R M}
{q : Submodule R M'}
{q' : Submodule R M'}
:
p ≤ p' → q ≤ q' → Submodule.prod p q ≤ Submodule.prod p' q'
@[simp]
theorem
Submodule.prod_inf_prod
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p : Submodule R M)
(p' : Submodule R M)
{M' : Type u_9}
[AddCommMonoid M']
[Module R M']
(q₁ : Submodule R M')
(q₁' : Submodule R M')
:
Submodule.prod p q₁ ⊓ Submodule.prod p' q₁' = Submodule.prod (p ⊓ p') (q₁ ⊓ q₁')
@[simp]
theorem
Submodule.prod_sup_prod
{R : Type u_1}
{M : Type u_4}
[Semiring R]
[AddCommMonoid M]
[Module R M]
(p : Submodule R M)
(p' : Submodule R M)
{M' : Type u_9}
[AddCommMonoid M']
[Module R M']
(q₁ : Submodule R M')
(q₁' : Submodule R M')
:
Submodule.prod p q₁ ⊔ Submodule.prod p' q₁' = Submodule.prod (p ⊔ p') (q₁ ⊔ q₁')
@[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
theorem
Submodule.mem_span_insert'
{R : Type u_1}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
{x : M}
{y : M}
{s : Set M}
:
x ∈ Submodule.span R (insert y s) ↔ ∃ (a : R), x + a • y ∈ Submodule.span R s
instance
Submodule.instIsModularLatticeSubmoduleToSemiringToAddCommMonoidToLatticeToConditionallyCompleteLatticeCompleteLattice
{R : Type u_1}
{M : Type u_4}
[Ring R]
[AddCommGroup M]
[Module R M]
:
IsModularLattice (Submodule R M)
Equations
- ⋯ = ⋯
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 (LinearMap.domRestrict f 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 ⇑(LinearMap.domRestrict f 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 (Submodule.subtype (⨆ i ∈ s, p i)) (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 : Set.Nonempty s)
(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 : Set.Nonempty s)
(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 : Submodule R M}
{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 : Submodule R M}
{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 = ⊤
@[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
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.smulRight LinearMap.id x
Instances For
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 : 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 : 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 : 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 : 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 : 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 = { val := t • x, property := ⋯ }
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 = { val := x, property := ⋯ }
@[inline, reducible]
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.symm (LinearEquiv.toSpanNonzeroSingleton R M x h)
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) { val := x, property := ⋯ } = 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