doc-next-gen

Mathlib.LinearAlgebra.Dimension.Basic

Module docstring

{"# Dimension of modules and vector spaces

Main definitions

  • The rank of a module is defined as Module.rank : Cardinal. This is defined as the supremum of the cardinalities of linearly independent subsets.

Main statements

  • LinearMap.rank_le_of_injective: the source of an injective linear map has dimension at most that of the target.
  • LinearMap.rank_le_of_surjective: the target of a surjective linear map has dimension at most that of that source.

Implementation notes

Many theorems in this file are not universe-generic when they relate dimensions in different universes. They should be as general as they can be without inserting lifts. The types M, M', ... all live in different universes, and M₁, M₂, ... all live in the same universe. "}

Module.rank definition
Full source 
/-- The rank of a module, defined as a term of type `Cardinal`.

We define this as the supremum of the cardinalities of linearly independent subsets.
The supremum may not be attained, see https://mathoverflow.net/a/263053.

For a free module over any ring satisfying the strong rank condition
(e.g. left-noetherian rings, commutative rings, and in particular division rings and fields),
this is the same as the dimension of the space (i.e. the cardinality of any basis).

In particular this agrees with the usual notion of the dimension of a vector space.

See also `Module.finrank` for a `ℕ`-valued function which returns the correct value
for a finite-dimensional vector space (but 0 for an infinite-dimensional vector space).
-/
@[stacks 09G3 "first part"]
protected irreducible_def Module.rank : Cardinal :=
  ⨆ ι : { s : Set M // LinearIndepOn R id s }, (#ι.1)
Rank of a module
Informal description
The rank of a module $M$ over a ring $R$ is defined as the supremum of the cardinalities of all linearly independent subsets of $M$. For a free module over a ring satisfying the strong rank condition (such as left-noetherian rings, commutative rings, division rings, or fields), this rank coincides with the dimension of the module, i.e., the cardinality of any basis. In particular, for vector spaces, this matches the conventional notion of dimension.
Module.rank_def theorem
: eta_helper Eq✝ @Module.rank.{} @(delta% @definition✝)
Full source 
/-- The rank of a module, defined as a term of type `Cardinal`.

We define this as the supremum of the cardinalities of linearly independent subsets.
The supremum may not be attained, see https://mathoverflow.net/a/263053.

For a free module over any ring satisfying the strong rank condition
(e.g. left-noetherian rings, commutative rings, and in particular division rings and fields),
this is the same as the dimension of the space (i.e. the cardinality of any basis).

In particular this agrees with the usual notion of the dimension of a vector space.

See also `Module.finrank` for a `ℕ`-valued function which returns the correct value
for a finite-dimensional vector space (but 0 for an infinite-dimensional vector space).
-/
@[stacks 09G3 "first part"]
protected irreducible_def Module.rank : Cardinal :=
  ⨆ ι : { s : Set M // LinearIndepOn R id s }, (#ι.1)
Definition of Module Rank as Supremum of Linearly Independent Subsets
Informal description
The rank of a module $M$ over a ring $R$ is defined as the supremum of the cardinalities of all linearly independent subsets of $M$.
rank_le_card theorem
: Module.rank R M ≤ #M
Full source 
theorem rank_le_card : Module.rank R M ≤ #M :=
  (Module.rank_def _ _).trans_le (ciSup_le' fun _ ↦ mk_set_le _)
Rank Bound by Cardinality of Module
Informal description
For any module $M$ over a ring $R$, the rank of $M$ is bounded above by the cardinality of $M$, i.e., $\text{rank}_R M \leq \#M$.
LinearIndependent.cardinal_lift_le_rank theorem
{ι : Type w} {v : ι → M} (hv : LinearIndependent R v) : Cardinal.lift.{v} #ι ≤ Cardinal.lift.{w} (Module.rank R M)
Full source 
theorem cardinal_lift_le_rank {ι : Type w} {v : ι → M}
    (hv : LinearIndependent R v) :
    Cardinal.lift.{v} #ι ≤ Cardinal.lift.{w} (Module.rank R M) := by
  rw [Module.rank]
  refine le_trans ?_ (lift_le.mpr <| le_ciSup (bddAbove_range _) ⟨_, hv.linearIndepOn_id⟩)
  exact lift_mk_le'.mpr ⟨(Equiv.ofInjective _ hv.injective).toEmbedding⟩
Cardinality of Linearly Independent Family Bounded by Module Rank
Informal description
Let $M$ be a module over a ring $R$, and let $\{v_i\}_{i \in \iota}$ be a linearly independent family of vectors in $M$ indexed by a type $\iota$. Then the cardinality of $\iota$ (lifted to a common universe) is less than or equal to the rank of $M$ (also lifted to the same universe), i.e., $\#\iota \leq \text{rank}_R M$.
LinearIndependent.aleph0_le_rank theorem
{ι : Type w} [Infinite ι] {v : ι → M} (hv : LinearIndependent R v) : ℵ₀ ≤ Module.rank R M
Full source 
lemma aleph0_le_rank {ι : Type w} [Infinite ι] {v : ι → M}
    (hv : LinearIndependent R v) : ℵ₀ ≤ Module.rank R M :=
  aleph0_le_lift.mp <| (aleph0_le_lift.mpr <| aleph0_le_mk ι).trans hv.cardinal_lift_le_rank
Infinite Linearly Independent Family Implies Module Rank at Least Aleph-Null
Informal description
Let $M$ be a module over a ring $R$, and let $\{v_i\}_{i \in \iota}$ be an infinite linearly independent family of vectors in $M$ indexed by a type $\iota$. Then the cardinality of $\iota$ is at least $\aleph_0$, and the rank of $M$ is also at least $\aleph_0$, i.e., $\aleph_0 \leq \text{rank}_R M$.
LinearIndependent.cardinal_le_rank theorem
{ι : Type v} {v : ι → M} (hv : LinearIndependent R v) : #ι ≤ Module.rank R M
Full source 
theorem cardinal_le_rank {ι : Type v} {v : ι → M}
    (hv : LinearIndependent R v) : #ι ≤ Module.rank R M := by
  simpa using hv.cardinal_lift_le_rank
Cardinality of Linearly Independent Family Bounded by Module Rank
Informal description
Let $M$ be a module over a ring $R$, and let $\{v_i\}_{i \in \iota}$ be a linearly independent family of vectors in $M$ indexed by a type $\iota$. Then the cardinality of $\iota$ is less than or equal to the rank of $M$, i.e., $\#\iota \leq \text{rank}_R M$.
LinearIndependent.cardinal_le_rank' theorem
{s : Set M} (hs : LinearIndependent R (fun x => x : s → M)) : #s ≤ Module.rank R M
Full source 
theorem cardinal_le_rank' {s : Set M}
    (hs : LinearIndependent R (fun x => x : s → M)) : #s ≤ Module.rank R M :=
  hs.cardinal_le_rank
Cardinality of Linearly Independent Subset Bounded by Module Rank
Informal description
Let $M$ be a module over a ring $R$, and let $s$ be a subset of $M$ such that the inclusion map $s \hookrightarrow M$ is $R$-linearly independent. Then the cardinality of $s$ is less than or equal to the rank of $M$ over $R$, i.e., $\#s \leq \text{rank}_R M$.
LinearIndepOn.encard_le_toENat_rank theorem
{ι : Type*} {v : ι → M} {s : Set ι} (hs : LinearIndepOn R v s) : s.encard ≤ (Module.rank R M).toENat
Full source 
theorem _root_.LinearIndepOn.encard_le_toENat_rank {ι : Type*} {v : ι → M} {s : Set ι}
    (hs : LinearIndepOn R v s) : s.encard ≤ (Module.rank R M).toENat := by
  simpa using OrderHom.mono (β := ℕ∞) Cardinal.toENat hs.linearIndependent.cardinal_lift_le_rank
Extended Cardinality Bound for Linearly Independent Subsets in Terms of Module Rank
Informal description
Let $M$ be a module over a ring $R$, and let $\{v_i\}_{i \in \iota}$ be a family of vectors in $M$ indexed by a type $\iota$. If the vectors $\{v_i\}_{i \in s}$ are linearly independent for some subset $s \subseteq \iota$, then the extended cardinality of $s$ is less than or equal to the rank of $M$ converted to an extended natural number, i.e., $\text{encard}(s) \leq (\text{rank}_R M).\text{toENat}$.
lift_rank_le_of_injective_injectiveₛ theorem
(i : R' → R) (j : M →+ M') (hi : Injective i) (hj : Injective j) (hc : ∀ (r : R') (m : M), j (i r • m) = r • j m) : lift.{v'} (Module.rank R M) ≤ lift.{v} (Module.rank R' M')
Full source 
/-- If `M / R` and `M' / R'` are modules, `i : R' → R` is an injective map
non-zero elements, `j : M →+ M'` is an injective monoid homomorphism, such that the scalar
multiplications on `M` and `M'` are compatible, then the rank of `M / R` is smaller than or equal to
the rank of `M' / R'`. As a special case, taking `R = R'` it is
`LinearMap.lift_rank_le_of_injective`. -/
theorem lift_rank_le_of_injective_injectiveₛ (i : R' → R) (j : M →+ M')
    (hi : Injective i) (hj : Injective j)
    (hc : ∀ (r : R') (m : M), j (i r • m) = r • j m) :
    lift.{v'} (Module.rank R M) ≤ lift.{v} (Module.rank R' M') := by
  simp_rw [Module.rank, lift_iSup (bddAbove_range _)]
  exact ciSup_mono' (bddAbove_range _) fun ⟨s, h⟩ ↦ ⟨⟨j '' s,
    LinearIndepOn.id_image (h.linearIndependent.map_of_injective_injectiveₛ i j hi hj hc)⟩,
    lift_mk_le'.mpr ⟨(Equiv.Set.image j s hj).toEmbedding⟩⟩
Rank Comparison under Injective Module Homomorphism with Compatible Scalar Multiplication
Informal description
Let $R$ and $R'$ be rings, and let $M$ be an $R$-module and $M'$ an $R'$-module. Suppose there exists an injective ring homomorphism $i: R' \to R$ (restricted to non-zero elements) and an injective additive homomorphism $j: M \to M'$ such that the scalar multiplication is compatible, i.e., for all $r \in R'$ and $m \in M$, we have $j(i(r) \cdot m) = r \cdot j(m)$. Then the rank of $M$ over $R$ is less than or equal to the rank of $M'$ over $R'$.
lift_rank_le_of_surjective_injective theorem
(i : R → R') (j : M →+ M') (hi : Surjective i) (hj : Injective j) (hc : ∀ (r : R) (m : M), j (r • m) = i r • j m) : lift.{v'} (Module.rank R M) ≤ lift.{v} (Module.rank R' M')
Full source 
/-- If `M / R` and `M' / R'` are modules, `i : R → R'` is a surjective map, and
`j : M →+ M'` is an injective monoid homomorphism, such that the scalar multiplications on `M` and
`M'` are compatible, then the rank of `M / R` is smaller than or equal to the rank of `M' / R'`.
As a special case, taking `R = R'` it is `LinearMap.lift_rank_le_of_injective`. -/
theorem lift_rank_le_of_surjective_injective (i : R → R') (j : M →+ M')
    (hi : Surjective i) (hj : Injective j) (hc : ∀ (r : R) (m : M), j (r • m) = i r • j m) :
    lift.{v'} (Module.rank R M) ≤ lift.{v} (Module.rank R' M') := by
  obtain ⟨i', hi'⟩ := hi.hasRightInverse
  refine lift_rank_le_of_injective_injectiveₛ i' j (fun _ _ h ↦ ?_) hj fun r m ↦ ?_
  · apply_fun i at h
    rwa [hi', hi'] at h
  rw [hc (i' r) m, hi']
Rank Comparison under Surjective Ring Homomorphism and Injective Module Homomorphism with Compatible Scalar Multiplication
Informal description
Let $R$ and $R'$ be rings, and let $M$ be an $R$-module and $M'$ an $R'$-module. Suppose there exists a surjective ring homomorphism $i: R \to R'$ and an injective additive homomorphism $j: M \to M'$ such that the scalar multiplication is compatible, i.e., for all $r \in R$ and $m \in M$, we have $j(r \cdot m) = i(r) \cdot j(m)$. Then the rank of $M$ over $R$ is less than or equal to the rank of $M'$ over $R'$.
lift_rank_eq_of_equiv_equiv theorem
(i : R → R') (j : M ≃+ M') (hi : Bijective i) (hc : ∀ (r : R) (m : M), j (r • m) = i r • j m) : lift.{v'} (Module.rank R M) = lift.{v} (Module.rank R' M')
Full source 
/-- If `M / R` and `M' / R'` are modules, `i : R → R'` is a bijective map which maps zero to zero,
`j : M ≃+ M'` is a group isomorphism, such that the scalar multiplications on `M` and `M'` are
compatible, then the rank of `M / R` is equal to the rank of `M' / R'`.
As a special case, taking `R = R'` it is `LinearEquiv.lift_rank_eq`. -/
theorem lift_rank_eq_of_equiv_equiv (i : R → R') (j : M ≃+ M')
    (hi : Bijective i) (hc : ∀ (r : R) (m : M), j (r • m) = i r • j m) :
    lift.{v'} (Module.rank R M) = lift.{v} (Module.rank R' M') :=
  (lift_rank_le_of_surjective_injective i j hi.2 j.injective hc).antisymm <|
    lift_rank_le_of_injective_injectiveₛ i j.symm hi.1
      j.symm.injective fun _ _ ↦ j.symm_apply_eq.2 <| by erw [hc, j.apply_symm_apply]
Rank Equality under Module Isomorphism with Compatible Ring Isomorphism
Informal description
Let $R$ and $R'$ be rings, and let $M$ be an $R$-module and $M'$ an $R'$-module. Suppose there exists a bijective ring homomorphism $i: R \to R'$ and a group isomorphism $j: M \simeq^+ M'$ such that the scalar multiplications are compatible, i.e., for all $r \in R$ and $m \in M$, we have $j(r \cdot m) = i(r) \cdot j(m)$. Then the rank of $M$ over $R$ is equal to the rank of $M'$ over $R'$.
rank_le_of_injective_injectiveₛ theorem
(i : R' → R) (j : M →+ M₁) (hi : Injective i) (hj : Injective j) (hc : ∀ (r : R') (m : M), j (i r • m) = r • j m) : Module.rank R M ≤ Module.rank R' M₁
Full source 
/-- The same-universe version of `lift_rank_le_of_injective_injective`. -/
theorem rank_le_of_injective_injectiveₛ (i : R' → R) (j : M →+ M₁)
    (hi : Injective i) (hj : Injective j)
    (hc : ∀ (r : R') (m : M), j (i r • m) = r • j m) :
    Module.rank R M ≤ Module.rank R' M₁ := by
  simpa only [lift_id] using lift_rank_le_of_injective_injectiveₛ i j hi hj hc
Rank Inequality under Injective Module Homomorphism with Compatible Scalar Multiplication
Informal description
Let $R$ and $R'$ be rings, and let $M$ be an $R$-module and $M₁$ an $R'$-module. Suppose there exists an injective ring homomorphism $i: R' \to R$ and an injective additive homomorphism $j: M \to M₁$ such that the scalar multiplication is compatible, i.e., for all $r \in R'$ and $m \in M$, we have $j(i(r) \cdot m) = r \cdot j(m)$. Then the rank of $M$ over $R$ is less than or equal to the rank of $M₁$ over $R'$.
rank_le_of_surjective_injective theorem
(i : R → R') (j : M →+ M₁) (hi : Surjective i) (hj : Injective j) (hc : ∀ (r : R) (m : M), j (r • m) = i r • j m) : Module.rank R M ≤ Module.rank R' M₁
Full source 
/-- The same-universe version of `lift_rank_le_of_surjective_injective`. -/
theorem rank_le_of_surjective_injective (i : R → R') (j : M →+ M₁)
    (hi : Surjective i) (hj : Injective j)
    (hc : ∀ (r : R) (m : M), j (r • m) = i r • j m) :
    Module.rank R M ≤ Module.rank R' M₁ := by
  simpa only [lift_id] using lift_rank_le_of_surjective_injective i j hi hj hc
Rank Inequality under Surjective Ring Homomorphism and Injective Module Homomorphism with Compatible Scalar Multiplication
Informal description
Let $R$ and $R'$ be rings, and let $M$ be an $R$-module and $M₁$ an $R'$-module. Suppose there exists a surjective ring homomorphism $i: R \to R'$ and an injective additive homomorphism $j: M \to M₁$ such that the scalar multiplication is compatible, i.e., for all $r \in R$ and $m \in M$, we have $j(r \cdot m) = i(r) \cdot j(m)$. Then the rank of $M$ over $R$ is less than or equal to the rank of $M₁$ over $R'$.
rank_eq_of_equiv_equiv theorem
(i : R → R') (j : M ≃+ M₁) (hi : Bijective i) (hc : ∀ (r : R) (m : M), j (r • m) = i r • j m) : Module.rank R M = Module.rank R' M₁
Full source 
/-- The same-universe version of `lift_rank_eq_of_equiv_equiv`. -/
theorem rank_eq_of_equiv_equiv (i : R → R') (j : M ≃+ M₁)
    (hi : Bijective i) (hc : ∀ (r : R) (m : M), j (r • m) = i r • j m) :
    Module.rank R M = Module.rank R' M₁ := by
  simpa only [lift_id] using lift_rank_eq_of_equiv_equiv i j hi hc
Rank Equality under Module Isomorphism with Compatible Ring Isomorphism (Same Universe)
Informal description
Let $R$ and $R'$ be rings, and let $M$ be an $R$-module and $M_1$ an $R'$-module. Suppose there exists a bijective ring homomorphism $i: R \to R'$ and a group isomorphism $j: M \simeq^+ M_1$ such that the scalar multiplications are compatible, i.e., for all $r \in R$ and $m \in M$, we have $j(r \cdot m) = i(r) \cdot j(m)$. Then the rank of $M$ over $R$ is equal to the rank of $M_1$ over $R'$.
lift_rank_le_of_injective_injective theorem
[AddCommGroup M'] [Module R' M'] (i : R' → R) (j : M →+ M') (hi : ∀ r, i r = 0 → r = 0) (hj : Injective j) (hc : ∀ (r : R') (m : M), j (i r • m) = r • j m) : lift.{v'} (Module.rank R M) ≤ lift.{v} (Module.rank R' M')
Full source 
/-- If `M / R` and `M' / R'` are modules, `i : R' → R` is a map which sends non-zero elements to
non-zero elements, `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` is smaller than or equal to
the rank of `M' / R'`. As a special case, taking `R = R'` it is
`LinearMap.lift_rank_le_of_injective`. -/
theorem lift_rank_le_of_injective_injective [AddCommGroup M'] [Module R' M']
    (i : R' → R) (j : M →+ M') (hi : ∀ r, i r = 0 → r = 0) (hj : Injective j)
    (hc : ∀ (r : R') (m : M), j (i r • m) = r • j m) :
    lift.{v'} (Module.rank R M) ≤ lift.{v} (Module.rank R' M') := by
  simp_rw [Module.rank, lift_iSup (bddAbove_range _)]
  exact ciSup_mono' (bddAbove_range _) fun ⟨s, h⟩ ↦
    ⟨⟨j '' s, LinearIndepOn.id_image <| h.linearIndependent.map_of_injective_injective i j hi
      (fun _ _ ↦ hj <| by rwa [j.map_zero]) hc⟩,
    lift_mk_le'.mpr ⟨(Equiv.Set.image j s hj).toEmbedding⟩⟩
Rank Inequality for Injective Module Homomorphisms with Compatible Scalar Multiplication
Informal description
Let $M$ be a module over a ring $R$ and $M'$ a module over a ring $R'$. Suppose $i : R' \to R$ is a map that sends non-zero elements to non-zero elements, and $j : M \to M'$ is an injective group homomorphism such that the scalar multiplications are compatible, i.e., for all $r \in R'$ and $m \in M$, we have $j(i(r) \cdot m) = r \cdot j(m)$. Then the rank of $M$ over $R$ is less than or equal to the rank of $M'$ over $R'$.
rank_le_of_injective_injective theorem
[AddCommGroup M₁] [Module R' M₁] (i : R' → R) (j : M →+ M₁) (hi : ∀ r, i r = 0 → r = 0) (hj : Injective j) (hc : ∀ (r : R') (m : M), j (i r • m) = r • j m) : Module.rank R M ≤ Module.rank R' M₁
Full source 
/-- The same-universe version of `lift_rank_le_of_injective_injective`. -/
theorem rank_le_of_injective_injective [AddCommGroup M₁] [Module R' M₁]
    (i : R' → R) (j : M →+ M₁) (hi : ∀ r, i r = 0 → r = 0) (hj : Injective j)
    (hc : ∀ (r : R') (m : M), j (i r • m) = r • j m) :
    Module.rank R M ≤ Module.rank R' M₁ := by
  simpa only [lift_id] using lift_rank_le_of_injective_injective i j hi hj hc
Rank Inequality for Injective Module Homomorphisms with Compatible Scalar Multiplication (Same Universe)
Informal description
Let $M$ be a module over a ring $R$ and $M_1$ a module over a ring $R'$. Suppose $i : R' \to R$ is a map that sends non-zero elements to non-zero elements, and $j : M \to M_1$ is an injective group homomorphism such that the scalar multiplications are compatible, i.e., for all $r \in R'$ and $m \in M$, we have $j(i(r) \cdot m) = r \cdot j(m)$. Then the rank of $M$ over $R$ is less than or equal to the rank of $M_1$ over $R'$.
Algebra.lift_rank_le_of_injective_injective theorem
(i : R' →+* R) (j : S →+* S') (hi : Injective i) (hj : Injective j) (hc : (j.comp (algebraMap R S)).comp i = algebraMap R' S') : lift.{v'} (Module.rank R S) ≤ lift.{v} (Module.rank R' S')
Full source 
/-- If `S / R` and `S' / R'` are algebras, `i : R' →+* R` and `j : S →+* S'` are injective ring
homomorphisms, such that `R' → R → S → S'` and `R' → S'` commute, then the rank of `S / R` is
smaller than or equal to the rank of `S' / R'`. -/
theorem lift_rank_le_of_injective_injective
    (i : R' →+* R) (j : S →+* S') (hi : Injective i) (hj : Injective j)
    (hc : (j.comp (algebraMap R S)).comp i = algebraMap R' S') :
    lift.{v'} (Module.rank R S) ≤ lift.{v} (Module.rank R' S') := by
  refine _root_.lift_rank_le_of_injective_injectiveₛ i j hi hj fun r _ ↦ ?_
  have := congr($hc r)
  simp only [RingHom.coe_comp, comp_apply] at this
  simp_rw [smul_def, AddMonoidHom.coe_coe, map_mul, this]
Rank Inequality for Algebras with Injective Homomorphisms
Informal description
Let $R$ and $R'$ be rings, and let $S$ be an $R$-algebra and $S'$ an $R'$-algebra. Suppose there exist injective ring homomorphisms $i: R' \to R$ and $j: S \to S'$ such that the following diagram commutes: \[ \begin{CD} R' @>{i}>> R \\ @V{\text{algebraMap } R' S'}VV @VV{\text{algebraMap } R S}V \\ S' @<{j}<< S \end{CD} \] Then the rank of $S$ as an $R$-module is less than or equal to the rank of $S'$ as an $R'$-module.
Algebra.lift_rank_le_of_surjective_injective theorem
(i : R →+* R') (j : S →+* S') (hi : Surjective i) (hj : Injective j) (hc : (algebraMap R' S').comp i = j.comp (algebraMap R S)) : lift.{v'} (Module.rank R S) ≤ lift.{v} (Module.rank R' S')
Full source 
/-- If `S / R` and `S' / R'` are algebras, `i : R →+* R'` is a surjective ring homomorphism,
`j : S →+* S'` is an injective ring homomorphism, such that `R → R' → S'` and `R → S → S'` commute,
then the rank of `S / R` is smaller than or equal to the rank of `S' / R'`. -/
theorem lift_rank_le_of_surjective_injective
    (i : R →+* R') (j : S →+* S') (hi : Surjective i) (hj : Injective j)
    (hc : (algebraMap R' S').comp i = j.comp (algebraMap R S)) :
    lift.{v'} (Module.rank R S) ≤ lift.{v} (Module.rank R' S') := by
  refine _root_.lift_rank_le_of_surjective_injective i j hi hj fun r _ ↦ ?_
  have := congr($hc r)
  simp only [RingHom.coe_comp, comp_apply] at this
  simp only [smul_def, AddMonoidHom.coe_coe, map_mul, ZeroHom.coe_coe, this]
Rank Inequality for Algebras under Surjective Base Change and Injective Extension
Informal description
Let $R$ and $R'$ be rings, and let $S$ be an $R$-algebra and $S'$ an $R'$-algebra. Suppose there exist a surjective ring homomorphism $i: R \to R'$ and an injective ring homomorphism $j: S \to S'$ such that the following diagram commutes: \[ \begin{CD} R @>{i}>> R' \\ @V{\text{algebraMap } R S}VV @VV{\text{algebraMap } R' S'}V \\ S @>{j}>> S' \end{CD} \] Then the rank of $S$ as an $R$-module is less than or equal to the rank of $S'$ as an $R'$-module.
Algebra.lift_rank_eq_of_equiv_equiv theorem
(i : R ≃+* R') (j : S ≃+* S') (hc : (algebraMap R' S').comp i.toRingHom = j.toRingHom.comp (algebraMap R S)) : lift.{v'} (Module.rank R S) = lift.{v} (Module.rank R' S')
Full source 
/-- If `S / R` and `S' / R'` are algebras, `i : R ≃+* R'` and `j : S ≃+* S'` are
ring isomorphisms, such that `R → R' → S'` and `R → S → S'` commute,
then the rank of `S / R` is equal to the rank of `S' / R'`. -/
theorem lift_rank_eq_of_equiv_equiv (i : R ≃+* R') (j : S ≃+* S')
    (hc : (algebraMap R' S').comp i.toRingHom = j.toRingHom.comp (algebraMap R S)) :
    lift.{v'} (Module.rank R S) = lift.{v} (Module.rank R' S') := by
  refine _root_.lift_rank_eq_of_equiv_equiv i j i.bijective fun r _ ↦ ?_
  have := congr($hc r)
  simp only [RingEquiv.toRingHom_eq_coe, RingHom.coe_comp, RingHom.coe_coe, comp_apply] at this
  simp only [smul_def, RingEquiv.coe_toAddEquiv, map_mul, ZeroHom.coe_coe, this]
Rank Equality for Algebras under Ring Isomorphisms
Informal description
Let $R$ and $R'$ be rings, and let $S$ be an $R$-algebra and $S'$ an $R'$-algebra. Suppose there exist ring isomorphisms $i: R \simeq^+ R'$ and $j: S \simeq^+ S'$ such that the following diagram commutes: \[ \begin{CD} R @>{i}>> R' \\ @V{\text{algebraMap } R S}VV @VV{\text{algebraMap } R' S'}V \\ S @>{j}>> S' \end{CD} \] Then the rank of $S$ as an $R$-module is equal to the rank of $S'$ as an $R'$-module.
Algebra.rank_le_of_injective_injective theorem
(i : R' →+* R) (j : S →+* S') (hi : Injective i) (hj : Injective j) (hc : (j.comp (algebraMap R S)).comp i = algebraMap R' S') : Module.rank R S ≤ Module.rank R' S'
Full source 
/-- The same-universe version of `Algebra.lift_rank_le_of_injective_injective`. -/
theorem rank_le_of_injective_injective
    (i : R' →+* R) (j : S →+* S') (hi : Injective i) (hj : Injective j)
    (hc : (j.comp (algebraMap R S)).comp i = algebraMap R' S') :
    Module.rank R S ≤ Module.rank R' S' := by
  simpa only [lift_id] using lift_rank_le_of_injective_injective i j hi hj hc
Rank Inequality for Algebras with Injective Homomorphisms (Same Universe)
Informal description
Let $R$ and $R'$ be rings, and let $S$ be an $R$-algebra and $S'$ an $R'$-algebra. Suppose there exist injective ring homomorphisms $i: R' \to R$ and $j: S \to S'$ such that the following diagram commutes: \[ \begin{CD} R' @>{i}>> R \\ @V{\text{algebraMap } R' S'}VV @VV{\text{algebraMap } R S}V \\ S' @<{j}<< S \end{CD} \] Then the rank of $S$ as an $R$-module is less than or equal to the rank of $S'$ as an $R'$-module.
Algebra.rank_le_of_surjective_injective theorem
(i : R →+* R') (j : S →+* S') (hi : Surjective i) (hj : Injective j) (hc : (algebraMap R' S').comp i = j.comp (algebraMap R S)) : Module.rank R S ≤ Module.rank R' S'
Full source 
/-- The same-universe version of `Algebra.lift_rank_le_of_surjective_injective`. -/
theorem rank_le_of_surjective_injective
    (i : R →+* R') (j : S →+* S') (hi : Surjective i) (hj : Injective j)
    (hc : (algebraMap R' S').comp i = j.comp (algebraMap R S)) :
    Module.rank R S ≤ Module.rank R' S' := by
  simpa only [lift_id] using lift_rank_le_of_surjective_injective i j hi hj hc
Rank Inequality for Algebras under Surjective Base Change and Injective Extension (Same Universe)
Informal description
Let $R$ and $R'$ be rings, and let $S$ be an $R$-algebra and $S'$ an $R'$-algebra. Given a surjective ring homomorphism $i \colon R \to R'$ and an injective ring homomorphism $j \colon S \to S'$ such that the following diagram commutes: \[ \begin{CD} R @>{i}>> R' \\ @V{\text{algebraMap } R S}VV @VV{\text{algebraMap } R' S'}V \\ S @>{j}>> S' \end{CD} \] then the rank of $S$ as an $R$-module is less than or equal to the rank of $S'$ as an $R'$-module.
Algebra.rank_eq_of_equiv_equiv theorem
(i : R ≃+* R') (j : S ≃+* S') (hc : (algebraMap R' S').comp i.toRingHom = j.toRingHom.comp (algebraMap R S)) : Module.rank R S = Module.rank R' S'
Full source 
/-- The same-universe version of `Algebra.lift_rank_eq_of_equiv_equiv`. -/
theorem rank_eq_of_equiv_equiv (i : R ≃+* R') (j : S ≃+* S')
    (hc : (algebraMap R' S').comp i.toRingHom = j.toRingHom.comp (algebraMap R S)) :
    Module.rank R S = Module.rank R' S' := by
  simpa only [lift_id] using lift_rank_eq_of_equiv_equiv i j hc
Rank Equality for Algebras under Ring Isomorphisms (Same Universe)
Informal description
Let $R$ and $R'$ be rings, and let $S$ be an $R$-algebra and $S'$ an $R'$-algebra. Suppose there exist ring isomorphisms $i: R \simeq^+ R'$ and $j: S \simeq^+ S'$ such that the following diagram commutes: \[ \begin{CD} R @>{i}>> R' \\ @V{\text{algebraMap } R S}VV @VV{\text{algebraMap } R' S'}V \\ S @>{j}>> S' \end{CD} \] Then the rank of $S$ as an $R$-module is equal to the rank of $S'$ as an $R'$-module.
LinearMap.lift_rank_le_of_injective theorem
(f : M →ₗ[R] M') (i : Injective f) : Cardinal.lift.{v'} (Module.rank R M) ≤ Cardinal.lift.{v} (Module.rank R M')
Full source 
theorem LinearMap.lift_rank_le_of_injective (f : M →ₗ[R] M') (i : Injective f) :
    Cardinal.lift.{v'} (Module.rank R M) ≤ Cardinal.lift.{v} (Module.rank R M') :=
  lift_rank_le_of_injective_injectiveₛ (RingHom.id R) f (fun _ _ h ↦ h) i f.map_smul
Rank Inequality for Injective Linear Maps: $\text{rank}_R(M) \leq \text{rank}_R(M')$
Informal description
Let $R$ be a ring, and let $M$ and $M'$ be modules over $R$. Given an injective linear map $f \colon M \to M'$, the rank of $M$ is less than or equal to the rank of $M'$. More precisely, if $\text{rank}_R(M)$ denotes the rank of $M$ (i.e., the supremum of the cardinalities of its linearly independent subsets), then $\text{rank}_R(M) \leq \text{rank}_R(M')$.
LinearMap.rank_le_of_injective theorem
(f : M →ₗ[R] M₁) (i : Injective f) : Module.rank R M ≤ Module.rank R M₁
Full source 
theorem LinearMap.rank_le_of_injective (f : M →ₗ[R] M₁) (i : Injective f) :
    Module.rank R M ≤ Module.rank R M₁ :=
  Cardinal.lift_le.1 (f.lift_rank_le_of_injective i)
Rank Inequality for Injective Linear Maps: $\text{rank}_R(M) \leq \text{rank}_R(M_1)$
Informal description
Let $R$ be a ring, and let $M$ and $M_1$ be modules over $R$. If $f \colon M \to M_1$ is an injective linear map, then the rank of $M$ is less than or equal to the rank of $M_1$, i.e., $\text{rank}_R(M) \leq \text{rank}_R(M_1)$.
lift_rank_range_le theorem
(f : M →ₗ[R] M') : Cardinal.lift.{v} (Module.rank R (LinearMap.range f)) ≤ Cardinal.lift.{v'} (Module.rank R M)
Full source 
/-- The rank of the range of a linear map is at most the rank of the source. -/
-- The proof is: a free submodule of the range lifts to a free submodule of the
-- source, by arbitrarily lifting a basis.
theorem lift_rank_range_le (f : M →ₗ[R] M') : Cardinal.lift.{v}
    (Module.rank R (LinearMap.range f)) ≤ Cardinal.lift.{v'} (Module.rank R M) := by
  simp only [Module.rank_def]
  rw [Cardinal.lift_iSup (Cardinal.bddAbove_range _)]
  apply ciSup_le'
  rintro ⟨s, li⟩
  apply le_trans
  swap
  · apply Cardinal.lift_le.mpr
    refine le_ciSup (Cardinal.bddAbove_range _) ⟨rangeSplitting f '' s, ?_⟩
    apply LinearIndependent.of_comp f.rangeRestrict
    convert li.comp (Equiv.Set.rangeSplittingImageEquiv f s) (Equiv.injective _) using 1
  · exact (Cardinal.lift_mk_eq'.mpr ⟨Equiv.Set.rangeSplittingImageEquiv f s⟩).ge
Rank of Range is Bounded by Rank of Source Module
Informal description
For any linear map $f \colon M \to M'$ between modules over a ring $R$, the rank of the range of $f$ is at most the rank of the source module $M$. More precisely, if $\text{rank}_R(M)$ denotes the rank of $M$ (i.e., the supremum of the cardinalities of its linearly independent subsets), then $\text{rank}_R(\text{range}(f)) \leq \text{rank}_R(M)$.
rank_range_le theorem
(f : M →ₗ[R] M₁) : Module.rank R (LinearMap.range f) ≤ Module.rank R M
Full source 
theorem rank_range_le (f : M →ₗ[R] M₁) : Module.rank R (LinearMap.range f) ≤ Module.rank R M := by
  simpa using lift_rank_range_le f
Rank of Range is Bounded by Rank of Source Module
Informal description
For any linear map $f \colon M \to M_1$ between modules over a ring $R$, the rank of the range of $f$ is at most the rank of the source module $M$. More precisely, if $\text{rank}_R(M)$ denotes the rank of $M$ (i.e., the supremum of the cardinalities of its linearly independent subsets), then $\text{rank}_R(\text{range}(f)) \leq \text{rank}_R(M)$.
lift_rank_map_le theorem
(f : M →ₗ[R] M') (p : Submodule R M) : Cardinal.lift.{v} (Module.rank R (p.map f)) ≤ Cardinal.lift.{v'} (Module.rank R p)
Full source 
theorem lift_rank_map_le (f : M →ₗ[R] M') (p : Submodule R M) :
    Cardinal.lift.{v} (Module.rank R (p.map f)) ≤ Cardinal.lift.{v'} (Module.rank R p) := by
  have h := lift_rank_range_le (f.comp (Submodule.subtype p))
  rwa [LinearMap.range_comp, range_subtype] at h
Rank of Submodule Image is Bounded by Rank of Submodule
Informal description
For any linear map $f \colon M \to M'$ between modules over a ring $R$ and any submodule $p$ of $M$, the rank of the image of $p$ under $f$ is at most the rank of $p$. More precisely, if $\text{rank}_R(p)$ denotes the rank of $p$ (i.e., the supremum of the cardinalities of its linearly independent subsets), then $\text{rank}_R(f(p)) \leq \text{rank}_R(p)$.
rank_map_le theorem
(f : M →ₗ[R] M₁) (p : Submodule R M) : Module.rank R (p.map f) ≤ Module.rank R p
Full source 
theorem rank_map_le (f : M →ₗ[R] M₁) (p : Submodule R M) :
    Module.rank R (p.map f) ≤ Module.rank R p := by simpa using lift_rank_map_le f p
Rank Inequality for Submodule Image: $\text{rank}_R(f(p)) \leq \text{rank}_R(p)$
Informal description
For any linear map $f \colon M \to M_1$ between modules over a ring $R$ and any submodule $p$ of $M$, the rank of the image of $p$ under $f$ is at most the rank of $p$. In other words, if $\text{rank}_R(p)$ denotes the rank of $p$ (i.e., the supremum of the cardinalities of its linearly independent subsets), then $\text{rank}_R(f(p)) \leq \text{rank}_R(p)$.
Submodule.rank_mono theorem
{s t : Submodule R M} (h : s ≤ t) : Module.rank R s ≤ Module.rank R t
Full source 
lemma Submodule.rank_mono {s t : Submodule R M} (h : s ≤ t) : Module.rank R s ≤ Module.rank R t :=
  (Submodule.inclusion h).rank_le_of_injective fun ⟨x, _⟩ ⟨y, _⟩ eq =>
    Subtype.eq <| show x = y from Subtype.ext_iff_val.1 eq
Monotonicity of Rank for Submodules: $s \leq t \implies \text{rank}_R(s) \leq \text{rank}_R(t)$
Informal description
For any submodules $s$ and $t$ of a module $M$ over a ring $R$, if $s$ is contained in $t$ (i.e., $s \leq t$), then the rank of $s$ is less than or equal to the rank of $t$, i.e., $\text{rank}_R(s) \leq \text{rank}_R(t)$.
LinearEquiv.lift_rank_eq theorem
(f : M ≃ₗ[R] M') : Cardinal.lift.{v'} (Module.rank R M) = Cardinal.lift.{v} (Module.rank R M')
Full source 
/-- Two linearly equivalent vector spaces have the same dimension, a version with different
universes. -/
theorem LinearEquiv.lift_rank_eq (f : M ≃ₗ[R] M') :
    Cardinal.lift.{v'} (Module.rank R M) = Cardinal.lift.{v} (Module.rank R M') := by
  apply le_antisymm
  · exact f.toLinearMap.lift_rank_le_of_injective f.injective
  · exact f.symm.toLinearMap.lift_rank_le_of_injective f.symm.injective
Rank Preservation under Linear Equivalence: $\text{rank}_R(M) = \text{rank}_R(M')$
Informal description
Let $R$ be a ring, and let $M$ and $M'$ be modules over $R$ (possibly in different universe levels). If $f \colon M \to M'$ is a linear equivalence, then the rank of $M$ is equal to the rank of $M'$. More precisely, if $\text{rank}_R(M)$ denotes the rank of $M$ (i.e., the supremum of the cardinalities of its linearly independent subsets), then $\text{rank}_R(M) = \text{rank}_R(M')$.
LinearEquiv.rank_eq theorem
(f : M ≃ₗ[R] M₁) : Module.rank R M = Module.rank R M₁
Full source 
/-- Two linearly equivalent vector spaces have the same dimension. -/
theorem LinearEquiv.rank_eq (f : M ≃ₗ[R] M₁) : Module.rank R M = Module.rank R M₁ :=
  Cardinal.lift_inj.1 f.lift_rank_eq
Rank Equality under Linear Equivalence: $\text{rank}_R(M) = \text{rank}_R(M_1)$
Informal description
Let $R$ be a ring, and let $M$ and $M_1$ be modules over $R$ (in the same universe level). If $f \colon M \to M_1$ is a linear equivalence, then the rank of $M$ is equal to the rank of $M_1$, i.e., $\text{rank}_R(M) = \text{rank}_R(M_1)$.
lift_rank_range_of_injective theorem
(f : M →ₗ[R] M') (h : Injective f) : lift.{v} (Module.rank R (LinearMap.range f)) = lift.{v'} (Module.rank R M)
Full source 
theorem lift_rank_range_of_injective (f : M →ₗ[R] M') (h : Injective f) :
    lift.{v} (Module.rank R (LinearMap.range f)) = lift.{v'} (Module.rank R M) :=
  (LinearEquiv.ofInjective f h).lift_rank_eq.symm
Rank Preservation under Injective Linear Maps: $\text{rank}_R(\text{range}(f)) = \text{rank}_R(M)$
Informal description
Let $R$ be a ring, and let $M$ and $M'$ be $R$-modules (possibly in different universe levels). If $f \colon M \to M'$ is an injective linear map, then the rank of the range of $f$ is equal to the rank of $M$. More precisely, if $\text{rank}_R(M)$ denotes the rank of $M$ (i.e., the supremum of the cardinalities of its linearly independent subsets), then $\text{rank}_R(\text{range}(f)) = \text{rank}_R(M)$.
rank_range_of_injective theorem
(f : M →ₗ[R] M₁) (h : Injective f) : Module.rank R (LinearMap.range f) = Module.rank R M
Full source 
theorem rank_range_of_injective (f : M →ₗ[R] M₁) (h : Injective f) :
    Module.rank R (LinearMap.range f) = Module.rank R M :=
  (LinearEquiv.ofInjective f h).rank_eq.symm
Rank Preservation under Injective Linear Maps: $\text{rank}_R(\text{range}(f)) = \text{rank}_R(M)$
Informal description
Let $R$ be a ring, and let $M$ and $M_1$ be $R$-modules. If $f \colon M \to M_1$ is an injective linear map, then the rank of the range of $f$ is equal to the rank of $M$, i.e., $\text{rank}_R(\text{range}(f)) = \text{rank}_R(M)$.
LinearEquiv.lift_rank_map_eq theorem
(f : M ≃ₗ[R] M') (p : Submodule R M) : lift.{v} (Module.rank R (p.map (f : M →ₗ[R] M'))) = lift.{v'} (Module.rank R p)
Full source 
theorem LinearEquiv.lift_rank_map_eq (f : M ≃ₗ[R] M') (p : Submodule R M) :
    lift.{v} (Module.rank R (p.map (f : M →ₗ[R] M'))) = lift.{v'} (Module.rank R p) :=
  (f.submoduleMap p).lift_rank_eq.symm
Rank Preservation under Linear Equivalence of Submodules: $\text{rank}_R(f(p)) = \text{rank}_R(p)$
Informal description
Let $R$ be a ring, and let $M$ and $M'$ be modules over $R$ (possibly in different universe levels). Given a linear equivalence $f \colon M \to M'$ and a submodule $p \subseteq M$, the rank of the image submodule $f(p)$ is equal to the rank of $p$. More precisely, if $\text{rank}_R(p)$ denotes the rank of $p$ (i.e., the supremum of the cardinalities of its linearly independent subsets), then $\text{rank}_R(f(p)) = \text{rank}_R(p)$.
LinearEquiv.rank_map_eq theorem
(f : M ≃ₗ[R] M₁) (p : Submodule R M) : Module.rank R (p.map (f : M →ₗ[R] M₁)) = Module.rank R p
Full source 
/-- Pushforwards of submodules along a `LinearEquiv` have the same dimension. -/
theorem LinearEquiv.rank_map_eq (f : M ≃ₗ[R] M₁) (p : Submodule R M) :
    Module.rank R (p.map (f : M →ₗ[R] M₁)) = Module.rank R p :=
  (f.submoduleMap p).rank_eq.symm
Rank Preservation under Linear Equivalence of Submodules: $\text{rank}_R(f(p)) = \text{rank}_R(p)$
Informal description
Let $R$ be a ring, and let $M$ and $M_1$ be modules over $R$. Given a linear equivalence $f \colon M \to M_1$ and a submodule $p \subseteq M$, the rank of the image submodule $f(p)$ is equal to the rank of $p$, i.e., $\text{rank}_R(f(p)) = \text{rank}_R(p)$.
rank_top theorem
: Module.rank R (⊤ : Submodule R M) = Module.rank R M
Full source 
@[simp]
theorem rank_top : Module.rank R (⊤ : Submodule R M) = Module.rank R M :=
  (LinearEquiv.ofTop ⊤ rfl).rank_eq
Rank of Top Submodule Equals Rank of Module: $\text{rank}_R(\top) = \text{rank}_R(M)$
Informal description
The rank of the top submodule of a module $M$ over a ring $R$ is equal to the rank of $M$ itself, i.e., $\text{rank}_R(\top) = \text{rank}_R(M)$.
rank_range_of_surjective theorem
(f : M →ₗ[R] M') (h : Surjective f) : Module.rank R (LinearMap.range f) = Module.rank R M'
Full source 
theorem rank_range_of_surjective (f : M →ₗ[R] M') (h : Surjective f) :
    Module.rank R (LinearMap.range f) = Module.rank R M' := by
  rw [LinearMap.range_eq_top.2 h, rank_top]
Rank of Range Equals Rank of Codomain for Surjective Linear Maps
Informal description
For a surjective linear map $f \colon M \to M'$ of modules over a ring $R$, the rank of the range of $f$ is equal to the rank of $M'$, i.e., $\text{rank}_R(\text{range}(f)) = \text{rank}_R(M')$.
Submodule.rank_le theorem
(s : Submodule R M) : Module.rank R s ≤ Module.rank R M
Full source 
theorem Submodule.rank_le (s : Submodule R M) : Module.rank R s ≤ Module.rank R M := by
  rw [← rank_top R M]
  exact rank_mono le_top
Submodule Rank Bound: $\text{rank}_R(s) \leq \text{rank}_R(M)$
Informal description
For any submodule $s$ of a module $M$ over a ring $R$, the rank of $s$ is less than or equal to the rank of $M$, i.e., $\text{rank}_R(s) \leq \text{rank}_R(M)$.
LinearMap.lift_rank_le_of_surjective theorem
(f : M →ₗ[R] M') (h : Surjective f) : lift.{v} (Module.rank R M') ≤ lift.{v'} (Module.rank R M)
Full source 
theorem LinearMap.lift_rank_le_of_surjective (f : M →ₗ[R] M') (h : Surjective f) :
    lift.{v} (Module.rank R M') ≤ lift.{v'} (Module.rank R M) := by
  rw [← rank_range_of_surjective f h]
  apply lift_rank_range_le
Rank Inequality for Surjective Linear Maps: $\text{rank}(M') \leq \text{rank}(M)$
Informal description
For any surjective linear map $f \colon M \to M'$ between modules over a ring $R$, the rank of $M'$ is at most the rank of $M$. More precisely, if $\text{rank}_R(M)$ and $\text{rank}_R(M')$ denote the ranks of $M$ and $M'$ respectively (i.e., the suprema of the cardinalities of their linearly independent subsets), then $\text{rank}_R(M') \leq \text{rank}_R(M)$.
LinearMap.rank_le_of_surjective theorem
(f : M →ₗ[R] M₁) (h : Surjective f) : Module.rank R M₁ ≤ Module.rank R M
Full source 
theorem LinearMap.rank_le_of_surjective (f : M →ₗ[R] M₁) (h : Surjective f) :
    Module.rank R M₁ ≤ Module.rank R M := by
  rw [← rank_range_of_surjective f h]
  apply rank_range_le
Rank Inequality for Surjective Linear Maps: $\text{rank}_R(M_1) \leq \text{rank}_R(M)$
Informal description
For any surjective linear map $f \colon M \to M_1$ between modules over a ring $R$, the rank of the target module $M_1$ is at most the rank of the source module $M$, i.e., $\text{rank}_R(M_1) \leq \text{rank}_R(M)$.
rank_subsingleton theorem
[Subsingleton R] : Module.rank R M = 1
Full source 
@[nontriviality, simp]
theorem rank_subsingleton [Subsingleton R] : Module.rank R M = 1 := by
  haveI := Module.subsingleton R M
  have : Nonempty { s : Set M // LinearIndepOn R id s} := ⟨⟨∅, linearIndepOn_empty _ _⟩⟩
  rw [Module.rank_def, ciSup_eq_of_forall_le_of_forall_lt_exists_gt]
  · rintro ⟨s, hs⟩
    rw [Cardinal.mk_le_one_iff_set_subsingleton]
    apply subsingleton_of_subsingleton
  intro w hw
  exact ⟨⟨{0}, LinearIndepOn.of_subsingleton⟩, hw.trans_eq (Cardinal.mk_singleton _).symm⟩
Rank of Module over Subsingleton Ring is One
Informal description
If the ring $R$ is a subsingleton (i.e., has at most one element), then the rank of any module $M$ over $R$ is equal to $1$.
rank_le_of_isSMulRegular theorem
{S : Type*} [CommSemiring S] [Algebra S R] [Module S M] [IsScalarTower S R M] (L L' : Submodule R M) {s : S} (hr : IsSMulRegular M s) (h : ∀ x ∈ L, s • x ∈ L') : Module.rank R L ≤ Module.rank R L'
Full source 
lemma rank_le_of_isSMulRegular {S : Type*} [CommSemiring S] [Algebra S R] [Module S M]
    [IsScalarTower S R M] (L L' : Submodule R M) {s : S} (hr : IsSMulRegular M s)
    (h : ∀ x ∈ L, s • x ∈ L') :
    Module.rank R L ≤ Module.rank R L' :=
  ((Algebra.lsmul S R M s).restrict h).rank_le_of_injective <|
    fun _ _ h ↦ by simpa using hr (Subtype.ext_iff.mp h)
Rank Inequality for Submodules under Regular Scalar Multiplication: $\text{rank}_R(L) \leq \text{rank}_R(L')$
Informal description
Let $R$ be a ring, $S$ a commutative semiring with an algebra structure over $R$, and $M$ a module over $R$ and $S$ such that the scalar multiplication is compatible via the `IsScalarTower` condition. Let $L$ and $L'$ be submodules of $M$ over $R$, and let $s \in S$ be an element that is left-regular for the scalar multiplication on $M$ (i.e., $s \cdot x = 0$ implies $x = 0$ for all $x \in M$). If for every $x \in L$, we have $s \cdot x \in L'$, then the rank of $L$ is less than or equal to the rank of $L'$, i.e., $\text{rank}_R(L) \leq \text{rank}_R(L')$.