Basis.reindex_apply
theorem Basis.reindex_apply :
∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] (b : Basis ι R M) (e : ι ≃ ι') (i' : ι'), (b.reindex e) i' = b (e.symm i')
The theorem `Basis.reindex_apply` states that for any semiring `R`, any additive commutative monoid `M` which is also a module over `R`, any basis `b` of `M` indexed by type `ι`, any bijection `e` from `ι` to another type `ι'`, and any element `i'` of `ι'`, the result of indexing the basis reindexed by `e` at `i'` is equal to the result of indexing the original basis at the inverse image of `i'` under `e`. In other words, reindexing a basis by a bijection and then applying the new index is the same as applying the inverse of the bijection to the new index and then indexing the original basis.
More concisely: For any semiring `R`, additive commutative `R`-module `M` with basis `b` indexed by `ι`, bijection `e` from `ι` to `ι'`, and `i'` in `ι'`, the reindexed basis element `b.e i'` is equal to the basis element `b.ι⁁⁻¹(eⁱ⁻¹i')`.
|
union_support_maximal_linearIndependent_eq_range_basis
theorem union_support_maximal_linearIndependent_eq_range_basis :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Nontrivial R] [inst_3 : Module R M]
{ι : Type w} (b : Basis ι R M) {κ : Type w'} (v : κ → M) (i : LinearIndependent R v),
i.Maximal → ⋃ k, ↑(b.repr (v k)).support = Set.univ
The theorem `union_support_maximal_linearIndependent_eq_range_basis` states that for any ring `R` and any module `M` over `R`, if `b` is a basis for `M`, and `s` is a maximal set of linearly independent elements, then the union of the supports of each element `x` in `s` (when expressed in terms of the basis `b`) covers all elements of the basis `b`. In other words, every basis element is involved in the representation of some member of the maximal linearly independent set in the basis `b`.
More concisely: Given a ring `R`, an `R`-module `M` with basis `b`, and a maximal linearly independent set `s` in `M`, the union of the supports of elements in `s` in terms of `b` spans `M`, i.e., every basis element is represented in the span of `s` using `b`.
|
Basis.ext_elem_iff
theorem Basis.ext_elem_iff :
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(b : Basis ι R M) {x y : M}, x = y ↔ ∀ (i : ι), (b.repr x) i = (b.repr y) i
This theorem states that for any given basis `b` in a module `M` over a semiring `R` and for any two elements `x` and `y` in `M`, `x` is equal to `y` if and only if their coordinates with respect to the basis `b` are equal for all indices `i` in the indexing set `ι`. In other words, two elements in a module are identical if their representations with respect to a particular basis are identical.
More concisely: For any module M over a semiring R with basis b, two elements x and y are equal if and only if their coordinate vectors with respect to b are equal component-wise.
|
Basis.total_repr
theorem Basis.total_repr :
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(b : Basis ι R M) (x : M), (Finsupp.total ι M R ⇑b) (b.repr x) = x
The theorem `Basis.total_repr` states that for any `ι` which is a type, `R` which is a type of semiring, and `M` which is a type of additively commutative monoid that is also a module over `R`, given any basis `b` of `M` over `R`, and any element `x` of `M`, the total function applied to the basis representation of `x` equals `x` itself. In mathematical terms, it states that given a basis of a vector space, any vector in the space can be represented as a linear combination of basis vectors, and applying the total function recovers the original vector.
More concisely: Given a semiring `R`, a type `M` of additively commutative `R`-module, a basis `b` of `M`, and any element `x` in `M`, the application of the total function to the basis representation of `x` equals `x`.
|
Basis.eq_of_apply_eq
theorem Basis.eq_of_apply_eq :
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{b₁ b₂ : Basis ι R M}, (∀ (i : ι), b₁ i = b₂ i) → b₁ = b₂
This theorem states that for any two bases `b₁` and `b₂` of a module `M` over a semiring `R`, indexed over a common index set `ι`, if every basis vector of `b₁` is equal to the corresponding basis vector of `b₂`, then the bases `b₁` and `b₂` are equal.
More concisely: If two bases `b₁` and `b₂` of a module `M` over a semiring `R`, indexed over a common index set `ι`, have the same basis vectors, then `b₁` and `b₂` are equal.
|
Basis.index_nonempty
theorem Basis.index_nonempty :
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
Basis ι R M → ∀ [inst : Nontrivial M], Nonempty ι
This theorem states that for a given index set `ι`, a ring `R`, and a module `M` over `R`, if `M` has a basis with respect to `ι` and `R`, and `M` is nontrivial (i.e., it contains at least two distinct elements), then `ι` is nonempty. In other words, a nontrivial module always has a nonempty set of basis indices.
More concisely: A nontrivial module over a ring with a basis has a nonempty index set.
|
Basis.mem_submodule_iff'
theorem Basis.mem_submodule_iff' :
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
[inst_3 : Fintype ι] {P : Submodule R M} (b : Basis ι R ↥P) {x : M},
x ∈ P ↔ ∃ c, x = Finset.univ.sum fun i => c i • ↑(b i)
This theorem states that for any given index type `ι`, ring `R`, module `M` over `R`, and a submodule `P` of `M`, if the submodule `P` has a finite basis `b` and `x` is an element of the module `M`, then `x` is an element of `P` if and only if there exists a function `c` such that `x` is the sum of the scalar products of `c(i)` and the basis vector `b(i)`, where the sum is taken over all elements `i` in the universal set of `ι`. Here, `•` denotes the scalar multiplication in the module, and `↑(b i)` is the embedding of the basis vector `b(i)` from the submodule `P` to the module `M`.
More concisely: For any index type `ι`, ring `R`, module `M` over `R`, and finite basis `b` of a submodule `P` of `M`, an element `x` in `M` belongs to `P` if and only if there exists a function `c` such that `x = ∑ (i: ι) (c i • b i)`.
|
infinite_basis_le_maximal_linearIndependent'
theorem infinite_basis_le_maximal_linearIndependent' :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Nontrivial R] [inst_3 : Module R M]
{ι : Type w},
Basis ι R M →
∀ [inst_4 : Infinite ι] {κ : Type w'} (v : κ → M) (i : LinearIndependent R v),
i.Maximal → Cardinal.lift.{w', w} (Cardinal.mk ι) ≤ Cardinal.lift.{w, w'} (Cardinal.mk κ)
This theorem states that for any ring `R` and module `M` over `R`, if `b` is a basis of `M` that is infinite, and `s` is a set that is linearly independent and maximal (meaning it cannot be extended by adding any element that is not already in it), then the cardinality of `b` is less than or equal to the cardinality of `s`. This is stated in the context of the type universe lifting operation on cardinals, which allows us to compare the cardinalities of sets even when the types of their elements are not in the same universe. The cardinality of a set is represented in Lean by the `Cardinal.mk` function, and the universe lift operation is represented by `Cardinal.lift`. Linear independence is represented by `LinearIndependent R v`, where `R` is a ring and `v` is a function from some index set to the module `M`. The `Basis ι R M` term represents the fact that `ι` indexes a basis of the module `M` over the ring `R`.
More concisely: If `R` is a ring, `M` is an `R`-module, `b` is an infinite basis of `M`, and `s` is a maximal linearly independent subset of `b`, then the cardinality of `b` is less than or equal to the cardinality of `s`.
|
Basis.groupSMul_span_eq_top
theorem Basis.groupSMul_span_eq_top :
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
{G : Type u_10} [inst_3 : Group G] [inst_4 : DistribMulAction G R] [inst_5 : DistribMulAction G M]
[inst_6 : IsScalarTower G R M] {v : ι → M},
Submodule.span R (Set.range v) = ⊤ → ∀ {w : ι → G}, Submodule.span R (Set.range (w • v)) = ⊤
The theorem `Basis.groupSMul_span_eq_top` states that for any types `ι`, `R`, `M`, and `G` where `R` is a ring, `M` is an additive commutative group and is a module over `R`, `G` is a group which acts distributively on `R` and `M`, and where the action of `G` on `R` is extendable to `M`, given a function `v : ι → M` such that the span of the range of `v` covers the whole space (`⊤`), then for any function `w : ι → G`, the span of the range of the scalar multiplication `w • v` also covers the whole space (`⊤`). In other words, if the vectors obtained by the function `v` span the whole space, then the vectors obtained by scalarly multiplying the vectors obtained from `v` by the elements from function `w` also span the whole space.
More concisely: If `v : ι → M` spans `M`, then for any `w : ι → G` where `G` acts linearly on `M` over a ring `R`, the scalars `{w x | x ∈ ι}` together with the span of `v` span the whole of `M`.
|
Basis.repr_apply_eq
theorem Basis.repr_apply_eq :
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(b : Basis ι R M) (f : M → ι → R),
(∀ (x y : M), f (x + y) = f x + f y) →
(∀ (c : R) (x : M), f (c • x) = c • f x) →
(∀ (i : ι), f (b i) = ⇑fun₀ | i => 1) → ∀ (x : M) (i : ι), (b.repr x) i = f x i
The theorem `Basis.repr_apply_eq` is an unbundled version of `repr_eq_iff`. It states that for any types `ι`, `R`, and `M`, given a semiring `R`, an additive commutative monoid `M`, and a `R`-module structure on `M`, along with a basis `b` of `M` over `R` indexed by `ι` and a function `f` mapping from `M` to `ι → R`, if `f` is linear (preserves addition and scalar multiplication) and `f` applied to basis vector `b i` gives '1' at index 'i' for all `i`, then the coefficients of the representation of any vector `x` in basis `b` (given by `b.repr x`) equal the values of `f x i` for all indices `i` in `ι`.
More concisely: Given a semiring `R`, an additive commutative monoid `M` with an `R`-module structure, a basis `b` of `M` over `R` indexed by `ι`, and a linear function `f : M → ι → R` such that `f b i = 1` for all `i ∈ ι`, the coefficients of the representation of any vector `x ∈ M` in basis `b` are equal to `f x i` for all `i ∈ ι`.
|
Basis.mk_coord_apply_eq
theorem Basis.mk_coord_apply_eq :
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} {v : ι → M} [inst : Ring R] [inst_1 : AddCommGroup M]
[inst_2 : Module R M] {hli : LinearIndependent R v} {hsp : ⊤ ≤ Submodule.span R (Set.range v)} (i : ι),
((Basis.mk hli hsp).coord i) (v i) = 1
The theorem `Basis.mk_coord_apply_eq` states that for any given basis of a module, the `i`th element of the dual basis evalutes to 1 when applied to the `i`th element of the basis. Here, a basis is defined as a linearly independent family of vectors that span the whole module. This theorem is a fundamental property in linear algebra, reflecting the intuitive idea that a basis vector has a coordinate of 1 on its corresponding dual basis vector and zero on other dual vectors.
More concisely: For any basis of a module, the i-th element of the dual basis evaluates to 1 when applied to the i-th basis element.
|
Basis.mem_span_iff_repr_mem
theorem Basis.mem_span_iff_repr_mem :
∀ {ι : Type u_1} (R : Type u_3) {M : Type u_6} {S : Type u_10} [inst : CommRing R] [inst_1 : Ring S]
[inst_2 : Nontrivial S] [inst_3 : AddCommGroup M] [inst_4 : Algebra R S] [inst_5 : Module S M]
[inst_6 : Module R M] [inst_7 : IsScalarTower R S M] [inst_8 : 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)
This theorem states that for a given basis `b` of a module `M` over a ring `S`, any element `m` in `M` lies in the submodule spanned by `b` over another ring `R` if and only if all the coordinates of `m` with respect to the basis `b` are in the image of the embedding from `R` to `S`. This condition is a generalization of `Basis.mem_span`, which handles the case where `R = S`. This is subject to the condition that `S` is a non-trivial ring, `M` is an additive commutative group, `S` is a module over `R`, and `R` acts on `M` through `S`.
More concisely: For a module M over a non-trivial ring S, an additive commutative group, and an R-module structure on M through S, an element m in M lies in the submodule of M spanned by basis b over ring R if and only if the coordinates of m with respect to basis b are in the image of the embedding from R into S.
|
Basis.mk_coord_apply_ne
theorem Basis.mk_coord_apply_ne :
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} {v : ι → M} [inst : Ring R] [inst_1 : AddCommGroup M]
[inst_2 : Module R M] {hli : LinearIndependent R v} {hsp : ⊤ ≤ Submodule.span R (Set.range v)} {i j : ι},
j ≠ i → ((Basis.mk hli hsp).coord i) (v j) = 0
This theorem states that given a basis for a module over a ring, the `i`th element of the dual basis evaluates to zero when applied to the `j`th element of the basis if `j` and `i` are not equal. In other words, if we have a basis of a module, and we consider the dual basis (which is a basis of the dual module), then each element of this dual basis will annihilate all elements of the original basis except for the corresponding one. This is a fundamental property in linear algebra, underpinning the orthogonality of a basis and its dual.
More concisely: Given a basis for a module and its dual basis, the i-th dual basis element evaluates to zero when applied to the j-th basis element for i ≠ j.
|
Basis.injective
theorem Basis.injective :
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(b : Basis ι R M) [inst_3 : Nontrivial R], Function.Injective ⇑b
The theorem `Basis.injective` states that for any Type `ι`, a semiring `R`, and an additive commutative monoid `M` that is also an `R`-module, if `b` is a basis of the `R`-module `M`, and `R` is nontrivial (meaning it contains at least two distinct elements), then the function defined by applying `b` is injective. In other words, if `b` is a basis of `M` and we have two elements from type `ι` such that applying `b` to both of them gives the same result, then these two elements must be equal. This is a key property of bases in module theory, reflecting that different elements of the basis are mapped to linearly independent vectors in the module.
More concisely: If `β` is a basis of the `R`-module `M` over a nontrivial semiring `R`, then the function `x ↦ ∑ (b : β) (x b)` is injective.
|
Basis.equivFun_ofEquivFun
theorem Basis.equivFun_ofEquivFun :
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
[inst_3 : Finite ι] (e : M ≃ₗ[R] ι → R), (Basis.ofEquivFun e).equivFun = e
This theorem, `Basis.equivFun_ofEquivFun`, states that for any semiring `R`, additive commutative monoid `M`, module structure on `M` over `R`, and finite type `ι`, given a linear equivalence `e` between `M` and the function type `ι → R`, the function `Basis.equivFun` applied to the basis of `M` over `R` as defined by the `Basis.ofEquivFun` function with `e` as its argument will equal to `e`. In simpler terms, it implies for a given linear equivalence between a module and a finite set of functions, the function to map a basis to this equivalence will recover the original equivalence.
More concisely: For any semiring `R`, additive commutative monoid `M` with an `R`-module structure, finite type `ι`, and a linear equivalence `e` between `M` and `ι → R`, the basis transformation `Basis.equivFun (Basis.ofEquivFun e)` equals `e`.
|
basis_finite_of_finite_spans
theorem basis_finite_of_finite_spans :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Nontrivial R] [inst_3 : Module R M]
(w : Set M), w.Finite → Submodule.span R w = ⊤ → ∀ {ι : Type w}, Basis ι R M → Finite ι
The theorem `basis_finite_of_finite_spans` states that over any nontrivial ring `R`, if there exists a finite spanning set `w` of a module `M` over that ring, such that the span of `w` equals the entire module (denoted by ⊤), then any basis of the module `M` is necessarily finite. In other words, in the presence of a finite spanning set that spans the entire module, the property of having a finite basis is guaranteed for the module over the nontrivial ring.
More concisely: Over a nontrivial ring, if a module has a finite spanning set that spans the entire module, then it has a finite basis.
|
Basis.coe_reindex
theorem Basis.coe_reindex :
∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] (b : Basis ι R M) (e : ι ≃ ι'), ⇑(b.reindex e) = ⇑b ∘ ⇑e.symm
The theorem `Basis.coe_reindex` states that for any semiring `R`, additively commutative monoid `M`, and for any `R`-module structure on `M`, given a basis `b` indexed by type `ι` for the module and a bijective map `e` from `ι` to another type `ι'`, the function corresponding to the reindexing of basis `b` with `e` (`Basis.reindex b e`) is equivalent to the composition of the function corresponding to basis `b` and the inverse of the function corresponding to `e`. Essentially, reindexing a basis and then mapping an index is the same as first mapping the index with the inverse of the reindexing map and then applying the original basis map.
More concisely: For any semiring `R`, additively commutative monoid `M` with an `R`-module structure, basis `b` indexed by `ι`, and bijective map `e` from `ι` to `ι'`, `Basis.reindex b e` equals the composition of `b` with the inverse of `e`.
|
Basis.ext_elem
theorem Basis.ext_elem :
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(b : Basis ι R M) {x y : M}, (∀ (i : ι), (b.repr x) i = (b.repr y) i) → x = y
The theorem `Basis.ext_elem` states that for any indexing type `ι`, ring `R`, and module `M` over `R` with a basis `b`, if two elements `x` and `y` of `M` have the same coordinates with respect to basis `b`, then `x` and `y` are equal. This is an "if" direction of the equivalence asserted by `Basis.ext_elem_iff`, hence referred to as the "reverse" direction. This theorem is crucial in linear algebra as it helps to identify elements of a module or vector space uniquely by their coordinates.
More concisely: If two elements of a module with a basis have the same coordinates with respect to that basis, then they are equal.
|
Module.card_fintype
theorem Module.card_fintype :
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
[inst_3 : Fintype ι],
Basis ι R M → ∀ [inst : Fintype R] [inst_4 : Fintype M], Fintype.card M = Fintype.card R ^ Fintype.card ι
The theorem `Module.card_fintype` states that for any types `ι`, `R`, and `M`, given a semiring structure on `R`, an additive commutative monoid structure on `M`, and a module structure on `M` over `R`, and assuming that `ι`, `R`, and `M` are finite types (i.e., they have finitely many distinct values), if `ι` serves as a basis for the module `M` over the ring `R`, then the number of elements in `M` (denoted `Fintype.card M`) is equal to the number of elements in `R` (denoted `Fintype.card R`) raised to the power of the number of elements in `ι` (denoted `Fintype.card ι`). In mathematical notation, this would be written as |M| = |R|^|ι|.
More concisely: If `ι` is a finite basis for a module `M` over a finite ring `R`, then |M| = |R|^|ι|.
|
Basis.ext'
theorem Basis.ext' :
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(b : Basis ι R M) {R₁ : Type u_10} [inst_3 : Semiring R₁] {σ : R →+* R₁} {σ' : R₁ →+* R}
[inst_4 : RingHomInvPair σ σ'] [inst_5 : RingHomInvPair σ' σ] {M₁ : Type u_11} [inst_6 : AddCommMonoid M₁]
[inst_7 : Module R₁ M₁] {f₁ f₂ : M ≃ₛₗ[σ] M₁}, (∀ (i : ι), f₁ (b i) = f₂ (b i)) → f₁ = f₂
This theorem states that, given two linear equivalences `f₁` and `f₂` between two modules `M` and `M₁` over different semirings `R` and `R₁` respectively, if they both map each basis vector of `M` (as defined by the basis `b`) to the same vector in `M₁`, then `f₁` and `f₂` are equal. This holds under the conditions that `R` and `R₁` are related by ring homomorphisms that form an inverse pair.
More concisely: Given linear equivalences `f₁ : M → M₁` and `f₂ : M → M₁` between modules `M` over semirings `R` and `M₁` over `R₁`, and ring homomorphisms `h : R → R₁` and `g : R₁ → R` with `h ∘ g = id R` and `f₁ (b) = f₂ (b)` for all basis vectors `b` of `M`, then `f₁ = f₂`.
|
Basis.mk_coord_apply
theorem Basis.mk_coord_apply :
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} {v : ι → M} [inst : Ring R] [inst_1 : AddCommGroup M]
[inst_2 : Module R M] {hli : LinearIndependent R v} {hsp : ⊤ ≤ Submodule.span R (Set.range v)}
[inst_3 : DecidableEq ι] {i j : ι}, ((Basis.mk hli hsp).coord i) (v j) = if j = i then 1 else 0
The theorem `Basis.mk_coord_apply` states that given a basis formed by a linearly independent family of vectors that spans the whole module, the `i`th element of the dual basis evaluates to the Kronecker delta on the `j`th element of the basis. In other words, when this `i`th element of the dual basis is applied to the `j`th element of the original basis, it results in the value 1 if `i` and `j` are the same and 0 otherwise. This is essentially a formal characterization of the properties of a basis in a module over a ring.
More concisely: Given a basis of a module over a ring and its dual basis, the i-th element of the dual basis evaluates to the Kronecker delta when applied to the j-th element of the original basis.
|
Basis.span_eq
theorem Basis.span_eq :
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(b : Basis ι R M), Submodule.span R (Set.range ⇑b) = ⊤
This theorem, `Basis.span_eq`, states that for any given basis `b` of a module `M` over a semiring `R`, the span of the range of the basis (i.e., the set of all elements obtained by applying the basis function to all elements in its domain) is the entire module `M`. In other words, any element of the module `M` can be expressed as a linear combination of elements from the basis `b`. This is a key property of a basis in the context of module theory.
More concisely: For any module M over a semiring R and basis b of M, the span of the basis equals M, i.e., every element in M can be expressed as a linear combination of basis elements.
|
Basis.repr_injective
theorem Basis.repr_injective :
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
Function.Injective Basis.repr
The theorem `Basis.repr_injective` states that for any semiring `R`, any additively commutative monoid `M`, and any basis `ι` for a module `M` over the semiring `R`, the function `Basis.repr` is injective. This means that if `Basis.repr` yields the same result for two different vectors, those vectors are in fact the same. In other words, two different vectors cannot have the same coordinates with respect to the basis `ι`.
More concisely: For any semiring R, additively commutative monoid M with basis ι, the representation function Basis.repr from M to R^ι is injective.
|
Basis.repr_total
theorem Basis.repr_total :
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(b : Basis ι R M) (v : ι →₀ R), b.repr ((Finsupp.total ι M R ⇑b) v) = v
The theorem `Basis.repr_total` states that for any semiring `R`, additive commutative monoid `M`, and a basis `b` of module `M` over `R`, and any function `v` mapping from a type `ι` to `R`, the representation of the linear combination of the basis elements (i.e., `b.repr`) evaluated at the total function (i.e., `(Finsupp.total ι M R ⇑b) v`) is equal to the function `v` itself. In other words, this theorem relates the representation of a vector in terms of the basis to the function describing the coefficients of the linear combination in that basis. This can be interpreted as the property that the coefficients you get when representing a vector in terms of a basis are exactly the ones you used to construct the vector as a linear combination of the basis elements.
More concisely: For any semiring `R`, additive commutative monoid `M`, basis `b` of `M` over `R`, and function `v : ι -> R`, we have `b.repr (Finsupp.total ι M R v) = v`.
|
Basis.constr_basis
theorem Basis.constr_basis :
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (b : Basis ι R M) (S : Type u_10)
[inst_5 : Semiring S] [inst_6 : Module S M'] [inst_7 : SMulCommClass R S M'] (f : ι → M') (i : ι),
((b.constr S) f) (b i) = f i
This theorem states that for any basis `b` of a module `M` over a semiring `R`, given a semiring `S` and an `S`-module `M'` where `S` commutes with `R` on `M'`, and a function `f` that maps from the index set `ι` of the basis to `M'`, applying the basis construction function `Basis.constr` to `f` and then applying this to a basis element `b i` will simply return `f i`. In other words, the basis construction function applied to `f` preserves the mapping of `f` on the basis elements.
More concisely: For any semiring-homomorphism f : ι -> M' between the index set ι of a module basis b in an R-module M and an S-module M', where S commutes with R on M', the application of Basis.constr(f) to the basis element bi is equal to f(bi) in M'.
|
Basis.range_reindex
theorem Basis.range_reindex :
∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] (b : Basis ι R M) (e : ι ≃ ι'), Set.range ⇑(b.reindex e) = Set.range ⇑b
The theorem `Basis.range_reindex` states that for any given types `ι`, `ι'`, `R`, and `M`, assuming `R` is a semiring and `M` is an additive commutative monoid and also a module over `R`, and given a basis `b` of the module `M` over `R` indexed by `ι`, and an equivalence `e` between `ι` and `ι'`, the range of the reindexed basis (obtained by applying `e` to the indices of `b`) is equal to the range of the original basis `b`. This means that reindexing the basis does not change the set of vectors it spans (i.e., its range).
More concisely: Given types `ι`, `ι'`, an equivalence `e` between `ι` and `ι'`, a semiring `R`, an additive commutative monoid and `R`-module `M`, and a basis `b` of `M` indexed by `ι`, the ranges of `b` and its reindexed version obtained by applying `e` are equal.
|
Basis.maximal
theorem Basis.maximal :
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : Nontrivial R] (b : Basis ι R M), ⋯.Maximal
This theorem asserts that any basis in a given context is a maximal linearly independent set. Specifically, for any type `ι` (which forms the indexing set), a ring `R`, and an additive commutative group `M` that is a module over `R`, and assuming that `R` is nontrivial (i.e., contains at least two distinct elements), if `b` is a basis, then `b` is a maximal linearly independent set in the module `M` over the ring `R`.
More concisely: Given a nontrivial ring `R` and an additive commutative `R`-module `M` with basis `b`, `b` is a maximal linearly independent set in `M`.
|
infinite_basis_le_maximal_linearIndependent
theorem infinite_basis_le_maximal_linearIndependent :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Nontrivial R] [inst_3 : Module R M]
{ι : Type w},
Basis ι R M →
∀ [inst_4 : Infinite ι] {κ : Type w} (v : κ → M) (i : LinearIndependent R v),
i.Maximal → Cardinal.mk ι ≤ Cardinal.mk κ
This theorem states that for any ring `R` and any module `M` over `R`, if `b` is an infinite basis for `M` and `s` is a maximal linearly independent set, then the cardinality of the basis `b` is less than or equal to the cardinality of the set `s`. In other words, the size of an infinite basis is bounded by the size of any maximal linearly independent set in the module.
More concisely: For any ring `R` and module `M` over `R`, if `b` is an infinite basis for `M` and `s` is a maximal linearly independent set in `M`, then the cardinality of `b` is bounded above by that of `s`.
|
Basis.equivFun_apply
theorem Basis.equivFun_apply :
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
[inst_3 : Finite ι] (b : Basis ι R M) (u : M), b.equivFun u = ⇑(b.repr u)
The theorem `Basis.equivFun_apply` states that for any type `ι`, any semiring `R`, any additively commutative monoid `M`, and any `M` module over `R` with a finite basis `b` and any element `u` of `M`, the application of the function `Basis.equivFun` to `u` is equal to the application of the coordinate representation of `u` with respect to the basis `b`. In other words, the function `Basis.equivFun` gives the same result as directly computing the coordinates of `u` in the basis `b`.
More concisely: For any type `ι`, semiring `R`, additively commutative monoid `M` with a finite basis `b`, and `M` module `u` over `R`, `Basis.equivFun u = coordRep_basis b u`, where `coordRep_basis` denotes the coordinate representation function with respect to `b`.
|
Basis.ext
theorem Basis.ext :
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(b : Basis ι R M) {R₁ : Type u_10} [inst_3 : Semiring R₁] {σ : R →+* R₁} {M₁ : Type u_11}
[inst_4 : AddCommMonoid M₁] [inst_5 : Module R₁ M₁] {f₁ f₂ : M →ₛₗ[σ] M₁},
(∀ (i : ι), f₁ (b i) = f₂ (b i)) → f₁ = f₂
This theorem states that given two linear maps `f₁` and `f₂` from a module `M` over a ring `R` to another module `M₁` over another ring `R₁`, if these two maps coincide on the basis vectors of `M`, then they are equal. This is under the context that `R` and `R₁` are semirings, `M` and `M₁` are additive commutative monoids with a module structure, and there's a ring homomorphism from `R` to `R₁`. The basis of module `M` is indexed by an arbitrary type `ι`.
More concisely: If `f₁` and `f₂` are linear maps from a module `M` over a semiring `R` to another module `M₁` over a semiring `R₁`, with a ring homomorphism from `R` to `R₁`, such that `f₁(eι) = f₂(eι)` for all basis vectors `eι` in `M`, then `f₁ = f₂`.
|
Basis.equiv_apply
theorem Basis.equiv_apply :
∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} {M' : Type u_7} [inst : Semiring R]
[inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M']
(b : Basis ι R M) (i : ι) (b' : Basis ι' R M') (e : ι ≃ ι'), (b.equiv b' e) (b i) = b' (e i)
This theorem states that for any semiring `R`, additively commutative monoids `M` and `M'`, and types `ι` and `ι'`, given a basis `b` for `M` over `R` indexed by `ι`, another basis `b'` for `M'` over `R` indexed by `ι'`, and a bijection `e` between `ι` and `ι'`, applying the equivalence between the two bases to `b i` results in `b'` at the index `e i`. In other words, it shows how elements from one basis get mapped to elements in the other basis under the given bijection between their indices.
More concisely: Given semirings `R`, additively commutative monoids `M` and `M'`, bases `b: M → ι → R` and `b': M' → ι' → R` for `M` and `M'` over `R`, and a bijection `e: ι ≃ ι'`, we have `b' (e x) = b x` for all `x ∈ ι`.
|
Basis.apply_eq_iff
theorem Basis.apply_eq_iff :
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{b : Basis ι R M} {x : M} {i : ι}, b i = x ↔ b.repr x = fun₀ | i => 1
The theorem `Basis.apply_eq_iff` states that for any types `ι`, `R`, and `M`, given a semiring structure for `R`, an additive commutative monoid structure for `M`, and a module structure for `R` and `M`, for any basis `b` of type `Basis ι R M`, any element `x` of `M`, and any index `i` of `ι`, `b i` equals `x` if and only if the representation of `x` with respect to the basis `b` is a function that gives `1` when applied to `i` and gives `0` when applied to all other indices. In other words, `x` is the `i`-th basis vector if and only if its representation in terms of the basis is a function that is `1` at `i` and `0` everywhere else.
More concisely: For any semiring `R`, additive commutative monoid `M`, and basis `b` of type `Basis ι R M`, an element `x` of `M` equals `b i` if and only if the representation of `x` with respect to `b` is the function that maps `i` to `1` and all other indices to `0`.
|
Basis.equivFun_symm_apply
theorem Basis.equivFun_symm_apply :
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
[inst_3 : Fintype ι] (b : Basis ι R M) (x : ι → R), b.equivFun.symm x = Finset.univ.sum fun i => x i • b i
The theorem `Basis.equivFun_symm_apply` states that for any set `ι`, semiring `R`, and additively commutative monoid `M` with a `R`-module structure, given a basis `v` indexed by `ι`, the inverse of the canonical linear equivalence between the function space `ι → R` and `M` maps a function `x : ι → R` to the linear combination of the basis vectors, where each vector `v i` is scaled by `x i`. This linear combination is represented as the sum over all elements `i` in the universal set of `ι`, of the product of `x i` and `v i`.
In mathematical notation, this might be written as:
\( (Basis.equivFun^{-1} b)(x) = \sum_{i \in univ} x(i) \cdot v(i) \).
More concisely: The theorem `Basis.equivFun_symm_apply` asserts that the inverse of the linear equivalence between a basis and the function space with respect to a set, semiring, additively commutative monoid, and `R`-module structure, maps a function `x` to the sum over its index set of the product of `x(i)` and the corresponding basis vector `v(i)`.
|
Basis.repr_symm_apply
theorem Basis.repr_symm_apply :
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(b : Basis ι R M) (v : ι →₀ R), b.repr.symm v = (Finsupp.total ι M R ⇑b) v
The theorem `Basis.repr_symm_apply` states that for any index type `ι`, ring `R`, and module `M` over `R` (with `R` being a semiring and `M` being an additive commutative monoid and also a module over `R`), and for any basis `b` of `M` and any function `v` from `ι` to `R`, the application of the inverse of the linear equivalence represented by `b` to `v` is equal to the total function of `v` under the map `b`. In other words, it says that applying the inverse of basis representation to a function `v` is equivalent to evaluating the linear combination of elements in the basis `b` with coefficients given by `v`.
More concisely: For any index type `ι`, ring `R`, additive commutative monoid `M` over `R`, basis `b` of `M`, and function `v` from `ι` to `R`, applying the inverse of the linear map represented by `b` to `v` equals the total function of `v` under `b`.
|
Basis.mem_center_iff
theorem Basis.mem_center_iff :
∀ {ι : Type u_1} {R : Type u_3} {A : Type u_10} [inst : Semiring R] [inst_1 : NonUnitalNonAssocSemiring A]
[inst_2 : Module R A] [inst_3 : SMulCommClass R A A] [inst_4 : SMulCommClass R R A] [inst_5 : 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 * z * b j = b i * (z * b j) ∧ b i * b j * z = b i * (b j * z)
The theorem `Basis.mem_center_iff` states that for a given non-unital-non-associative algebra over a semiring, an element is in the center of the algebra if and only if it commutes with all basis elements. More specifically, an element `z` of the algebra is in the center if, for every basis vector `i`, `z` commutes with `i` and for every pair of basis vectors `i` and `j`, the triple products `z*(b_i*b_j)`, `b_i*z*b_j`, and `b_i*b_j*z` can be rearranged without changing their value.
More concisely: An element is in the center of a non-unital-non-associative algebra over a semiring if and only if it commutes with all basis elements and their products satisfy the associativity condition.
|
Basis.linearIndependent
theorem Basis.linearIndependent :
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(b : Basis ι R M), LinearIndependent R ⇑b
The theorem `Basis.linearIndependent` asserts that for any semiring `R`, any additively commutative monoid `M`, and any module `R M`, if `b` is a basis of the module, then the basis `b` is linearly independent over the semiring `R`. In other words, no vector in the basis can be represented as a linear combination of the other vectors in the basis set.
More concisely: If `b` is a basis of the `R-module` `M`, then `b` is linearly independent over the semiring `R`.
|
Basis.mem_submodule_iff
theorem Basis.mem_submodule_iff :
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{P : Submodule R M} (b : Basis ι R ↥P) {x : M}, x ∈ P ↔ ∃ c, x = c.sum fun i x => x • ↑(b i)
This theorem states that for a given submodule `P` of a module `M` over a semiring `R`, if `P` has a basis `b`, then an element `x` belongs to `P` if and only if `x` can be expressed as a linear combination of the basis vectors of `P`. Here, the linear combination is represented as the sum of scalar multiplications of basis vectors, where the scalars are elements of the semiring `R` and the sum is indexed by `ι`, the type of the index set of the basis.
More concisely: Given a submodule `P` of a module `M` over a semiring `R` with basis `b`, an element `x` belongs to `P` if and only if there exist scalars `r` in `R` indexed by `ι`, such that `x = ∑ r(ι) · b(ι)`, where `∑` denotes summation over `ι`.
|
Basis.coe_mk
theorem Basis.coe_mk :
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} {v : ι → M} [inst : Ring R] [inst_1 : AddCommGroup M]
[inst_2 : Module R M] (hli : LinearIndependent R v) (hsp : ⊤ ≤ Submodule.span R (Set.range v)),
⇑(Basis.mk hli hsp) = v
The theorem `Basis.coe_mk` states that for any type `ι`, ring `R`, and additively commutative group `M`, if we have a function `v` from `ι` to `M` such that `v` is a linearly independent family of vectors over `R` and the span of the range of `v` is the entire module `M`, then the function returned by the constructor `Basis.mk` for these inputs is exactly the function `v`. This essentially means that `v` is a basis for the module `M`.
More concisely: If `v : ι → M` is a linearly independent family of vectors over a ring `R` whose span equals `M`, then `Basis.mk ι R M v` is equal to `v`.
|
Basis.eq_ofRepr_eq_repr
theorem Basis.eq_ofRepr_eq_repr :
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{b₁ b₂ : Basis ι R M}, (∀ (x : M) (i : ι), (b₁.repr x) i = (b₂.repr x) i) → b₁ = b₂
The theorem `Basis.eq_ofRepr_eq_repr` states that for any two bases `b₁` and `b₂` of a module `M` over a semiring `R` indexed by the type `ι`, if for every element `x` in `M` and every index `i` in `ι`, the `i`-th coordinate of `x` with respect to `b₁` is equal to the `i`-th coordinate of `x` with respect to `b₂`, then `b₁` and `b₂` are the same basis. Here, `repr` is the function that returns the coordinates of `x` with respect to a basis.
More concisely: If for all `x` in a module `M` over a semiring `R` indexed by `ι`, and for all `i` in `ι`, the `i`-th coordinates of `x` with respect to bases `b₁` and `b₂` are equal, then `b₁` and `b₂` are the same basis of `M`.
|
Basis.repr_self
theorem Basis.repr_self :
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(b : Basis ι R M) (i : ι), b.repr (b i) = fun₀ | i => 1
The theorem `Basis.repr_self` states that for any index set `ι`, ring `R`, module `M` over `R`, and basis `b` of the module `M` indexed by `ι`, the representation of the basis element `b i` with respect to the basis `b` is the function that maps `i` to `1` and all other indices to `0`. In other words, each basis element is represented as having a coefficient of `1` at its own index and `0` at every other index. This is a formal encoding of one of the fundamental properties of a basis in linear algebra.
More concisely: Given a module `M` over a ring `R` with basis `b` indexed by `ι`, the representation function of `b i` with respect to `b` is the function that maps `i` to `1` and all other indices to `0`.
|
Basis.mk_apply
theorem Basis.mk_apply :
∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} {v : ι → M} [inst : Ring R] [inst_1 : AddCommGroup M]
[inst_2 : Module R M] (hli : LinearIndependent R v) (hsp : ⊤ ≤ Submodule.span R (Set.range v)) (i : ι),
(Basis.mk hli hsp) i = v i
The theorem `Basis.mk_apply` states that for any type `ι`, any ring `R`, any additive commutative group `M`, and any function `v` from `ι` to `M`, given that `v` is linearly independent over `R` and the span of the range of `v` is the whole module `M` (i.e., every element of `M` can be expressed as a linear combination of elements in the range of `v`), then for any `i` of type `ι`, the `i`th element of the basis created by `v` is exactly the `i`th element of `v`. In other words, the basis created using `v` under these conditions is identical to `v` itself.
More concisely: If `v` is a linearly independent function from type `ι` to an additive commutative group `M` over ring `R` such that the span of `v` equals `M`, then the basis obtained from `v` is equal to `v` itself.
|