Submodule.nonempty_basis_of_pid
theorem Submodule.nonempty_basis_of_pid :
∀ {R : Type u_2} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R] {M : Type u_3}
[inst_3 : AddCommGroup M] [inst_4 : Module R M] {ι : Type u_4} [inst_5 : Finite ι],
Basis ι R M → ∀ (N : Submodule R M), ∃ n, Nonempty (Basis (Fin n) R ↥N)
This theorem states that for any principal ideal domain `R`, if we have a free `R`-module of finite rank (represented by `M`), then any submodule `N` of `M` is also a free `R`-module of finite rank. More specifically, if we have a basis for `M`, then there exists a corresponding basis for `N`.
This theorem is a tool for simplifying induction proofs, hence it's described as a `lemma`. To actually retrieve the basis for the submodule `N`, one should refer to the `Submodule.basisOfPid`. A stronger version of this theorem is provided by `Submodule.smithNormalForm`.
More concisely: In a principal ideal domain `R`, any submodule `N` of a free `R`-module of finite rank `M` is itself a free `R`-module of finite rank, and there exists a basis for `N` that can be obtained from a basis for `M`.
|
Ideal.selfBasis_def
theorem Ideal.selfBasis_def :
∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R]
{S : Type u_4} [inst_3 : CommRing S] [inst_4 : IsDomain S] [inst_5 : Algebra R S] [inst_6 : Finite ι]
(b : Basis ι R S) (I : Ideal S) (hI : I ≠ ⊥) (i : ι),
↑((Ideal.selfBasis b I hI) i) = Ideal.smithCoeffs b I hI i • (Ideal.ringBasis b I hI) i
The theorem `Ideal.selfBasis_def` states that for a finite-dimensional ring extension `S` of a principal ideal domain (PID) `R`, which is free as an `R`-module, and any non-zero `S`-ideal `I`, we can establish a basis for `S` and `I` such that the inclusion map is a square diagonal matrix. Specifically, if we have such a basis `b` and an element `i` of the index set of the basis, the `i`th element of the `S`-basis of `I` (in the context of the `R`-module structure on `S`) is the `i`th Smith coefficient times the `i`th element of the `R`-basis of `S`.
More concisely: For a finite-dimensional ring extension of a principal ideal domain as an free `R`-module, any non-zero ideal has a basis whose inclusion map is represented by a square diagonal matrix with Smith coefficients as diagonal entries when expressed in terms of the `R`-basis of the extension ring.
|
Submodule.exists_smith_normal_form_of_le
theorem Submodule.exists_smith_normal_form_of_le :
∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R]
{M : Type u_3} [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Finite ι],
Basis ι R M →
∀ (N O : Submodule R M),
N ≤ O → ∃ n o, ∃ (hno : n ≤ o), ∃ bO bN a, ∀ (i : Fin n), ↑(bN i) = a i • ↑(bO (Fin.castLE hno i))
The theorem `Submodule.exists_smith_normal_form_of_le` states that for any type `ι`, commutative ring `R` which is also a domain and a principal ideal ring, type `M` which is an additive commutative group and an `R`-module, and assuming that `ι` is finite, given a basis of `M` over `R`, for any two submodules `N` and `O` of `M` such that `N` is a subset of `O`, there exist natural numbers `n` and `o` with `n ≤ o`, bases `bO` for `O` and `bN` for `N` and a sequence `a`, such that for every `i` in `Fin n`, the `i`-th element of the basis `bN` is equal to the `i`-th element of `a` scaled by `i`-th element of the basis `bO` under the embedding from `Fin n` to `Fin o` provided by `Fin.castLE hno i`. This essentially says that every submodule `N` of a module `M` which is finite and free over a principal ideal domain `R`, is also free and we can find bases for `M` and `N` such that the inclusion map is a diagonal matrix in Smith normal form.
More concisely: Given a finite, free submodule `N` of a finitely generated free module `M` over a principal ideal domain `R`, there exist natural numbers `n ≤ o`, bases `bO` for `M` and `bN` for `N`, and a diagonal matrix `a` such that `N` is spanned by the scaled elements of `bN` with respect to `bO`.
|
Basis.SmithNormalForm.snf
theorem Basis.SmithNormalForm.snf :
∀ {R : Type u_2} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{N : Submodule R M} {ι : Type u_4} {n : ℕ} (self : Basis.SmithNormalForm N ι n) (i : Fin n),
↑(self.bN i) = self.a i • self.bM (self.f i)
This theorem states that for any commutative ring `R`, any additive commutative group `M` that is also an `R`-module, a submodule `N` of `M`, an index type `ι`, and a natural number `n`, given a `SmithNormalForm` of `N` with regard to `ι` and `n`, for any finite index `i` in `n`, the `i`-th basis vector of `N` (in its Smith Normal Form) can be expressed as the `i`-th elementary divisor times the `i`-th basis vector of `M` under a certain linear map.
More concisely: For any commutative ring `R`, additive commutative `R`-module `M`, submodule `N` of `M`, index type `ι`, and natural number `n`, there exists a linear map `φ : M -> M` such that for any finite index `i` in `n`, the `i`-th basis vector of `N` in its Smith Normal Form is equal to the `i`-th elementary divisor multiplied by the `i`-th basis vector of `M`.
|
Ideal.exists_smith_normal_form
theorem Ideal.exists_smith_normal_form :
∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R]
{S : Type u_4} [inst_3 : CommRing S] [inst_4 : IsDomain S] [inst_5 : Algebra R S] [inst_6 : Finite ι],
Basis ι R S → ∀ (I : Ideal S), I ≠ ⊥ → ∃ b' a ab', ∀ (i : ι), ↑(ab' i) = a i • b' i
This theorem states that for a commutative ring `R`, which is also a domain and a Principal Ideal Ring (PID), and its finite-dimensional ring extension `S` (which also is a domain and a commutative ring) that is free as an `R`-module, any non-zero `S`-ideal `I` is free as an `R`-submodule of `S`. Moreover, we can find a basis for both `S` and `I` such that the inclusion map from `I` to `S` is represented by a square diagonal matrix. The elements of this diagonal matrix are obtained by scaling the basis vectors of `S` with certain coefficients to obtain the corresponding basis vectors for `I`.
In more formal terms, given a basis for `S` over `R`, if `I` is a non-zero `S`-ideal, then there exist bases `b'` for `S` and `a` for `I` and a function `ab'` that for each index `i` of the basis maps it to a coefficient such that the `i`-th basis element of `I` is the `i`-th basis element of `S` scaled by the corresponding coefficient.
More concisely: For a commutative domain and Principal Ideal Ring (PID) `R`, and its finite-dimensional free `R`-module extension `S`, any non-zero `S`-ideal `I` is free as an `R`-submodule, and there exist bases for `S` and `I` such that the inclusion map from `I` to `S` is represented by a diagonal matrix with scaling coefficients.
|
LinearIndependent.restrict_scalars_algebras
theorem LinearIndependent.restrict_scalars_algebras :
∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {ι : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring S]
[inst_2 : AddCommMonoid M] [inst_3 : Algebra R S] [inst_4 : Module R M] [inst_5 : Module S M]
[inst_6 : IsScalarTower R S M],
Function.Injective ⇑(algebraMap R S) → ∀ {v : ι → M}, LinearIndependent S v → LinearIndependent R v
The theorem `LinearIndependent.restrict_scalars_algebras` states that for any commutative semiring `R`, semiring `S`, `AddCommMonoid` M, and an arbitrary type `ι`, given `R` is a subring of `S` (Algebra structure between R and S), `M` is a module over both `R` and `S`, and `R`, `S` and `M` form a scalar tower, if the function defined by the algebra map from `R` to `S` is injective, then any set of vectors `v : ι → M` that is linearly independent over `S` is also linearly independent over `R`.
In other words, if we have a set of vectors that are linearly independent in a module `M` over a semiring `S`, and `S` includes a subring `R` such that the algebra map from `R` to `S` is injective, then this set of vectors remains linearly independent when considered over the subring `R`.
More concisely: If `R` is a subring of commutative semiring `S`, `M` is a module over both `R` and `S`, `R`, `S`, and `M` form a scalar tower, and the algebra map from `R` to `S` is injective, then linear independence of a set of vectors over `S` implies linear independence over `R`.
|