Bases of submodules

theorem Module.Basis.mem_submodule_iff {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {P : Submodule R M} (b : Basis ι R ↥P) {x : M} : x ∈ P ↔ ∃ (c : ι →₀ R), x = c.sum fun (i : ι) (x : R) => x • ↑(b i)

If the submodule P has a basis, x ∈ P iff it is a linear combination of basis vectors.

theorem Module.Basis.mem_submodule_iff' {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Fintype ι] {P : Submodule R M} (b : Basis ι R ↥P) {x : M} : x ∈ P ↔ ∃ (c : ι → R), x = ∑ i : ι, c i • ↑(b i)

If the submodule P has a finite basis, x ∈ P iff it is a linear combination of basis vectors.

theorem Module.Basis.eq_bot_of_rank_eq_zero {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] [NoZeroDivisors R] (b : Basis ι R M) (N : Submodule R M) (rank_eq : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m = 0) : N = ⊥

def Submodule.inductionOnRankAux {ι : Type u_1} {R : Type u_3} {M : Type u_5} [Ring R] [IsDomain R] [AddCommGroup M] [Module R M] (b : Module.Basis ι R M) (P : Submodule R M → Sort u_7) (ih : (N : Submodule R M) → ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N) (n : ℕ) (N : Submodule R M) (rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m ≤ n) : P N

If N is a submodule with finite rank, do induction on adjoining a linear independent element to a submodule.

Equations

• One or more equations did not get rendered due to their size.

theorem Module.Basis.mem_center_iff {ι : Type u_1} {R : Type u_3} {A : Type u_7} [Semiring R] [NonUnitalNonAssocSemiring A] [Module R A] [SMulCommClass R A A] [SMulCommClass R R A] [IsScalarTower R A A] (b : Basis ι R A) {z : A} : z ∈ Set.center A ↔ (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)

An element of a non-unital-non-associative algebra is in the center exactly when it commutes with the basis elements.

noncomputable def Module.Basis.restrictScalars {ι : Type u_1} (R : Type u_3) {M : Type u_5} {S : Type u_7} [CommRing R] [Ring S] [Nontrivial S] [AddCommGroup M] [Algebra R S] [Module S M] [Module R M] [IsScalarTower R S M] [NoZeroSMulDivisors R S] (b : Basis ι S M) : Basis ι R ↥(Submodule.span R (Set.range ⇑b))

Let b be an S-basis of M. Let R be a CommRing such that Algebra R S has no zero smul divisors, then the submodule of M spanned by b over R admits b as an R-basis.

Equations

• Module.Basis.restrictScalars R b = Module.Basis.span ⋯

@[simp]

theorem Module.Basis.restrictScalars_apply {ι : Type u_1} (R : Type u_3) {M : Type u_5} {S : Type u_7} [CommRing R] [Ring S] [Nontrivial S] [AddCommGroup M] [Algebra R S] [Module S M] [Module R M] [IsScalarTower R S M] [NoZeroSMulDivisors R S] (b : Basis ι S M) (i : ι) : ↑((restrictScalars R b) i) = b i

@[simp]

theorem Module.Basis.restrictScalars_repr_apply {ι : Type u_1} (R : Type u_3) {M : Type u_5} {S : Type u_7} [CommRing R] [Ring S] [Nontrivial S] [AddCommGroup M] [Algebra R S] [Module S M] [Module R M] [IsScalarTower R S M] [NoZeroSMulDivisors R S] (b : Basis ι S M) (m : ↥(Submodule.span R (Set.range ⇑b))) (i : ι) : (algebraMap R S) (((restrictScalars R b).repr m) i) = (b.repr ↑m) i

theorem Module.Basis.mem_span_iff_repr_mem {ι : Type u_1} (R : Type u_3) {M : Type u_5} {S : Type u_7} [CommRing R] [Ring S] [Nontrivial S] [AddCommGroup M] [Algebra R S] [Module S M] [Module R M] [IsScalarTower R S M] [NoZeroSMulDivisors R S] (b : Basis ι S M) (m : M) : m ∈ Submodule.span R (Set.range ⇑b) ↔ ∀ (i : ι), (b.repr m) i ∈ Set.range ⇑(algebraMap R S)

Let b be an S-basis of M. Then m : M lies in the R-module spanned by b iff all the coordinates of m on the basis b are in R (see Basis.mem_span for the case R = S).

noncomputable def Module.Basis.addSubgroupOfClosure {M : Type u_7} {R : Type u_8} [Ring R] [Nontrivial R] [NoZeroSMulDivisors ℤ R] [AddCommGroup M] [Module R M] (A : AddSubgroup M) {ι : Type u_9} (b : Basis ι R M) (h : A = AddSubgroup.closure (Set.range ⇑b)) : Basis ι ℤ ↥(AddSubgroup.toIntSubmodule A)

Let A be an subgroup of an additive commutative group M that is also an R-module. Construct a basis of A as a ℤ-basis from a R-basis of E that generates A.

Equations

• Module.Basis.addSubgroupOfClosure A b h = (Module.Basis.restrictScalars ℤ b).map (LinearEquiv.ofEq (Submodule.span ℤ (Set.range ⇑b)) (AddSubgroup.toIntSubmodule A) ⋯)

@[simp]

theorem Module.Basis.addSubgroupOfClosure_apply {M : Type u_7} {R : Type u_8} [Ring R] [Nontrivial R] [NoZeroSMulDivisors ℤ R] [AddCommGroup M] [Module R M] (A : AddSubgroup M) {ι : Type u_9} (b : Basis ι R M) (h : A = AddSubgroup.closure (Set.range ⇑b)) (i : ι) : ↑((addSubgroupOfClosure A b h) i) = b i

@[simp]

theorem Module.Basis.addSubgroupOfClosure_repr_apply {M : Type u_7} {R : Type u_8} [Ring R] [Nontrivial R] [NoZeroSMulDivisors ℤ R] [AddCommGroup M] [Module R M] (A : AddSubgroup M) {ι : Type u_9} (b : Basis ι R M) (h : A = AddSubgroup.closure (Set.range ⇑b)) (x : ↥A) (i : ι) : ↑(((addSubgroupOfClosure A b h).repr x) i) = (b.repr ↑x) i