Algebra.rank_eq_of_equiv_equiv
theorem Algebra.rank_eq_of_equiv_equiv :
∀ {R : Type w} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {R' : Type w'}
{S' : Type v} [inst_3 : CommRing R'] [inst_4 : Ring S'] [inst_5 : Algebra R' S'] (i : R ≃+* R') (j : S ≃+* S'),
(algebraMap R' S').comp i.toRingHom = j.toRingHom.comp (algebraMap R S) → Module.rank R S = Module.rank R' S'
The theorem `Algebra.rank_eq_of_equiv_equiv` states that for any commutative ring `R`, ring `S`, and algebra structure between `R` and `S`, and any other commutative ring `R'`, ring `S'`, and algebra structure between `R'` and `S'`, if there exist ring isomorphisms `i` from `R` to `R'` and `j` from `S` to `S'` such that the algebra map from `R'` to `S'` composed with `i` equals `j` composed with the algebra map from `R` to `S`, then the rank of the module `S` over `R` is equal to the rank of the module `S'` over `R'`. Here, the rank of a module is the cardinality of its basis, and `algebraMap` is a function that returns the ring homomorphism associated with a given algebra structure.
More concisely: If there exist ring isomorphisms between commutative rings `R` and `R'`, and between their algebra structures over a commutative ring `S`, then the modules `S` over `R` and `S'` over `R'` have equal rank.
|
LinearEquiv.rank_eq
theorem LinearEquiv.rank_eq :
∀ {R : Type u} {M M₁ : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M₁]
[inst_3 : Module R M] [inst_4 : Module R M₁], (M ≃ₗ[R] M₁) → Module.rank R M = Module.rank R M₁
This theorem states that if two vector spaces, M and M₁, are linearly equivalent over a ring R, then they have the same dimension. It applies to any types M and M₁ that form additive commutative groups and are modules over the ring R. The operator ≃ₗ[R] denotes a linear equivalence between the vector spaces. The dimension of a vector space is represented by the function `Module.rank`.
More concisely: If two additive commutative groups M and M₁ are linearly equivalent modules over a ring R, then they have equal dimensions.
|
Algebra.rank_le_of_surjective_injective
theorem Algebra.rank_le_of_surjective_injective :
∀ {R : Type w} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {R' : Type w'}
{S' : Type v} [inst_3 : CommRing R'] [inst_4 : Ring S'] [inst_5 : Algebra R' S'] (i : R →+* R') (j : S →+* S'),
Function.Surjective ⇑i →
Function.Injective ⇑j →
(algebraMap R' S').comp i = j.comp (algebraMap R S) → Module.rank R S ≤ Module.rank R' S'
The theorem `Algebra.rank_le_of_surjective_injective` states that for any two ringed types `R` and `R'` with a commutative ring structure, and any two ringed types `S` and `S'` with a ring structure, where `R` and `S` have an algebra structure and `R'` and `S'` also have an algebra structure, if there exist ring homomorphisms `i : R →+* R'` and `j : S →+* S'` such that `i` is surjective and `j` is injective, and the algebra map from `R'` to `S'` composed with `i` is equal to `j` composed with the algebra map from `R` to `S`, then the rank of `S` as an `R`-module is less than or equal to the rank of `S'` as an `R'`-module.
More concisely: If `i : R -> R'` is a surjective ring homomorphism and `j : S -> S'` is an injective ring homomorphism between rings `R`, `R'`, `S`, and `S'` such that the algebra maps `R -> S` and `R' -> S'` satisfy `(R'.algebraMap : R' -> S') . i = j . (R.algebraMap : R -> S)`, then the rank of `S` as an `R`-module is less than or equal to the rank of `S'` as an `R'`-module.
|
LinearIndependent.cardinal_le_rank
theorem LinearIndependent.cardinal_le_rank :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : Nontrivial R]
{ι : Type v} {v : ι → M}, LinearIndependent R v → Cardinal.mk ι ≤ Module.rank R M
This theorem states that for any type `R` with a ring structure, a type `M` with an additive commutative group structure and a module structure over `R`, and a nontrivial structure for `R`, given another type `ι` and a function `v` which maps `ι` to `M` such that `v` is linearly independent over `R`, the cardinality of the type `ι` is less than or equal to the rank of the module `M` over `R`. In mathematical terms, if a set of vectors is linearly independent, then the size of this set is less than or equal to the rank of the vector space.
More concisely: Given a ring `R`, an additive commutative group `M` with a module structure over `R`, and a linearly independent set `v` of elements from `M` with domain `ι`, the cardinality of `ι` is less than or equal to the rank of the `R`-module `M`.
|
lift_rank_range_le
theorem lift_rank_range_le :
∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M']
[inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M'),
Cardinal.lift.{v, v'} (Module.rank R ↥(LinearMap.range f)) ≤ Cardinal.lift.{v', v} (Module.rank R M)
This theorem states that for any given ring `R` and two additive commutative groups `M` and `M'` with `M` and `M'` being modules over `R`, and a linear map `f` from `M` to `M'`, the cardinality (or "rank" in terms of modules) of the image (or "range") of `f` is less than or equal to the cardinality (or "rank") of the source module `M`. In other words, the dimension of the image of a linear map is always less than or equal to the dimension of the domain. This is done by lifting the cardinalities to a common universe before comparing.
More concisely: The cardinality of the image of a linear map between two finite-dimensional modules over a ring is less than or equal to the cardinality of the source module.
|
rank_le_of_submodule
theorem rank_le_of_submodule :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (s t : Submodule R M),
s ≤ t → Module.rank R ↥s ≤ Module.rank R ↥t
This theorem states that for any two submodules `s` and `t` of a module `M` over a ring `R` (where `M` is also an additive commutative group), if `s` is a subset of (or equal to) `t`, then the rank of `s` is less than or equal to the rank of `t`. In other words, the dimension of a submodule cannot exceed the dimension of the module it is contained in.
More concisely: If `s` is a submodule of module `M` over ring `R` with `s` being a subset of or equal to submodule `t`, then the rank of `s` is less than or equal to the rank of `t`.
|
cardinal_lift_le_rank_of_linearIndependent'
theorem cardinal_lift_le_rank_of_linearIndependent' :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : Nontrivial R]
{ι : Type w} {v : ι → M},
LinearIndependent R v → Cardinal.lift.{v, w} (Cardinal.mk ι) ≤ Cardinal.lift.{w, v} (Module.rank R M)
The theorem `cardinal_lift_le_rank_of_linearIndependent'` states that for any ring `R`, an additive commutative group `M`, a module `M` over the ring `R`, and a nontrivial ring `R`, if we have a type `ι` and a function `v` from `ι` to `M` such that `v` is a linearly independent family of vectors over `R`, then the lift of the cardinal number of `ι` (which can be thought of as "the size of `ι`") is less than or equal to the lift of the rank of the module `M` over the ring `R`. The cardinal lift operation is lifting the cardinal number from one universe to another. The rank of a module over a ring is the size of a largest linearly independent subset.
More concisely: For any commutative ring R, additive group M as an R-module, and nontrivial R, if ι has a linearly independent family v: ι → M, then |ι| (lifted cardinality) ≤ rank M (lifted rank), where |.| is the cardinality function and rank M is the size of a maximal linearly independent subset in M over R.
|
rank_top
theorem rank_top :
∀ (R : Type u) (M : Type v) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
Module.rank R ↥⊤ = Module.rank R M
This theorem, `rank_top`, states that for any Ring `R` and any Additive Commutative Group `M` which is also a `R`-module, the rank of the top submodule of `M` (denoted by `↥⊤`) is equal to the rank of the module `M` itself. In other words, it expresses that the maximal submodule of a module has the same rank as the module itself.
More concisely: The rank of the top submodule of an R-module M, as an R-vector space, equals the rank of M.
|
LinearMap.lift_rank_le_of_injective
theorem LinearMap.lift_rank_le_of_injective :
∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M']
[inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M'),
Function.Injective ⇑f → Cardinal.lift.{v', v} (Module.rank R M) ≤ Cardinal.lift.{v, v'} (Module.rank R M')
This theorem, `LinearMap.lift_rank_le_of_injective`, states that for any ring `R` and additive commutative groups `M` and `M'` that are also `R`-modules, if we have a linear map `f` from `M` to `M'` that is injective (meaning that if the map sends two elements of `M` to the same element of `M'`, then those two elements were the same to begin with), then the rank of `M` (after a universe-lifting operation) is less than or equal to the rank of `M'` (after a universe-lifting operation). Here, the rank of a module is a measure of the "size" of the module, and is represented as a cardinal number. The universe-lifting operation is a way of relating cardinal numbers from different type universes.
More concisely: If `f : M -> M'` is an injective linear map between free `R`-modules `M` and `M'` of finite rank, then the rank of `M` is less than or equal to the rank of `M'`.
|
Algebra.rank_le_of_injective_injective
theorem Algebra.rank_le_of_injective_injective :
∀ {R : Type w} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {R' : Type w'}
{S' : Type v} [inst_3 : CommRing R'] [inst_4 : Ring S'] [inst_5 : Algebra R' S'] (i : R' →+* R) (j : S →+* S'),
Function.Injective ⇑i →
Function.Injective ⇑j →
(j.comp (algebraMap R S)).comp i = algebraMap R' S' → Module.rank R S ≤ Module.rank R' S'
This theorem, named `Algebra.rank_le_of_injective_injective`, states the following:
Given two types `R` and `S`, with `R` being a commutative ring and `S` a ring, and an algebra structure from `R` to `S`, and similarly another two types `R'` and `S'`, also with `R'` being a commutative ring, `S'` a ring, and an algebra structure from `R'` to `S'`. If there exist two homomorphisms `i` from `R'` to `R` and `j` from `S` to `S'` which are both injective, and the composition of `j` with the algebra map from `R` to `S` followed by `i` equals the algebra map from `R'` to `S'`, then the rank of the module `S` over the ring `R` is less than or equal to the rank of the module `S'` over the ring `R'`.
Here, "rank" of a module over a ring is a measure of the size of a basis, or a minimal generating set, for the module. So this theorem is discussing a kind of size comparison between two modules under certain conditions.
More concisely: If two commutative rings `R` and `R'`, their modules `S` over `R` and `S'` over `R'`, and algebra structures between them satisfy the given conditions of injective homomorphisms `i` from `R'` to `R` and `j` from `S` to `S'`, then the rank of `S` over `R` is less than or equal to the rank of `S'` over `R'`.
|
rank_submodule_le
theorem rank_submodule_le :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (s : Submodule R M),
Module.rank R ↥s ≤ Module.rank R M
This theorem states that for any Ring `R` and an additive commutative group `M` that also has a structure of `R`-Module, the rank of any submodule `s` of `M` is less than or equal to the rank of `M` itself. In mathematical terms, this means that the dimension of a subspace is always less than or equal to the dimension of the space that it is contained in.
More concisely: For any submodule `s` of an `R`-Module `M` over a ring `R`, the rank of `s` is less than or equal to the rank of `M`.
|
LinearEquiv.lift_rank_eq
theorem LinearEquiv.lift_rank_eq :
∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M']
[inst_3 : Module R M] [inst_4 : Module R M'],
(M ≃ₗ[R] M') → Cardinal.lift.{v', v} (Module.rank R M) = Cardinal.lift.{v, v'} (Module.rank R M')
This theorem states that if you have two vector spaces, `M` and `M'`, over a ring `R`, that are linearly equivalent (denoted by `M ≃ₗ[R] M'`), then their dimensions are the same, even when the vector spaces exist in different universes. In particular, the dimensions are represented using the cardinality function `Module.rank`, and the universes' dimensions, possibly different, are equalized through the use of the `Cardinal.lift` function.
More concisely: If two vector spaces over a ring are linearly equivalent, then they have equal dimensions.
|
cardinal_le_rank_of_linearIndependent'
theorem cardinal_le_rank_of_linearIndependent' :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : Nontrivial R]
{s : Set M}, (LinearIndependent R fun (x : ↑s) => ↑x) → Cardinal.mk ↑s ≤ Module.rank R M
This theorem, `cardinal_le_rank_of_linearIndependent'`, states that for any ring `R`, an additive commutative group `M`, and a module of `R` and `M` with non-trivial `R`, if a set `s` of `M` is linearly independent over `R` (where each member of the set `s` is a vector in the vector space), then the cardinality (or "size") of set `s` is less than or equal to the rank of the module `R` over `M`. Here, the rank of a module is a measure of the 'size' or 'dimension' of the module, and a set is said to be linearly independent if no vector in the set can be written as a linear combination of the others.
More concisely: For any commutative ring R, additive group M, and R-module M with non-zero R-rank, if S is a linearly independent set in M, then the cardinality of S is less than or equal to the rank of M as an R-module.
|
rank_le_of_injective_injective
theorem rank_le_of_injective_injective :
∀ {R : Type u} {R' : Type u'} {M M₁ : Type v} [inst : Ring R] [inst_1 : Ring R'] [inst_2 : AddCommGroup M]
[inst_3 : AddCommGroup M₁] [inst_4 : Module R M] [inst_5 : Module R' M₁] (i : R' → R) (j : M →+ M₁),
(∀ (r : R'), i r = 0 → r = 0) →
Function.Injective ⇑j → (∀ (r : R') (m : M), j (i r • m) = r • j m) → Module.rank R M ≤ Module.rank R' M₁
The theorem `rank_le_of_injective_injective` says that for any two types `R` and `R'` representing rings, and any two types `M` and `M₁` representing additive commutative groups that are also modules over `R` and `R'` respectively, given a function `i` from `R'` to `R` and an additive group homomorphism `j` from `M` to `M₁`, if for all `r` in `R'`, `i` maps `r` to `0` implies `r` is `0`, and `j` is injective, and for all `r` in `R'` and `m` in `M`, mapping `m` scaled by `i r` under `j` equals to `j m` scaled by `r`, then the rank of the module `M` over `R` is less than or equal to the rank of the module `M₁` over `R'`.
More concisely: If `i` is a ring homomorphism from `R'` to `R`, `j` is an injective additive group homomorphism from an `R`-module `M` to an `R'`-module `M₁`, and for all `r` in `R'` and `m` in `M`, `j(rm) = r(j(m))`, then the rank of `M` over `R` is less than or equal to the rank of `M₁` over `R'`.
|
Algebra.lift_rank_le_of_injective_injective
theorem Algebra.lift_rank_le_of_injective_injective :
∀ {R : Type w} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {R' : Type w'}
{S' : Type v'} [inst_3 : CommRing R'] [inst_4 : Ring S'] [inst_5 : Algebra R' S'] (i : R' →+* R) (j : S →+* S'),
Function.Injective ⇑i →
Function.Injective ⇑j →
(j.comp (algebraMap R S)).comp i = algebraMap R' S' →
Cardinal.lift.{v', v} (Module.rank R S) ≤ Cardinal.lift.{v, v'} (Module.rank R' S')
The theorem `Algebra.lift_rank_le_of_injective_injective` states that if `S / R` and `S' / R'` are algebras, and `i : R' →+* R` and `j : S →+* S'` are injective ring homomorphisms such that the composition of functions from `R'` to `R`, `R` to `S`, and `S` to `S'` is the same as the function from `R'` to `S'`, then the rank of the algebra `S / R` (measured as a cardinal number and lifted to a common universe) is less than or equal to the rank of the algebra `S' / R'`. In other words, the rank (size of a basis) of an algebra can't increase under an injective homomorphism that commutes with the algebra structures.
More concisely: If `i : R' → R` and `j : S → S'` are injective ring homomorphisms between commutative rings `R`, `R'`, `S`, and `S'`, such that `j (r * s) = i r * j s` for all `r in R` and `s in S`, then the rank of `S / R` is less than or equal to the rank of `S' / R'`.
|
rank_range_of_surjective
theorem rank_range_of_surjective :
∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M']
[inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M'),
Function.Surjective ⇑f → Module.rank R ↥(LinearMap.range f) = Module.rank R M'
The theorem `rank_range_of_surjective` states that for any ring `R`, and for any two types `M` and `M'` that form commutative additive groups and are modules over `R`, if there exists a linear map `f` from `M` to `M'` which is surjective (every element in `M'` is the image of some element in `M` under `f`), then the rank of the range of `f` (as a module over `R`) is equal to the rank of `M'` when it's considered as a module over `R`. In more mathematical terms, if $f: M \rightarrow M'$ is a surjective linear map between two modules over a ring $R$, then the rank of the range of $f$ as a $R$-module is equal to the rank of the $R$-module $M'$.
More concisely: For any surjective linear map `f` between commutative additive groups and R-modules `M` and `M'`, the rank of the range of `f` as an R-module equals the rank of M' as an R-module.
|
Algebra.lift_rank_le_of_surjective_injective
theorem Algebra.lift_rank_le_of_surjective_injective :
∀ {R : Type w} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {R' : Type w'}
{S' : Type v'} [inst_3 : CommRing R'] [inst_4 : Ring S'] [inst_5 : Algebra R' S'] (i : R →+* R') (j : S →+* S'),
Function.Surjective ⇑i →
Function.Injective ⇑j →
(algebraMap R' S').comp i = j.comp (algebraMap R S) →
Cardinal.lift.{v', v} (Module.rank R S) ≤ Cardinal.lift.{v, v'} (Module.rank R' S')
This theorem states that if `S / R` and `S' / R'` are algebras, where `R → R'` is a surjective ring homomorphism denoted by `i` and `S → S'` is an injective ring homomorphism denoted by `j`, and the compositions `R → R' → S'` and `R → S → S'` commute, then the rank (the cardinality of a basis) of `S / R` is less than or equal to the rank of `S' / R'`. Here, the rank is considered as a cardinal number and lifted to a common universe to make the comparison meaningful. The notion of rank is generalized from the rank of a free module (number of elements in a basis).
More concisely: If `i: R → R'` is a surjective ring homomorphism, `j: S → S'` is an injective ring homomorphism with commuting compositions `R → S → S'` and `R → R' → S'`, then the rank of `S / R` is less than or equal to the rank of `S' / R'`.
|
rank_eq_of_equiv_equiv
theorem rank_eq_of_equiv_equiv :
∀ {R : Type u} {R' : Type u'} {M M₁ : Type v} [inst : Ring R] [inst_1 : Ring R'] [inst_2 : AddCommGroup M]
[inst_3 : AddCommGroup M₁] [inst_4 : Module R M] [inst_5 : Module R' M₁] (i : ZeroHom R R') (j : M ≃+ M₁),
Function.Bijective ⇑i → (∀ (r : R) (m : M), j (r • m) = i r • j m) → Module.rank R M = Module.rank R' M₁
This theorem, `rank_eq_of_equiv_equiv`, states that for any two types `R` and `R'` representing rings, and any two types `M` and `M₁` representing additive commutative groups with a module structure over `R` and `R'` respectively, if there exists a zero-preserving homomorphism `i` from `R` to `R'`, and an additive group isomorphism `j` from `M` to `M₁`, such that `i` is bijective and `j` preserves scalar multiplication (in the sense that for any scalar `r` in `R` and vector `m` in `M`, the image of the scalar multiplied vector `r • m` under `j` is equal to the image of `r` under `i` scalar multiplied by the image of `m` under `j`), then the rank of the module `M` over `R` is equal to the rank of the module `M₁` over `R'`.
More concisely: If there exists a ring homomorphism i from R to R', a group isomorphism j from M to M\_1 that is a scalar multiplication preserving additive homomorphism, and i is bijective, then the rank of the module M over R is equal to the rank of the module M\_1 over R'.
|
LinearEquiv.rank_map_eq
theorem LinearEquiv.rank_map_eq :
∀ {R : Type u} {M M₁ : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M₁]
[inst_3 : Module R M] [inst_4 : Module R M₁] (f : M ≃ₗ[R] M₁) (p : Submodule R M),
Module.rank R ↥(Submodule.map (↑f) p) = Module.rank R ↥p
The theorem `LinearEquiv.rank_map_eq` states that for any ring `R`, and any two types `M` and `M₁` that are modules over `R`, if there is a linear equivalence `f` between `M` and `M₁`, and `p` is a submodule of `M`, then the dimension (rank) of the pushforward of `p` along `f` (i.e., the submodule of `M₁` obtained by applying `f` to every element of `p`) is the same as the dimension (rank) of `p` itself. This theorem is essentially saying that linear equivalences preserve the dimension of submodules.
More concisely: For any ring `R`, given modules `M` and `M₁` over `R`, if there is a linear equivalence `f : M ≅ M₁` and `p ⊆ M` is a submodule, then the rank of `f(p)` equals the rank of `p`.
|
rank_le_of_surjective_injective
theorem rank_le_of_surjective_injective :
∀ {R : Type u} {R' : Type u'} {M M₁ : Type v} [inst : Ring R] [inst_1 : Ring R'] [inst_2 : AddCommGroup M]
[inst_3 : AddCommGroup M₁] [inst_4 : Module R M] [inst_5 : Module R' M₁] (i : ZeroHom R R') (j : M →+ M₁),
Function.Surjective ⇑i →
Function.Injective ⇑j → (∀ (r : R) (m : M), j (r • m) = i r • j m) → Module.rank R M ≤ Module.rank R' M₁
The theorem `rank_le_of_surjective_injective` states that for any two types `R` and `R'`, and any two types `M` and `M₁` which form modules over `R` and `R'` respectively, given a ring homomorphism `i` from `R` to `R'` and an additive group homomorphism `j` from `M` to `M₁`, if `i` is surjective and `j` is injective, and for all `r` in `R` and `m` in `M`, the action of `j` on the scalar multiplication `r • m` is the same as the scalar multiplication `i r • j m`, then the rank of the module `M` over `R` is less than or equal to the rank of the module `M₁` over `R'`. In mathematical terms, this theorem is about the relation between the ranks of two modules under certain conditions of surjectivity, injectivity, and a particular equality of scalar multiplications.
More concisely: If `i` is a surjective ring homomorphism from `R` to `R'`, `j` is an injective additive group homomorphism from the module `M` over `R` to the module `M₁` over `R'`, and for all `r` in `R` and `m` in `M`, `r • m = i r • j m`, then the rank of `M` is less than or equal to the rank of `M₁`.
|
LinearIndependent.cardinal_lift_le_rank
theorem LinearIndependent.cardinal_lift_le_rank :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : Nontrivial R]
{ι : Type w} {v : ι → M},
LinearIndependent R v → Cardinal.lift.{v, w} (Cardinal.mk ι) ≤ Cardinal.lift.{w, v} (Module.rank R M)
The theorem `LinearIndependent.cardinal_lift_le_rank` states that for any ring `R` and `AddCommGroup` `M` (with `M` being a module over `R`), given a family of vectors `v` indexed by type `ι` that is linearly independent over `R`, the cardinality of `ι` (after applying the universe lift operation) is less than or equal to the rank of the module `M` over `R` (again, after applying the universe lift operation). In other words, the lifted cardinality of the set of indices of a linearly independent family of vectors is less than or equal to the lifted rank of the module.
More concisely: For any ring `R` and `AddCommGroup` `M` (a module over `R`), if `ι` is the index type of a linearly independent family of vectors in `M` over `R`, then the lifted cardinality of `ι` is less than or equal to the lifted rank of `M` over `R`.
|
lift_rank_le_of_injective_injective
theorem lift_rank_le_of_injective_injective :
∀ {R : Type u} {R' : Type u'} {M : Type v} {M' : Type v'} [inst : Ring R] [inst_1 : Ring R']
[inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M'] [inst_4 : Module R M] [inst_5 : Module R' M'] (i : R' → R)
(j : M →+ M'),
(∀ (r : R'), i r = 0 → r = 0) →
Function.Injective ⇑j →
(∀ (r : R') (m : M), j (i r • m) = r • j m) →
Cardinal.lift.{v', v} (Module.rank R M) ≤ Cardinal.lift.{v, v'} (Module.rank R' M')
This theorem states that if `M / R` and `M' / R'` are modules, `i : R' → R` is a function that maps non-zero elements to non-zero elements, and `j : M →+ M'` is an injective group homomorphism such that the scalar multiplications on `M` and `M'` are compatible, then the rank of `M / R` (lifted to a higher universe) is less than or equal to the rank of `M' / R'` (lifted to a higher universe). This theorem can be specialized to the case where `R = R'` to give a result about the rank of a module under an injective linear map. The rank of a module is a cardinality measure of its basis, so this theorem is essentially asserting that the "size" of a module does not increase under an injective linear map.
More concisely: If `i : R' → R` is a function mapping non-zero elements to non-zero elements, `j : M →+ M'` is an injective group homomorphism between modules `M / R` and `M' / R'` with compatible scalar multiplications, then the rank of `M / R` (in a higher universe) is less than or equal to the rank of `M' / R'` (in a higher universe).
|
lift_rank_le_of_surjective_injective
theorem lift_rank_le_of_surjective_injective :
∀ {R : Type u} {R' : Type u'} {M : Type v} {M' : Type v'} [inst : Ring R] [inst_1 : Ring R']
[inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M'] [inst_4 : Module R M] [inst_5 : Module R' M']
(i : ZeroHom R R') (j : M →+ M'),
Function.Surjective ⇑i →
Function.Injective ⇑j →
(∀ (r : R) (m : M), j (r • m) = i r • j m) →
Cardinal.lift.{v', v} (Module.rank R M) ≤ Cardinal.lift.{v, v'} (Module.rank R' M')
The theorem states that for any two modules `M / R` and `M' / R'`, if there exists a surjective map `i` from `R` to `R'` that maps zero to zero and an injective group homomorphism `j` from `M` to `M'` that is compatible with the scalar multiplications on `M` and `M'`, then the rank (dimension of the space over the field `R`) of the module `M / R` is less than or equal to the rank of the module `M' / R'`.
In a special case where `R = R'`, this theorem reduces to `LinearMap.lift_rank_le_of_injective`, which says that the rank of a module does not increase when it is mapped injectively into another module.
The rank of a module is measured in terms of cardinals, which are a generalization of the natural numbers to possibly infinite sets. The `Cardinal.lift` function is used here to handle the fact that the rank may live in a different universe (size of set) in Lean 4, which tracks the size of sets to avoid paradoxes.
More concisely: Given modules `M/R` and `M'/R'`, if there exists a surjective ring homomorphism `i: R → R'` with `i(0) = 0` and an injective group homomorphism `j: M → M'` compatible with scalar multiplications, then the rank of `M/R` is less than or equal to the rank of `M'/R'`.
|
Module.rank_def
theorem Module.rank_def :
∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
Module.rank R M = ⨆ ι, Cardinal.mk ↑↑ι
The `Module.rank_def` theorem states that for any Type 'R', Type 'M', where 'R' is a semiring, 'M' is an additive commutative monoid, and 'M' is a module over 'R', the rank of the module 'M' over the ring 'R' is equal to the supremum over all cardinal numbers 'ι'. In other words, the rank of a module over a ring is determined by the highest cardinal number of its basis.
More concisely: The rank of a module over a semiring is equal to the size of its largest basis.
|
lift_rank_eq_of_equiv_equiv
theorem lift_rank_eq_of_equiv_equiv :
∀ {R : Type u} {R' : Type u'} {M : Type v} {M' : Type v'} [inst : Ring R] [inst_1 : Ring R']
[inst_2 : AddCommGroup M] [inst_3 : AddCommGroup M'] [inst_4 : Module R M] [inst_5 : Module R' M']
(i : ZeroHom R R') (j : M ≃+ M'),
Function.Bijective ⇑i →
(∀ (r : R) (m : M), j (r • m) = i r • j m) →
Cardinal.lift.{v', v} (Module.rank R M) = Cardinal.lift.{v, v'} (Module.rank R' M')
This theorem, named `lift_rank_eq_of_equiv_equiv`, states that if we have two modules, `M / R` and `M' / R'`, and `i : R → R'` is a bijective map that sends zero to zero, and `j : M ≃+ M'` is a group isomorphism such that the scalar multiplications on `M` and `M'` are compatible (that is, for all `r : R` and `m : M`, the result of scaling `m` by `r` and then applying `j` is the same as applying `j` to `m` and then scaling by `i r`), then the lift of the rank of `M / R` to a larger universe (represented by `Cardinal.lift (Module.rank R M)`) is equal to the lift of the rank of `M' / R'` to a larger universe (represented by `Cardinal.lift (Module.rank R' M')`). As a special case, when `R = R'`, this theorem reduces to `LinearEquiv.lift_rank_eq`.
More concisely: If `i : R → R'` is a bijective map sending zero to zero, `j : M ≃+ M'` is a group isomorphism with compatible scalar multiplications, then `Cardinal.lift (Module.rank R M) = Cardinal.lift (Module.rank R' M')`.
|
cardinal_lift_le_rank_of_linearIndependent
theorem cardinal_lift_le_rank_of_linearIndependent :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : Nontrivial R]
{ι : Type w} {v : ι → M},
LinearIndependent R v → Cardinal.lift.{v, w} (Cardinal.mk ι) ≤ Cardinal.lift.{w, v} (Module.rank R M)
The theorem `cardinal_lift_le_rank_of_linearIndependent` states that for any type `R` with a ring structure, any type `M` that is an additive commutative group and a module over `R`, any non-trivial type `R`, any type `ι`, and any function `v` from `ι` to `M` that provides a linearly independent family of vectors, the cardinality of the type `ι` (interpreted as the cardinality of a set of indices for the family of vectors), when lifted to the larger of the universes of `M` and `ι`, is less than or equal to the rank of the module `M` over `R`, when also lifted to the larger of the universes of `M` and `ι`. The rank of a module is a measure of its "size" or "complexity", similar to the dimension of a vector space.
More concisely: For any ring `R`, additive commutative group and `R`-module `M`, linearly independent family `v` of `M` vectors indexed by type `ι`, the cardinality of `ι` (lifted to the larger universe) is less than or equal to the rank of `M` over `R` (lifted to the larger universe).
|
cardinal_le_rank_of_linearIndependent
theorem cardinal_le_rank_of_linearIndependent :
∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : Nontrivial R]
{ι : Type v} {v : ι → M}, LinearIndependent R v → Cardinal.mk ι ≤ Module.rank R M
The theorem `cardinal_le_rank_of_linearIndependent` states that for any type `R` with a Ring structure, any type `M` with an additive commutative group structure and a module over `R` structure, and any nontrivial type `R`, given also a type `ι` and a mapping `v` from `ι` to `M`, if the family of vectors `v` is linearly independent over `R`, then the cardinality of the type `ι` (i.e., the "size" of the set of indices) is less than or equal to the rank of the module `M` over `R`. This basically means that the number of linearly independent vectors in a module is at most the rank of the module.
More concisely: If `R` is a ring, `M` is an `R`-module with an additive commutative group structure, `ι` is a nonempty set, and the family `{v(i) | i ∈ ι}` of vectors in `M` is linearly independent over `R`, then the cardinality of `ι` is less than or equal to the rank of `M` over `R`.
|
Algebra.lift_rank_eq_of_equiv_equiv
theorem Algebra.lift_rank_eq_of_equiv_equiv :
∀ {R : Type w} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {R' : Type w'}
{S' : Type v'} [inst_3 : CommRing R'] [inst_4 : Ring S'] [inst_5 : Algebra R' S'] (i : R ≃+* R') (j : S ≃+* S'),
(algebraMap R' S').comp i.toRingHom = j.toRingHom.comp (algebraMap R S) →
Cardinal.lift.{v', v} (Module.rank R S) = Cardinal.lift.{v, v'} (Module.rank R' S')
The theorem `Algebra.lift_rank_eq_of_equiv_equiv` states that if `S / R` and `S' / R'` are algebras, where `R` and `R'` are commutative rings, and `S` and `S'` are rings, and we have ring isomorphisms `i : R ≃+* R'` and `j : S ≃+* S'` such that the maps `R → R' → S'` and `R → S → S'` commute, i.e., the composition of the algebra map from `R'` to `S'` with `i` is the same as the composition of `j` with the algebra map from `R` to `S`, then the rank of the `R`-module `S` is equal to the rank of the `R'`-module `S'`, where rank is measured in terms of the cardinality of a basis, and the comparison is done after lifting the cardinalities to a common universe.
More concisely: If `R` and `R'` are commutative rings, `S` and `S'` are rings, and there are ring isomorphisms `i : R ≃+* R'`, `j : S ≃+* S'` with commuting diagrams `R → R' → S'` and `R → S → S'`, then the ranks of the `R`-module `S` and the `R'`-module `S'` are equal.
|