Mathlib.LinearAlgebra.Dimension.Constructions

LinearIndependent.sumElim_of_quotient theorem

 {M' : Submodule R M} {ι₁ ι₂} {f : ι₁ → M'} (hf : LinearIndependent R f) (g : ι₂ → M)
  (hg : LinearIndependent R (Submodule.Quotient.mk (p := M') ∘ g)) : LinearIndependent R (Sum.elim (f · : ι₁ → M) g)

Full source

theorem LinearIndependent.sumElim_of_quotient
    {M' : Submodule R M} {ι₁ ι₂} {f : ι₁ → M'} (hf : LinearIndependent R f) (g : ι₂ → M)
    (hg : LinearIndependent R (Submodule.Quotient.mkSubmodule.Quotient.mk (p := M') ∘ g)) :
    LinearIndependent R (Sum.elim (f · : ι₁ → M) g) := by
  refine .sum_type (hf.map' M'.subtype M'.ker_subtype) (.of_comp M'.mkQ hg) ?_
  refine disjoint_def.mpr fun x h₁ h₂ ↦ ?_
  have : x ∈ M' := span_le.mpr (Set.range_subset_iff.mpr fun i ↦ (f i).prop) h₁
  obtain ⟨c, rfl⟩ := Finsupp.mem_span_range_iff_exists_finsupp.mp h₂
  simp_rw [← Quotient.mk_eq_zero, ← mkQ_apply, map_finsuppSum, map_smul, mkQ_apply] at this
  rw [linearIndependent_iff.mp hg _ this, Finsupp.sum_zero_index]

Linear Independence of Combined Functions Under Quotient Condition

Informal description

Let $R$ be a ring, $M$ an $R$-module, and $M'$ a submodule of $M$. Given two index sets $\iota_1$ and $\iota_2$, a function $f: \iota_1 \to M'$ that is linearly independent over $R$, and a function $g: \iota_2 \to M$ such that the composition of $g$ with the quotient map $M \to M/M'$ is linearly independent over $R$, then the combined function $\text{Sum.elim}(f, g): \iota_1 \oplus \iota_2 \to M$ is linearly independent over $R$.

LinearIndepOn.union_of_quotient theorem

 {s t : Set ι} {f : ι → M} (hs : LinearIndepOn R f s) (ht : LinearIndepOn R (mkQ (span R (f '' s)) ∘ f) t) :
  LinearIndepOn R f (s ∪ t)

Full source

theorem LinearIndepOn.union_of_quotient {s t : Set ι} {f : ι → M} (hs : LinearIndepOn R f s)
    (ht : LinearIndepOn R (mkQmkQ (span R (f '' s)) ∘ f) t) : LinearIndepOn R f (s ∪ t) := by
  apply hs.union ht.of_comp
  convert (Submodule.range_ker_disjoint ht).symm
  · simp
  aesop

Linear Independence of Union under Quotient Condition

Informal description

Let $R$ be a ring, $M$ an $R$-module, and $f : \iota \to M$ a function. For any subsets $s, t \subseteq \iota$, if $f$ is linearly independent on $s$ and the composition of $f$ with the quotient map $M \to M/\text{span}_R(f(s))$ is linearly independent on $t$, then $f$ is linearly independent on the union $s \cup t$.

LinearIndepOn.union_id_of_quotient theorem

 {M' : Submodule R M} {s : Set M} (hs : s ⊆ M') (hs' : LinearIndepOn R id s) {t : Set M}
  (ht : LinearIndepOn R (mkQ M') t) : LinearIndepOn R id (s ∪ t)

Full source

theorem LinearIndepOn.union_id_of_quotient {M' : Submodule R M}
    {s : Set M} (hs : s ⊆ M') (hs' : LinearIndepOn R id s) {t : Set M}
    (ht : LinearIndepOn R (mkQ M') t) : LinearIndepOn R id (s ∪ t) :=
  hs'.union_of_quotient <| by
    rw [image_id]
    exact ht.of_comp ((span R s).mapQ M' (LinearMap.id) (span_le.2 hs))

Linear Independence of Union via Quotient Condition for Identity Map

Informal description

Let $R$ be a ring, $M$ an $R$-module, and $M'$ a submodule of $M$. For any subset $s \subseteq M$ contained in $M'$, if the identity map is linearly independent on $s$ and the quotient map $M \to M/M'$ is linearly independent on another subset $t \subseteq M$, then the identity map is linearly independent on the union $s \cup t$.

linearIndepOn_union_iff_quotient theorem

 {s t : Set ι} {f : ι → M} (hst : Disjoint s t) :
  LinearIndepOn R f (s ∪ t) ↔ LinearIndepOn R f s ∧ LinearIndepOn R (mkQ (span R (f '' s)) ∘ f) t

Full source

theorem linearIndepOn_union_iff_quotient {s t : Set ι} {f : ι → M} (hst : Disjoint s t) :
    LinearIndepOnLinearIndepOn R f (s ∪ t) ↔
    LinearIndepOn R f s ∧ LinearIndepOn R (mkQ (span R (f '' s)) ∘ f) t := by
  refine ⟨fun h ↦ ⟨?_, ?_⟩, fun h ↦ h.1.union_of_quotient h.2⟩
  · exact h.mono subset_union_left
  apply (h.mono subset_union_right).map
  simpa [← image_eq_range] using ((linearIndepOn_union_iff hst).1 h).2.2.symm

Linear Independence of Union via Quotient Criterion for Disjoint Sets

Informal description

Let $R$ be a ring, $M$ an $R$-module, and $f : \iota \to M$ a function. For any disjoint subsets $s, t \subseteq \iota$, the function $f$ is linearly independent on $s \cup t$ if and only if $f$ is linearly independent on $s$ and the composition of $f$ with the quotient map $M \to M/\text{span}_R(f(s))$ is linearly independent on $t$.

LinearIndepOn.quotient_iff_union theorem

 {s t : Set ι} {f : ι → M} (hs : LinearIndepOn R f s) (hst : Disjoint s t) :
  LinearIndepOn R (mkQ (span R (f '' s)) ∘ f) t ↔ LinearIndepOn R f (s ∪ t)

Full source

theorem LinearIndepOn.quotient_iff_union {s t : Set ι} {f : ι → M} (hs : LinearIndepOn R f s)
    (hst : Disjoint s t) :
    LinearIndepOnLinearIndepOn R (mkQ (span R (f '' s)) ∘ f) t ↔ LinearIndepOn R f (s ∪ t) := by
  rw [linearIndepOn_union_iff_quotient hst, and_iff_right hs]

Linear Independence of Quotient Composition on Disjoint Union

Informal description

Let $R$ be a ring, $M$ an $R$-module, and $f : \iota \to M$ a function. Given a subset $s \subseteq \iota$ such that $f$ is linearly independent on $s$, and a subset $t \subseteq \iota$ disjoint from $s$, the composition of $f$ with the quotient map $M \to M/\text{span}_R(f(s))$ is linearly independent on $t$ if and only if $f$ is linearly independent on the union $s \cup t$.

rank_quotient_add_rank_le theorem

[Nontrivial R] (M' : Submodule R M) : Module.rank R (M ⧸ M') + Module.rank R M' ≤ Module.rank R M

Full source

theorem rank_quotient_add_rank_le [Nontrivial R] (M' : Submodule R M) :
    Module.rank R (M ⧸ M') + Module.rank R M' ≤ Module.rank R M := by
  conv_lhs => simp only [Module.rank_def]
  have := nonempty_linearIndependent_set R (M ⧸ M')
  have := nonempty_linearIndependent_set R M'
  rw [Cardinal.ciSup_add_ciSup _ (bddAbove_range _) _ (bddAbove_range _)]
  refine ciSup_le fun ⟨s, hs⟩ ↦ ciSup_le fun ⟨t, ht⟩ ↦ ?_
  choose f hf using Submodule.Quotient.mk_surjective M'
  simpa [add_comm] using (LinearIndependent.sumElim_of_quotient ht (fun (i : s) ↦ f i)
    (by simpa [Function.comp_def, hf] using hs)).cardinal_le_rank

Rank Subadditivity for Module and Quotient: $\text{rank}_R(M/M') + \text{rank}_R(M') \leq \text{rank}_R(M)$

Informal description

Let $R$ be a nontrivial ring and $M$ an $R$-module with a submodule $M'$. Then the sum of the ranks of the quotient module $M/M'$ and the submodule $M'$ is less than or equal to the rank of $M$, i.e., \[ \text{rank}_R(M/M') + \text{rank}_R(M') \leq \text{rank}_R(M). \]

rank_quotient_le theorem

(p : Submodule R M) : Module.rank R (M ⧸ p) ≤ Module.rank R M

Full source

theorem rank_quotient_le (p : Submodule R M) : Module.rank R (M ⧸ p) ≤ Module.rank R M :=
  (mkQ p).rank_le_of_surjective Quot.mk_surjective

Rank Inequality for Quotient Module: $\text{rank}_R(M/p) \leq \text{rank}_R(M)$

Informal description

For any submodule $p$ of a module $M$ over a ring $R$, the rank of the quotient module $M/p$ is less than or equal to the rank of $M$, i.e., $\text{rank}_R(M/p) \leq \text{rank}_R(M)$.

Submodule.finrank_quotient_le theorem

[StrongRankCondition R] [Module.Finite R M] (s : Submodule R M) : finrank R (M ⧸ s) ≤ finrank R M

Full source

/-- The dimension of a quotient is bounded by the dimension of the ambient space. -/
theorem Submodule.finrank_quotient_le [StrongRankCondition R] [Module.Finite R M]
    (s : Submodule R M) : finrank R (M ⧸ s) ≤ finrank R M :=
  toNat_le_toNat ((Submodule.mkQ s).rank_le_of_surjective Quot.mk_surjective)
    (rank_lt_aleph0 _ _)

Finite Dimension Inequality for Quotient Module: $\text{finrank}_R(M/s) \leq \text{finrank}_R(M)$

Informal description

Let $R$ be a ring satisfying the strong rank condition, and let $M$ be a finite-dimensional module over $R$. For any submodule $s$ of $M$, the finite dimension of the quotient module $M/s$ is less than or equal to the finite dimension of $M$, i.e., $\text{finrank}_R(M/s) \leq \text{finrank}_R(M)$.

rank_ulift theorem

: Module.rank R (ULift.{w} M) = Cardinal.lift.{w} (Module.rank R M)

Full source

@[simp]
theorem rank_ulift : Module.rank R (ULift.{w} M) = Cardinal.lift.{w} (Module.rank R M) :=
  Cardinal.lift_injective.{v} <| Eq.symm <| (lift_lift _).trans ULift.moduleEquiv.symm.lift_rank_eq

Rank Preservation under ULift: $\text{rank}_R(\text{ULift}_{\omega} M) = \text{lift}_{\omega}(\text{rank}_R M)$

Informal description

The rank of the lifted module $\text{ULift}_{\omega} M$ over a ring $R$ is equal to the cardinal lift of the rank of $M$ over $R$, i.e., $\text{rank}_R(\text{ULift}_{\omega} M) = \text{lift}_{\omega}(\text{rank}_R M)$.

finrank_ulift theorem

: finrank R (ULift M) = finrank R M

Full source

@[simp]
theorem finrank_ulift : finrank R (ULift M) = finrank R M := by
  simp_rw [finrank, rank_ulift, toNat_lift]

Finite Dimension Preservation under ULift: $\text{finrank}_R(\text{ULift} M) = \text{finrank}_R M$

Informal description

The finite dimension of the lifted module $\text{ULift} M$ over a ring $R$ is equal to the finite dimension of $M$ over $R$, i.e., $\text{finrank}_R(\text{ULift} M) = \text{finrank}_R M$.

rank_add_rank_le_rank_prod theorem

[Nontrivial R] : Module.rank R M + Module.rank R M₁ ≤ Module.rank R (M × M₁)

Full source

theorem rank_add_rank_le_rank_prod [Nontrivial R] :
    Module.rank R M + Module.rank R M₁ ≤ Module.rank R (M × M₁) := by
  conv_lhs => simp only [Module.rank_def]
  have := nonempty_linearIndependent_set R M
  have := nonempty_linearIndependent_set R M₁
  rw [Cardinal.ciSup_add_ciSup _ (bddAbove_range _) _ (bddAbove_range _)]
  exact ciSup_le fun ⟨s, hs⟩ ↦ ciSup_le fun ⟨t, ht⟩ ↦
    (linearIndependent_inl_union_inr' hs ht).cardinal_le_rank

Rank Sum Bound for Direct Product of Modules: $\text{rank}_R M + \text{rank}_R M_1 \leq \text{rank}_R (M \times M_1)$

Informal description

For any nontrivial ring $R$ and $R$-modules $M$ and $M_1$, the sum of their ranks is less than or equal to the rank of their direct product, i.e., $\text{rank}_R M + \text{rank}_R M_1 \leq \text{rank}_R (M \times M_1)$.

lift_rank_add_lift_rank_le_rank_prod theorem

[Nontrivial R] : lift.{v'} (Module.rank R M) + lift.{v} (Module.rank R M') ≤ Module.rank R (M × M')

Full source

theorem lift_rank_add_lift_rank_le_rank_prod [Nontrivial R] :
    lift.{v'} (Module.rank R M) + lift.{v} (Module.rank R M') ≤ Module.rank R (M × M') := by
  rw [← rank_ulift, ← rank_ulift]
  exact (rank_add_rank_le_rank_prod R _).trans_eq
    (ULift.moduleEquiv.prodCongr ULift.moduleEquiv).rank_eq

Lifted Rank Sum Bound for Direct Product of Modules: $\text{lift}(\text{rank}_R M) + \text{lift}(\text{rank}_R M') \leq \text{rank}_R (M \times M')$

Informal description

For any nontrivial ring $R$ and $R$-modules $M$ and $M'$, the sum of the lifted ranks of $M$ and $M'$ is less than or equal to the rank of their direct product $M \times M'$. That is, $\text{lift}(\text{rank}_R M) + \text{lift}(\text{rank}_R M') \leq \text{rank}_R (M \times M')$.

rank_prod theorem

: Module.rank R (M × M') = Cardinal.lift.{v'} (Module.rank R M) + Cardinal.lift.{v, v'} (Module.rank R M')

Full source

/-- If `M` and `M'` are free, then the rank of `M × M'` is
`(Module.rank R M).lift + (Module.rank R M').lift`. -/
@[simp]
theorem rank_prod : Module.rank R (M × M') =
    Cardinal.lift.{v'} (Module.rank R M) + Cardinal.lift.{v, v'} (Module.rank R M') := by
  simpa [rank_eq_card_chooseBasisIndex R M, rank_eq_card_chooseBasisIndex R M', lift_umax]
    using ((chooseBasis R M).prod (chooseBasis R M')).mk_eq_rank.symm

Rank of Direct Product of Free Modules Equals Sum of Ranks

Informal description

For free modules $M$ and $M'$ over a ring $R$, the rank of their direct product $M \times M'$ is equal to the sum of the ranks of $M$ and $M'$, where the ranks are lifted to a common universe level. That is, $\text{rank}_R (M \times M') = \text{lift}(\text{rank}_R M) + \text{lift}(\text{rank}_R M')$.

rank_prod' theorem

: Module.rank R (M × M₁) = Module.rank R M + Module.rank R M₁

Full source

/-- If `M` and `M'` are free (and lie in the same universe), the rank of `M × M'` is
  `(Module.rank R M) + (Module.rank R M')`. -/
theorem rank_prod' : Module.rank R (M × M₁) = Module.rank R M + Module.rank R M₁ := by simp

Rank of Product of Free Modules Equals Sum of Ranks

Informal description

For free modules $M$ and $M_1$ over a ring $R$, the rank of their direct product $M \times M_1$ is equal to the sum of their ranks, i.e., $\text{rank}_R (M \times M_1) = \text{rank}_R M + \text{rank}_R M_1$.

Module.finrank_prod theorem

[Module.Finite R M] [Module.Finite R M'] : finrank R (M × M') = finrank R M + finrank R M'

Full source

/-- The finrank of `M × M'` is `(finrank R M) + (finrank R M')`. -/
@[simp]
theorem Module.finrank_prod [Module.Finite R M] [Module.Finite R M'] :
    finrank R (M × M') = finrank R M + finrank R M' := by
  simp [finrank, rank_lt_aleph0 R M, rank_lt_aleph0 R M']

Finite Rank of Product of Free Modules Equals Sum of Finite Ranks

Informal description

For finite free modules $M$ and $M'$ over a ring $R$, the finite rank of their direct product $M \times M'$ is equal to the sum of their finite ranks, i.e., $\text{finrank}_R (M \times M') = \text{finrank}_R M + \text{finrank}_R M'$.

rank_finsupp theorem

(ι : Type w) : Module.rank R (ι →₀ M) = Cardinal.lift.{v} #ι * Cardinal.lift.{w} (Module.rank R M)

Full source

@[simp]
theorem rank_finsupp (ι : Type w) :
    Module.rank R (ι →₀ M) = Cardinal.lift.{v} #ι * Cardinal.lift.{w} (Module.rank R M) := by
  obtain ⟨⟨_, bs⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
  rw [← bs.mk_eq_rank'', ← (Finsupp.basis fun _ : ι => bs).mk_eq_rank'', Cardinal.mk_sigma,
    Cardinal.sum_const]

Rank of Finitely Supported Functions: $\text{rank}_R (\iota \to_{\text{f}} M) = \#\iota \cdot \text{rank}_R M$

Informal description

For any type $\iota$ (in universe $w$) and any module $M$ over a ring $R$ (in universe $v$), the rank of the finitely supported functions $\iota \to_{\text{f}} M$ is equal to the product of the cardinality of $\iota$ and the rank of $M$, where both cardinals are lifted to a common universe. That is, \[ \text{rank}_R (\iota \to_{\text{f}} M) = \#\iota \cdot \text{rank}_R M. \]

rank_finsupp' theorem

(ι : Type v) : Module.rank R (ι →₀ M) = #ι * Module.rank R M

Full source

theorem rank_finsupp' (ι : Type v) : Module.rank R (ι →₀ M) = #ι * Module.rank R M := by
  simp [rank_finsupp]

Rank of Finitely Supported Functions: $\text{rank}_R (\iota \to_{\text{f}} M) = \#\iota \cdot \text{rank}_R M$ (same universe version)

Informal description

For any type $\iota$ (in the same universe as $M$) and any module $M$ over a ring $R$, the rank of the finitely supported functions $\iota \to_{\text{f}} M$ is equal to the product of the cardinality of $\iota$ and the rank of $M$, i.e., \[ \text{rank}_R (\iota \to_{\text{f}} M) = \#\iota \cdot \text{rank}_R M. \]

rank_finsupp_self theorem

(ι : Type w) : Module.rank R (ι →₀ R) = Cardinal.lift.{u} #ι

Full source

/-- The rank of `(ι →₀ R)` is `(#ι).lift`. -/
theorem rank_finsupp_self (ι : Type w) : Module.rank R (ι →₀ R) = Cardinal.lift.{u} #ι := by
  simp

Rank of Free Module of Finitely Supported Functions: $\text{rank}_R (\iota \to_{\text{f}} R) = \#\iota$

Informal description

For any type $\iota$ (in universe $w$), the rank of the free module of finitely supported functions from $\iota$ to $R$ is equal to the cardinality of $\iota$ lifted to the appropriate universe. That is, \[ \text{rank}_R (\iota \to_{\text{f}} R) = \#\iota. \]

rank_finsupp_self' theorem

{ι : Type u} : Module.rank R (ι →₀ R) = #ι

Full source

/-- If `R` and `ι` lie in the same universe, the rank of `(ι →₀ R)` is `# ι`. -/
theorem rank_finsupp_self' {ι : Type u} : Module.rank R (ι →₀ R) = #ι := by simp

Rank of Finitely Supported $R$-valued Functions: $\text{rank}_R(\iota \to_{\text{f}} R) = \#\iota$

Informal description

For any type $\iota$ (in the same universe as $R$), the rank of the $R$-module of finitely supported functions from $\iota$ to $R$ is equal to the cardinality of $\iota$, i.e., \[ \text{rank}_R(\iota \to_{\text{f}} R) = \#\iota. \]

rank_directSum theorem

 {ι : Type v} (M : ι → Type w) [∀ i : ι, AddCommMonoid (M i)] [∀ i : ι, Module R (M i)] [∀ i : ι, Module.Free R (M i)] :
  Module.rank R (⨁ i, M i) = Cardinal.sum fun i => Module.rank R (M i)

Full source

/-- The rank of the direct sum is the sum of the ranks. -/
@[simp]
theorem rank_directSum {ι : Type v} (M : ι → Type w) [∀ i : ι, AddCommMonoid (M i)]
    [∀ i : ι, Module R (M i)] [∀ i : ι, Module.Free R (M i)] :
    Module.rank R (⨁ i, M i) = Cardinal.sum fun i => Module.rank R (M i) := by
  let B i := chooseBasis R (M i)
  let b : Basis _ R (⨁ i, M i) := DFinsupp.basis fun i => B i
  simp [← b.mk_eq_rank'', fun i => (B i).mk_eq_rank'']

Rank of Direct Sum Equals Sum of Ranks

Informal description

Let $R$ be a ring satisfying the strong rank condition, and let $\{M_i\}_{i \in \iota}$ be a family of free $R$-modules indexed by $\iota$. The rank of the direct sum $\bigoplus_{i \in \iota} M_i$ is equal to the sum of the ranks of the individual modules $M_i$, i.e., \[ \text{rank}_R\left(\bigoplus_{i \in \iota} M_i\right) = \sum_{i \in \iota} \text{rank}_R(M_i). \]

rank_matrix_module theorem

 (m : Type w) (n : Type w') [Finite m] [Finite n] :
  Module.rank R (Matrix m n M) = lift.{max v w'} #m * lift.{max v w} #n * lift.{max w w'} (Module.rank R M)

Full source

/-- If `m` and `n` are finite, the rank of `m × n` matrices over a module `M` is
`(#m).lift * (#n).lift * rank R M`. -/
@[simp]
theorem rank_matrix_module (m : Type w) (n : Type w') [Finite m] [Finite n] :
    Module.rank R (Matrix m n M) =
      lift.{max v w'} #m * lift.{max v w} #n * lift.{max w w'} (Module.rank R M) := by
  cases nonempty_fintype m
  cases nonempty_fintype n
  obtain ⟨I, b⟩ := Module.Free.exists_basis (R := R) (M := M)
  rw [← (b.matrix m n).mk_eq_rank'']
  simp only [mk_prod, lift_mul, lift_lift, ← mul_assoc, b.mk_eq_rank'']

Rank Formula for Matrix Modules: $\text{rank}_R(\text{Matrix}(m, n, M)) = |m| \cdot |n| \cdot \text{rank}_R(M)$

Informal description

Let $R$ be a ring satisfying the strong rank condition, and let $M$ be a free $R$-module. For finite types $m$ and $n$, the rank of the $R$-module of $m \times n$ matrices with entries in $M$ is given by: \[ \text{rank}_R(\text{Matrix}(m, n, M)) = |m| \cdot |n| \cdot \text{rank}_R(M) \] where $|m|$ and $|n|$ denote the cardinalities of $m$ and $n$ respectively.

rank_matrix_module' theorem

 (m n : Type w) [Finite m] [Finite n] :
  Module.rank R (Matrix m n M) = lift.{max v} (#m * #n) * lift.{w} (Module.rank R M)

Full source

/-- If `m` and `n` are finite and lie in the same universe, the rank of `m × n` matrices over a
module `M` is `(#m * #n).lift * rank R M`. -/
@[simp high]
theorem rank_matrix_module' (m n : Type w) [Finite m] [Finite n] :
    Module.rank R (Matrix m n M) =
      lift.{max v} (#m * #n) * lift.{w} (Module.rank R M) := by
  rw [rank_matrix_module, lift_mul, lift_umaxlift_umax.{w, v}]

Rank Formula for Matrix Modules with Same Universe: $\text{rank}_R(\text{Matrix}(m, n, M)) = |m \times n| \cdot \text{rank}_R(M)$

Informal description

Let $R$ be a ring satisfying the strong rank condition, and let $M$ be a free $R$-module. For finite types $m$ and $n$ in the same universe, the rank of the $R$-module of $m \times n$ matrices with entries in $M$ is given by: \[ \text{rank}_R(\text{Matrix}(m, n, M)) = |m \times n| \cdot \text{rank}_R(M) \] where $|m \times n|$ denotes the cardinality of the product type $m \times n$.

rank_matrix theorem

 (m : Type v) (n : Type w) [Finite m] [Finite n] :
  Module.rank R (Matrix m n R) = Cardinal.lift.{max v w u, v} #m * Cardinal.lift.{max v w u, w} #n

Full source

/-- If `m` and `n` are finite, the rank of `m × n` matrices is `(#m).lift * (#n).lift`. -/
theorem rank_matrix (m : Type v) (n : Type w) [Finite m] [Finite n] :
    Module.rank R (Matrix m n R) =
      Cardinal.lift.{max v w u, v} #m * Cardinal.lift.{max v w u, w} #n := by
  rw [rank_matrix_module, rank_self, lift_one, mul_one, ← lift_liftlift_lift.{v, max u w}, lift_id,
    ← lift_liftlift_lift.{w, max u v}, lift_id]

Rank Formula for Matrix Modules over $R$: $\text{rank}_R(\text{Matrix}(m, n, R)) = |m| \cdot |n|$

Informal description

Let $R$ be a ring satisfying the strong rank condition, and let $m$ and $n$ be finite types. The rank of the $R$-module of $m \times n$ matrices over $R$ is given by: \[ \text{rank}_R(\text{Matrix}(m, n, R)) = |m| \cdot |n| \] where $|m|$ and $|n|$ denote the cardinalities of $m$ and $n$ respectively.

rank_matrix' theorem

(m n : Type v) [Finite m] [Finite n] : Module.rank R (Matrix m n R) = Cardinal.lift.{u} (#m * #n)

Full source

/-- If `m` and `n` are finite and lie in the same universe, the rank of `m × n` matrices is
  `(#n * #m).lift`. -/
theorem rank_matrix' (m n : Type v) [Finite m] [Finite n] :
    Module.rank R (Matrix m n R) = Cardinal.lift.{u} (#m * #n) := by
  rw [rank_matrix, lift_mul, lift_umaxlift_umax.{v, u}]

Rank of Matrix Module for Types in Same Universe: $\text{rank}_R(\text{Matrix}(m, n, R)) = |m \times n|$

Informal description

Let $R$ be a ring satisfying the strong rank condition, and let $m$ and $n$ be finite types in the same universe. The rank of the $R$-module of $m \times n$ matrices over $R$ is given by: \[ \text{rank}_R(\text{Matrix}(m, n, R)) = |m \times n| \] where $|m \times n|$ denotes the cardinality of the product type $m \times n$.

rank_matrix'' theorem

(m n : Type u) [Finite m] [Finite n] : Module.rank R (Matrix m n R) = #m * #n

Full source

/-- If `m` and `n` are finite and lie in the same universe as `R`, the rank of `m × n` matrices
  is `# m * # n`. -/
theorem rank_matrix'' (m n : Type u) [Finite m] [Finite n] :
    Module.rank R (Matrix m n R) = #m * #n := by simp

Rank of Matrix Module: $\text{rank}_R(\text{Matrix}(m, n, R)) = |m| \cdot |n|$

Informal description

Let $R$ be a ring satisfying the strong rank condition, and let $m$ and $n$ be finite types in the same universe. The rank of the $R$-module of $m \times n$ matrices over $R$ is given by: \[ \text{rank}_R(\text{Matrix}(m, n, R)) = |m| \cdot |n| \] where $|m|$ and $|n|$ denote the cardinalities of $m$ and $n$ respectively.

Module.finrank_finsupp theorem

{ι : Type v} [Fintype ι] : finrank R (ι →₀ M) = card ι * finrank R M

Full source

@[simp]
theorem finrank_finsupp {ι : Type v} [Fintype ι] : finrank R (ι →₀ M) = card ι * finrank R M := by
  rw [finrank, finrank, rank_finsupp, ← mk_toNat_eq_card, toNat_mul, toNat_lift, toNat_lift]

Finite Rank of Finitely Supported Functions: $\text{finrank}_R(\iota \to_{\text{f}} M) = |\iota| \cdot \text{finrank}_R M$

Informal description

For a finite type $\iota$ and a module $M$ over a ring $R$, the finite rank of the finitely supported functions $\iota \to_{\text{f}} M$ is equal to the product of the cardinality of $\iota$ and the finite rank of $M$, i.e., \[ \text{finrank}_R(\iota \to_{\text{f}} M) = |\iota| \cdot \text{finrank}_R M. \]

Module.finrank_finsupp_self theorem

{ι : Type v} [Fintype ι] : finrank R (ι →₀ R) = card ι

Full source

/-- The finrank of `(ι →₀ R)` is `Fintype.card ι`. -/
@[simp]
theorem finrank_finsupp_self {ι : Type v} [Fintype ι] : finrank R (ι →₀ R) = card ι := by
  rw [finrank, rank_finsupp_self, ← mk_toNat_eq_card, toNat_lift]

Finite Rank of Free Module of Finitely Supported Functions: $\text{finrank}_R(\iota \to_{\text{f}} R) = |\iota|$

Informal description

For any finite type $\iota$, the finite rank of the free module of finitely supported functions from $\iota$ to $R$ is equal to the cardinality of $\iota$, i.e., \[ \text{finrank}_R(\iota \to_{\text{f}} R) = |\iota|. \]

Module.finrank_directSum theorem

 {ι : Type v} [Fintype ι] (M : ι → Type w) [∀ i : ι, AddCommMonoid (M i)] [∀ i : ι, Module R (M i)]
  [∀ i : ι, Module.Free R (M i)] [∀ i : ι, Module.Finite R (M i)] : finrank R (⨁ i, M i) = ∑ i, finrank R (M i)

Full source

/-- The finrank of the direct sum is the sum of the finranks. -/
@[simp]
theorem finrank_directSum {ι : Type v} [Fintype ι] (M : ι → Type w) [∀ i : ι, AddCommMonoid (M i)]
    [∀ i : ι, Module R (M i)] [∀ i : ι, Module.Free R (M i)] [∀ i : ι, Module.Finite R (M i)] :
    finrank R (⨁ i, M i) = ∑ i, finrank R (M i) := by
  letI := nontrivial_of_invariantBasisNumber R
  simp only [finrank, fun i => rank_eq_card_chooseBasisIndex R (M i), rank_directSum, ← mk_sigma,
    mk_toNat_eq_card, card_sigma]

Finite Rank of Direct Sum Equals Sum of Finite Ranks

Informal description

Let $R$ be a ring, $\iota$ a finite index set, and $\{M_i\}_{i \in \iota}$ a family of finite free $R$-modules. The finite rank of the direct sum $\bigoplus_{i \in \iota} M_i$ is equal to the sum of the finite ranks of the individual modules $M_i$, i.e., \[ \text{finrank}_R\left(\bigoplus_{i \in \iota} M_i\right) = \sum_{i \in \iota} \text{finrank}_R(M_i). \]

Module.finrank_matrix theorem

(m n : Type*) [Fintype m] [Fintype n] : finrank R (Matrix m n M) = card m * card n * finrank R M

Full source

/-- If `m` and `n` are `Fintype`, the finrank of `m × n` matrices over a module `M` is
  `(Fintype.card m) * (Fintype.card n) * finrank R M`. -/
theorem finrank_matrix (m n : Type*) [Fintype m] [Fintype n] :
    finrank R (Matrix m n M) = card m * card n * finrank R M := by simp [finrank]

Finite Rank Formula for Matrix Modules: $\text{finrank}_R(\text{Matrix}(m, n, M)) = |m| \cdot |n| \cdot \text{finrank}_R(M)$

Informal description

Let $R$ be a ring and $M$ be a finite free $R$-module. For finite types $m$ and $n$, the finite rank of the $R$-module of $m \times n$ matrices with entries in $M$ is given by: \[ \text{finrank}_R(\text{Matrix}(m, n, M)) = |m| \cdot |n| \cdot \text{finrank}_R(M) \] where $|m|$ and $|n|$ denote the cardinalities of $m$ and $n$ respectively, and $\text{finrank}_R(M)$ denotes the finite rank of $M$ over $R$.

rank_pi theorem

[Finite η] : Module.rank R (∀ i, φ i) = Cardinal.sum fun i => Module.rank R (φ i)

Full source

/-- The rank of a finite product of free modules is the sum of the ranks. -/
-- this result is not true without the freeness assumption
@[simp]
theorem rank_pi [Finite η] : Module.rank R (∀ i, φ i) =
    Cardinal.sum fun i => Module.rank R (φ i) := by
  cases nonempty_fintype η
  let B i := chooseBasis R (φ i)
  let b : Basis _ R (∀ i, φ i) := Pi.basis fun i => B i
  simp [← b.mk_eq_rank'', fun i => (B i).mk_eq_rank'']

Rank of Product of Modules Equals Sum of Ranks

Informal description

For a finite index set $\eta$ and a family of $R$-modules $(\phi_i)_{i \in \eta}$, the rank of the product module $\prod_{i \in \eta} \phi_i$ is equal to the sum of the ranks of the individual modules $\phi_i$, i.e., \[ \text{rank}_R \left( \prod_{i \in \eta} \phi_i \right) = \sum_{i \in \eta} \text{rank}_R (\phi_i). \]

Module.finrank_pi theorem

{ι : Type v} [Fintype ι] : finrank R (ι → R) = Fintype.card ι

Full source

/-- The finrank of `(ι → R)` is `Fintype.card ι`. -/
theorem Module.finrank_pi {ι : Type v} [Fintype ι] :
    finrank R (ι → R) = Fintype.card ι := by
  simp [finrank]

Finite Rank of Function Module Equals Cardinality of Index Set

Informal description

For a finite type $\iota$, the finite rank of the $R$-module of functions from $\iota$ to $R$ is equal to the cardinality of $\iota$, i.e., \[ \text{finrank}_R (\iota \to R) = |\iota|. \]

Module.finrank_pi_fintype theorem

 {ι : Type v} [Fintype ι] {M : ι → Type w} [∀ i : ι, AddCommMonoid (M i)] [∀ i : ι, Module R (M i)]
  [∀ i : ι, Module.Free R (M i)] [∀ i : ι, Module.Finite R (M i)] : finrank R (∀ i, M i) = ∑ i, finrank R (M i)

Full source

/-- The finrank of a finite product is the sum of the finranks. -/
theorem Module.finrank_pi_fintype
    {ι : Type v} [Fintype ι] {M : ι → Type w} [∀ i : ι, AddCommMonoid (M i)]
    [∀ i : ι, Module R (M i)] [∀ i : ι, Module.Free R (M i)] [∀ i : ι, Module.Finite R (M i)] :
    finrank R (∀ i, M i) = ∑ i, finrank R (M i) := by
  letI := nontrivial_of_invariantBasisNumber R
  simp only [finrank, fun i => rank_eq_card_chooseBasisIndex R (M i), rank_pi, ← mk_sigma,
    mk_toNat_eq_card, Fintype.card_sigma]

Finite Rank of Product of Free Finitely Generated Modules Equals Sum of Finite Ranks

Informal description

For a finite index set $\iota$ and a family of free and finitely generated $R$-modules $(M_i)_{i \in \iota}$, the finite rank of the product module $\prod_{i \in \iota} M_i$ is equal to the sum of the finite ranks of the individual modules $M_i$, i.e., \[ \text{finrank}_R \left( \prod_{i \in \iota} M_i \right) = \sum_{i \in \iota} \text{finrank}_R (M_i). \]

rank_fun theorem

 {M η : Type u} [Fintype η] [AddCommMonoid M] [Module R M] [Module.Free R M] :
  Module.rank R (η → M) = Fintype.card η * Module.rank R M

Full source

theorem rank_fun {M η : Type u} [Fintype η] [AddCommMonoid M] [Module R M] [Module.Free R M] :
    Module.rank R (η → M) = Fintype.card η * Module.rank R M := by
  rw [rank_pi, Cardinal.sum_const', Cardinal.mk_fintype]

Rank of Function Module Equals Cardinality Times Rank: $\text{rank}_R (\eta \to M) = |\eta| \cdot \text{rank}_R M$

Informal description

For a finite type $\eta$ and a free $R$-module $M$, the rank of the function module $\eta \to M$ is equal to the product of the cardinality of $\eta$ and the rank of $M$, i.e., \[ \text{rank}_R (\eta \to M) = |\eta| \cdot \text{rank}_R M. \]

rank_fun_eq_lift_mul theorem

: Module.rank R (η → M) = (Fintype.card η : Cardinal.{max u₁' v}) * Cardinal.lift.{u₁'} (Module.rank R M)

Full source

theorem rank_fun_eq_lift_mul : Module.rank R (η → M) =
    (Fintype.card η : CardinalCardinal.{max u₁' v}) * Cardinal.lift.{u₁'} (Module.rank R M) := by
  rw [rank_pi, Cardinal.sum_const, Cardinal.mk_fintype, Cardinal.lift_natCast]

Rank of Function Module as Lifted Product: $\text{rank}_R (\eta \to M) = |\eta| \cdot \text{rank}_R M$

Informal description

For a finite type $\eta$ and a free $R$-module $M$, the rank of the function module $\eta \to M$ is equal to the product of the cardinality of $\eta$ (lifted to an appropriate cardinal universe) and the rank of $M$ (also lifted), i.e., \[ \text{rank}_R (\eta \to M) = |\eta| \cdot \text{rank}_R M. \]

rank_fun' theorem

: Module.rank R (η → R) = Fintype.card η

Full source

theorem rank_fun' : Module.rank R (η → R) = Fintype.card η := by
  rw [rank_fun_eq_lift_mul, rank_self, Cardinal.lift_one, mul_one]

Rank of Function Module Equals Cardinality of Index Set: $\text{rank}_R (\eta \to R) = |\eta|$

Informal description

For a finite type $\eta$ and a ring $R$, the rank of the free module $\eta \to R$ (the module of functions from $\eta$ to $R$) is equal to the cardinality of $\eta$, i.e., \[ \text{rank}_R (\eta \to R) = |\eta|. \]

rank_fin_fun theorem

(n : ℕ) : Module.rank R (Fin n → R) = n

Full source

theorem rank_fin_fun (n : ℕ) : Module.rank R (Fin n → R) = n := by simp [rank_fun']

Rank of Finite Function Module Equals Cardinality of Index Set

Informal description

For any natural number $n$ and any ring $R$ satisfying the strong rank condition, the rank of the free module $\text{Fin } n \to R$ (the module of functions from $\text{Fin } n$ to $R$) is equal to $n$.

Module.finrank_fintype_fun_eq_card theorem

: finrank R (η → R) = Fintype.card η

Full source

/-- The vector space of functions on a `Fintype ι` has finrank equal to the cardinality of `ι`. -/
@[simp]
theorem Module.finrank_fintype_fun_eq_card : finrank R (η → R) = Fintype.card η :=
  finrank_eq_of_rank_eq rank_fun'

Finite Rank of Function Module Equals Cardinality of Index Set: $\text{finrank}_R (\eta \to R) = |\eta|$

Informal description

For a finite type $\eta$ and a ring $R$, the finite rank of the free module $\eta \to R$ (the module of functions from $\eta$ to $R$) is equal to the cardinality of $\eta$, i.e., \[ \text{finrank}_R (\eta \to R) = |\eta|. \]

Module.finrank_fin_fun theorem

{n : ℕ} : finrank R (Fin n → R) = n

Full source

/-- The vector space of functions on `Fin n` has finrank equal to `n`. -/
theorem Module.finrank_fin_fun {n : ℕ} : finrank R (Fin n → R) = n := by simp

Finite Rank of Finite Function Module: $\text{finrank}_R (\text{Fin } n \to R) = n$

Informal description

For any natural number $n$ and any ring $R$, the finite rank of the free module of functions from $\text{Fin } n$ to $R$ is equal to $n$, i.e., \[ \text{finrank}_R (\text{Fin } n \to R) = n. \]

finDimVectorspaceEquiv definition

(n : ℕ) (hn : Module.rank R M = n) : M ≃ₗ[R] Fin n → R

Full source

/-- An `n`-dimensional `R`-vector space is equivalent to `Fin n → R`. -/
def finDimVectorspaceEquiv (n : ℕ) (hn : Module.rank R M = n) : M ≃ₗ[R] Fin n → R := by
  haveI := nontrivial_of_invariantBasisNumber R
  have : Cardinal.lift.{u} (n : CardinalCardinal.{v}) = Cardinal.lift.{v} (n : CardinalCardinal.{u}) := by simp
  have hn := Cardinal.lift_inj.{v, u}.2 hn
  rw [this] at hn
  rw [← @rank_fin_fun R _ _ n] at hn
  haveI : Module.Free R (Fin n → R) := Module.Free.pi _ _
  exact Classical.choice (nonempty_linearEquiv_of_lift_rank_eq hn)

Finite-dimensional vector space equivalence to function space

Informal description

For a finite-dimensional vector space $ M $ over a ring $ R $ with dimension $ n $, there exists a linear equivalence between $ M $ and the space of functions from the finite type $ \text{Fin } n $ to $ R $.

rank_tensorProduct theorem

: Module.rank R (M ⊗[S] M') = Cardinal.lift.{v'} (Module.rank R M) * Cardinal.lift.{v} (Module.rank S M')

Full source

/-- The `S`-rank of `M ⊗[R] M'` is `(Module.rank S M).lift * (Module.rank R M').lift`. -/
@[simp]
theorem rank_tensorProduct :
    Module.rank R (M ⊗[S] M') =
      Cardinal.lift.{v'} (Module.rank R M) * Cardinal.lift.{v} (Module.rank S M') := by
  obtain ⟨⟨_, bM⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
  obtain ⟨⟨_, bN⟩⟩ := Module.Free.exists_basis (R := S) (M := M')
  rw [← bM.mk_eq_rank'', ← bN.mk_eq_rank'', ← (bM.tensorProduct bN).mk_eq_rank'', Cardinal.mk_prod]

Rank of Tensor Product of Modules

Informal description

Let $R$ and $S$ be rings, and let $M$ be an $R$-module and $M'$ an $S$-module. Then the rank of the tensor product $M \otimes_{S} M'$ as an $R$-module is equal to the product of the ranks of $M$ and $M'$, where the ranks are lifted to the appropriate universes. That is, \[ \text{rank}_R(M \otimes_S M') = \text{rank}_R(M) \cdot \text{rank}_S(M'). \]

rank_tensorProduct' theorem

: Module.rank R (M ⊗[S] M₁) = Module.rank R M * Module.rank S M₁

Full source

/-- If `M` and `M'` lie in the same universe, the `S`-rank of `M ⊗[R] M'` is
  `(Module.rank S M) * (Module.rank R M')`. -/
theorem rank_tensorProduct' :
    Module.rank R (M ⊗[S] M₁) = Module.rank R M * Module.rank S M₁ := by simp

Rank of Tensor Product of Modules: $\text{rank}_R(M \otimes_S M_1) = \text{rank}_R(M) \cdot \text{rank}_S(M_1)$

Informal description

Let $R$ and $S$ be rings, and let $M$ be an $R$-module and $M_1$ an $S$-module. Then the rank of the tensor product $M \otimes_S M_1$ as an $R$-module is equal to the product of the ranks of $M$ as an $R$-module and $M_1$ as an $S$-module. That is, \[ \text{rank}_R(M \otimes_S M_1) = \text{rank}_R(M) \cdot \text{rank}_S(M_1). \]

Module.rank_baseChange theorem

: Module.rank R (R ⊗[S] M') = Cardinal.lift.{u} (Module.rank S M')

Full source

theorem Module.rank_baseChange :
    Module.rank R (R ⊗[S] M') = Cardinal.lift.{u} (Module.rank S M') := by simp

Rank of Base Change: $\text{rank}_R(R \otimes_S M') = \text{rank}_S(M')$

Informal description

Let $R$ and $S$ be rings, and let $M'$ be an $S$-module. Then the rank of the base change $R \otimes_S M'$ as an $R$-module is equal to the rank of $M'$ as an $S$-module, lifted to the appropriate universe. That is, \[ \text{rank}_R(R \otimes_S M') = \text{rank}_S(M'). \]

Module.finrank_tensorProduct theorem

: finrank R (M ⊗[S] M') = finrank R M * finrank S M'

Full source

/-- The `S`-finrank of `M ⊗[R] M'` is `(finrank S M) * (finrank R M')`. -/
@[simp]
theorem Module.finrank_tensorProduct :
    finrank R (M ⊗[S] M') = finrank R M * finrank S M' := by simp [finrank]

Finite Rank of Tensor Product of Modules: $\text{finrank}_R(M \otimes_S M') = \text{finrank}_R(M) \cdot \text{finrank}_S(M')$

Informal description

Let $R$ and $S$ be rings, and let $M$ be an $R$-module and $M'$ an $S$-module. If $M$ and $M'$ have finite rank as modules over $R$ and $S$ respectively, then the finite rank of the tensor product $M \otimes_S M'$ as an $R$-module is equal to the product of the finite ranks of $M$ and $M'$. That is, \[ \text{finrank}_R(M \otimes_S M') = \text{finrank}_R(M) \cdot \text{finrank}_S(M'). \]

Module.finrank_baseChange theorem

: finrank R (R ⊗[S] M') = finrank S M'

Full source

theorem Module.finrank_baseChange : finrank R (R ⊗[S] M') = finrank S M' := by simp

Finite Rank of Base Change: $\text{finrank}_R(R \otimes_S M') = \text{finrank}_S(M')$

Informal description

Let $R$ and $S$ be rings, and let $M'$ be an $S$-module of finite rank. Then the finite rank of the base change $R \otimes_S M'$ as an $R$-module is equal to the finite rank of $M'$ as an $S$-module, i.e., \[ \text{finrank}_R(R \otimes_S M') = \text{finrank}_S(M'). \]

Submodule.lt_of_le_of_finrank_lt_finrank theorem

{s t : Submodule R M} (le : s ≤ t) (lt : finrank R s < finrank R t) : s < t

Full source

theorem lt_of_le_of_finrank_lt_finrank {s t : Submodule R M} (le : s ≤ t)
    (lt : finrank R s < finrank R t) : s < t :=
  lt_of_le_of_ne le fun h => ne_of_lt lt (by rw [h])

Strict Containment of Submodules via Rank Comparison

Informal description

Let $s$ and $t$ be submodules of a module $M$ over a ring $R$ such that $s \leq t$. If the (finite) rank of $s$ is strictly less than the (finite) rank of $t$, then $s$ is strictly contained in $t$, i.e., $s < t$.

Submodule.lt_top_of_finrank_lt_finrank theorem

{s : Submodule R M} (lt : finrank R s < finrank R M) : s < ⊤

Full source

theorem lt_top_of_finrank_lt_finrank {s : Submodule R M} (lt : finrank R s < finrank R M) :
    s < ⊤ := by
  rw [← finrank_top R M] at lt
  exact lt_of_le_of_finrank_lt_finrank le_top lt

Proper Submodule Criterion via Rank Comparison: $\text{rank}(s) < \text{rank}(M) \implies s < M$

Informal description

For any submodule $s$ of a finite-dimensional module $M$ over a ring $R$, if the rank of $s$ is strictly less than the rank of $M$, then $s$ is strictly contained in the top submodule (i.e., $s$ is a proper submodule of $M$).

Submodule.finrank_le theorem

[Module.Finite R M] (s : Submodule R M) : finrank R s ≤ finrank R M

Full source

/-- The dimension of a submodule is bounded by the dimension of the ambient space. -/
theorem Submodule.finrank_le [Module.Finite R M] (s : Submodule R M) :
    finrank R s ≤ finrank R M :=
  toNat_le_toNat (Submodule.rank_le s) (rank_lt_aleph0 _ _)

Submodule Rank Bound: $\text{rank}(s) \leq \text{rank}(M)$ for Finite-Dimensional Modules

Informal description

For any finite-dimensional module $M$ over a ring $R$ and any submodule $s$ of $M$, the rank of $s$ is less than or equal to the rank of $M$, i.e., $\text{rank}(s) \leq \text{rank}(M)$.

Submodule.finrank_map_le theorem

[Module R M'] (f : M →ₗ[R] M') (p : Submodule R M) [Module.Finite R p] : finrank R (p.map f) ≤ finrank R p

Full source

/-- Pushforwards of finite submodules have a smaller finrank. -/
theorem Submodule.finrank_map_le
    [Module R M'] (f : M →ₗ[R] M') (p : Submodule R M) [Module.Finite R p] :
    finrank R (p.map f) ≤ finrank R p :=
  finrank_le_finrank_of_rank_le_rank (lift_rank_map_le _ _) (rank_lt_aleph0 _ _)

Rank Inequality for Linear Image of Finite Submodule

Informal description

Let $R$ be a ring, $M$ and $M'$ be $R$-modules, and $f: M \to M'$ be an $R$-linear map. For any finite-rank submodule $p \subseteq M$, the rank of the image submodule $f(p)$ satisfies $\operatorname{finrank}_R(f(p)) \leq \operatorname{finrank}_R(p)$.

Submodule.finrank_mono theorem

{s t : Submodule R M} [Module.Finite R t] (hst : s ≤ t) : finrank R s ≤ finrank R t

Full source

theorem Submodule.finrank_mono {s t : Submodule R M} [Module.Finite R t] (hst : s ≤ t) :
    finrank R s ≤ finrank R t :=
  Cardinal.toNat_le_toNat (Submodule.rank_mono hst) (rank_lt_aleph0 R ↥t)

Monotonicity of Rank for Submodules

Informal description

For any submodules $s$ and $t$ of a module $M$ over a ring $R$, if $s$ is contained in $t$ and $t$ is finitely generated as an $R$-module, then the rank of $s$ is less than or equal to the rank of $t$.

rank_span_le theorem

(s : Set M) : Module.rank R (span R s) ≤ #s

Full source

theorem rank_span_le (s : Set M) : Module.rank R (span R s) ≤ #s := by
  rw [Finsupp.span_eq_range_linearCombination, ← lift_strictMono.le_iff_le]
  refine (lift_rank_range_le _).trans ?_
  rw [rank_finsupp_self]
  simp only [lift_lift, le_refl]

Rank Bound for Span of a Set: $\text{rank}_R (\text{span}_R s) \leq \#s$

Informal description

For any subset $s$ of an $R$-module $M$, the rank of the submodule spanned by $s$ is bounded above by the cardinality of $s$, i.e., \[ \text{rank}_R (\text{span}_R s) \leq \#s. \]

rank_span_finset_le theorem

(s : Finset M) : Module.rank R (span R (s : Set M)) ≤ s.card

Full source

theorem rank_span_finset_le (s : Finset M) : Module.rank R (span R (s : Set M)) ≤ s.card := by
  simpa using rank_span_le s.toSet

Rank Bound for Span of a Finite Set: $\text{rank}_R (\text{span}_R s) \leq |s|$

Informal description

For any finite subset $s$ of an $R$-module $M$, the rank of the submodule spanned by $s$ is bounded above by the cardinality of $s$, i.e., \[ \text{rank}_R (\text{span}_R s) \leq |s|. \]

rank_span_of_finset theorem

(s : Finset M) : Module.rank R (span R (s : Set M)) < ℵ₀

Full source

theorem rank_span_of_finset (s : Finset M) : Module.rank R (span R (s : Set M)) < ℵ₀ :=
  (rank_span_finset_le s).trans_lt (Cardinal.nat_lt_aleph0 _)

Finite Rank of Span for Finite Sets

Informal description

For any finite subset $s$ of an $R$-module $M$, the rank of the submodule spanned by $s$ is finite, i.e., \[ \text{rank}_R (\text{span}_R s) < \aleph_0. \]

Set.finrank definition

(s : Set M) : ℕ

Full source

/-- The rank of a set of vectors as a natural number. -/
protected noncomputable def Set.finrank (s : Set M) : ℕ :=
  finrank R (span R s)

Dimension of the span of a set in a module

Informal description

The function assigns to a subset $s$ of a module $M$ over a ring $R$ the dimension of the submodule generated by $s$, as a natural number. This is defined as the dimension of the span of $s$ over $R$.

finrank_span_le_card theorem

(s : Set M) [Fintype s] : finrank R (span R s) ≤ s.toFinset.card

Full source

theorem finrank_span_le_card (s : Set M) [Fintype s] : finrank R (span R s) ≤ s.toFinset.card :=
  finrank_le_of_rank_le (by simpa using rank_span_le (R := R) s)

Finite Rank Bound for Span: $\text{finrank}_R (\text{span}_R s) \leq |s|$

Informal description

For any finite subset $s$ of an $R$-module $M$, the dimension of the submodule spanned by $s$ is bounded above by the cardinality of $s$, i.e., \[ \text{finrank}_R (\text{span}_R s) \leq |s|. \]

finrank_span_finset_le_card theorem

(s : Finset M) : (s : Set M).finrank R ≤ s.card

Full source

theorem finrank_span_finset_le_card (s : Finset M) : (s : Set M).finrank R ≤ s.card :=
  calc
    (s : Set M).finrank R ≤ (s : Set M).toFinset.card := finrank_span_le_card (M := M) s
    _ = s.card := by simp

Finite Rank Bound for Span: $\text{finrank}_R (\text{span}_R s) \leq |s|$

Informal description

For any finite subset $s$ of an $R$-module $M$, the dimension of the submodule spanned by $s$ is bounded above by the cardinality of $s$, i.e., \[ \text{finrank}_R (\text{span}_R s) \leq |s|. \]

finrank_range_le_card theorem

{ι : Type*} [Fintype ι] (b : ι → M) : (Set.range b).finrank R ≤ Fintype.card ι

Full source

theorem finrank_range_le_card {ι : Type*} [Fintype ι] (b : ι → M) :
    (Set.range b).finrank R ≤ Fintype.card ι := by
  classical
  refine (finrank_span_le_card _).trans ?_
  rw [Set.toFinset_range]
  exact Finset.card_image_le

Finite Rank Bound for Range: $\text{finrank}_R (\text{span}_R (\text{range } b)) \leq |\iota|$

Informal description

For any finite type $\iota$ and any function $b : \iota \to M$ mapping into an $R$-module $M$, the dimension of the span of the range of $b$ is bounded above by the cardinality of $\iota$, i.e., \[ \text{finrank}_R (\text{span}_R (\text{range } b)) \leq \text{card } \iota. \]

finrank_span_eq_card theorem

 [Nontrivial R] {ι : Type*} [Fintype ι] {b : ι → M} (hb : LinearIndependent R b) :
  finrank R (span R (Set.range b)) = Fintype.card ι

Full source

theorem finrank_span_eq_card [Nontrivial R] {ι : Type*} [Fintype ι] {b : ι → M}
    (hb : LinearIndependent R b) :
    finrank R (span R (Set.range b)) = Fintype.card ι :=
  finrank_eq_of_rank_eq
    (by
      have : Module.rank R (span R (Set.range b)) = #(Set.range b) := rank_span hb
      rwa [← lift_inj, mk_range_eq_of_injective hb.injective, Cardinal.mk_fintype, lift_natCast,
        lift_eq_nat_iff] at this)

Rank of Span Equals Cardinality for Linearly Independent Family

Informal description

Let $R$ be a nontrivial ring and $M$ an $R$-module. For any finite type $\iota$ and a linearly independent family $b : \iota \to M$, the rank of the span of the range of $b$ equals the cardinality of $\iota$, i.e., \[ \text{finrank}_R (\text{span}_R (\text{range } b)) = \text{card } \iota. \]

finrank_span_set_eq_card theorem

{s : Set M} [Fintype s] (hs : LinearIndepOn R id s) : finrank R (span R s) = s.toFinset.card

Full source

theorem finrank_span_set_eq_card {s : Set M} [Fintype s] (hs : LinearIndepOn R id s) :
    finrank R (span R s) = s.toFinset.card :=
  finrank_eq_of_rank_eq
    (by
      have : Module.rank R (span R s) = #s := rank_span_set hs
      rwa [Cardinal.mk_fintype, ← Set.toFinset_card] at this)

Rank of Span Equals Cardinality for Linearly Independent Finite Sets

Informal description

For any finite set $s$ of vectors in a module $M$ over a ring $R$, if the vectors in $s$ are linearly independent, then the rank of the submodule spanned by $s$ is equal to the cardinality of $s$.

finrank_span_finset_eq_card theorem

{s : Finset M} (hs : LinearIndepOn R id (s : Set M)) : finrank R (span R (s : Set M)) = s.card

Full source

theorem finrank_span_finset_eq_card {s : Finset M} (hs : LinearIndepOn R id (s : Set M)) :
    finrank R (span R (s : Set M)) = s.card := by
  convert finrank_span_set_eq_card (s := (s : Set M)) hs
  ext
  simp

Rank of Span Equals Cardinality for Linearly Independent Finite Sets

Informal description

For any finite set $s$ of vectors in a module $M$ over a ring $R$, if the vectors in $s$ are linearly independent, then the rank of the submodule spanned by $s$ is equal to the cardinality of $s$, i.e., $\text{finrank}_R (\text{span}_R s) = \text{card } s$.

span_lt_of_subset_of_card_lt_finrank theorem

{s : Set M} [Fintype s] {t : Submodule R M} (subset : s ⊆ t) (card_lt : s.toFinset.card < finrank R t) : span R s < t

Full source

theorem span_lt_of_subset_of_card_lt_finrank {s : Set M} [Fintype s] {t : Submodule R M}
    (subset : s ⊆ t) (card_lt : s.toFinset.card < finrank R t) : span R s < t :=
  lt_of_le_of_finrank_lt_finrank (span_le.mpr subset)
    (lt_of_le_of_lt (finrank_span_le_card _) card_lt)

Strict Span Containment via Cardinality and Rank Comparison

Informal description

Let $s$ be a finite subset of an $R$-module $M$ and $t$ a submodule of $M$ such that $s \subseteq t$. If the cardinality of $s$ is strictly less than the rank of $t$, then the submodule spanned by $s$ is strictly contained in $t$, i.e., \[ \text{span}_R s < t. \]

span_lt_top_of_card_lt_finrank theorem

{s : Set M} [Fintype s] (card_lt : s.toFinset.card < finrank R M) : span R s < ⊤

Full source

theorem span_lt_top_of_card_lt_finrank {s : Set M} [Fintype s]
    (card_lt : s.toFinset.card < finrank R M) : span R s < ⊤ :=
  lt_top_of_finrank_lt_finrank (lt_of_le_of_lt (finrank_span_le_card _) card_lt)

Proper Span Criterion via Cardinality and Rank: $|s| < \text{rank}(M) \implies \text{span}_R s < M$

Informal description

For any finite subset $s$ of an $R$-module $M$, if the cardinality of $s$ is strictly less than the rank of $M$, then the submodule spanned by $s$ is strictly contained in the top submodule (i.e., $\text{span}_R s$ is a proper submodule of $M$).

finrank_le_of_span_eq_top theorem

{ι : Type*} [Fintype ι] {v : ι → M} (hv : Submodule.span R (Set.range v) = ⊤) : finrank R M ≤ Fintype.card ι

Full source

lemma finrank_le_of_span_eq_top {ι : Type*} [Fintype ι] {v : ι → M}
    (hv : Submodule.span R (Set.range v) = ⊤) : finrank R M ≤ Fintype.card ι := by
  classical
  rw [← finrank_top, ← hv]
  exact (finrank_span_le_card _).trans (by convert Fintype.card_range_le v; rw [Set.toFinset_card])

Finite Dimension Bound for Spanning Sets: $\operatorname{finrank}_R M \leq |\iota|$

Informal description

Let $M$ be a module over a ring $R$ and let $\{v_i\}_{i \in \iota}$ be a finite family of vectors in $M$ indexed by a finite type $\iota$. If the span of $\{v_i\}_{i \in \iota}$ is the entire module $M$, then the finite dimension of $M$ over $R$ is bounded above by the cardinality of $\iota$, i.e., \[ \operatorname{finrank}_R M \leq |\iota|. \]

Subalgebra.rank_toSubmodule theorem

(S : Subalgebra F E) : Module.rank F (Subalgebra.toSubmodule S) = Module.rank F S

Full source

@[simp]
theorem Subalgebra.rank_toSubmodule (S : Subalgebra F E) :
    Module.rank F (Subalgebra.toSubmodule S) = Module.rank F S :=
  rfl

Rank Equality for Subalgebra and its Underlying Submodule

Informal description

For any subalgebra $S$ of a field extension $E$ over $F$, the rank of $S$ as an $F$-vector space is equal to the rank of its underlying submodule over $F$. That is, $\operatorname{rank}_F (\operatorname{toSubmodule} S) = \operatorname{rank}_F S$.

Subalgebra.finrank_toSubmodule theorem

(S : Subalgebra F E) : finrank F (Subalgebra.toSubmodule S) = finrank F S

Full source

@[simp]
theorem Subalgebra.finrank_toSubmodule (S : Subalgebra F E) :
    finrank F (Subalgebra.toSubmodule S) = finrank F S :=
  rfl

Equality of Finite Dimension for Subalgebra and its Underlying Submodule

Informal description

For any subalgebra $S$ of a field extension $E$ over $F$, the finite dimension of $S$ as a vector space over $F$ is equal to the finite dimension of its underlying submodule over $F$. That is, $\operatorname{finrank}_F (S) = \operatorname{finrank}_F (\operatorname{toSubmodule} S)$.

subalgebra_top_rank_eq_submodule_top_rank theorem

: Module.rank F (⊤ : Subalgebra F E) = Module.rank F (⊤ : Submodule F E)

Full source

theorem subalgebra_top_rank_eq_submodule_top_rank :
    Module.rank F (⊤ : Subalgebra F E) = Module.rank F (⊤ : Submodule F E) := by
  rw [← Algebra.top_toSubmodule]
  rfl

Rank Equality for Top Subalgebra and Top Submodule in Field Extension

Informal description

For a field extension $E$ over $F$, the rank of the top subalgebra $\top$ in $E$ is equal to the rank of the top submodule $\top$ in $E$ as $F$-vector spaces. That is, $\operatorname{rank}_F (\top : \operatorname{Subalgebra} F E) = \operatorname{rank}_F (\top : \operatorname{Submodule} F E)$.

subalgebra_top_finrank_eq_submodule_top_finrank theorem

: finrank F (⊤ : Subalgebra F E) = finrank F (⊤ : Submodule F E)

Full source

theorem subalgebra_top_finrank_eq_submodule_top_finrank :
    finrank F (⊤ : Subalgebra F E) = finrank F (⊤ : Submodule F E) := by
  rw [← Algebra.top_toSubmodule]
  rfl

Finite Dimension Equality for Top Subalgebra and Top Submodule in Field Extension

Informal description

For a field extension $E$ over $F$, the finite dimension of the top subalgebra $\top$ in $E$ is equal to the finite dimension of the top submodule $\top$ in $E$ as $F$-vector spaces. That is, $\operatorname{finrank}_F (\top : \operatorname{Subalgebra} F E) = \operatorname{finrank}_F (\top : \operatorname{Submodule} F E)$.

Subalgebra.rank_top theorem

: Module.rank F (⊤ : Subalgebra F E) = Module.rank F E

Full source

theorem Subalgebra.rank_top : Module.rank F (⊤ : Subalgebra F E) = Module.rank F E := by
  rw [subalgebra_top_rank_eq_submodule_top_rank]
  exact _root_.rank_top F E

Rank Equality for Top Subalgebra and Entire Field Extension

Informal description

For a field extension $E$ over $F$, the rank of the top subalgebra $\top$ in $E$ is equal to the rank of $E$ as an $F$-vector space, i.e., $\operatorname{rank}_F (\top : \operatorname{Subalgebra} F E) = \operatorname{rank}_F E$.

Subalgebra.rank_bot theorem

: Module.rank F (⊥ : Subalgebra F E) = 1

Full source

@[simp]
theorem Subalgebra.rank_bot : Module.rank F (⊥ : Subalgebra F E) = 1 :=
  (Subalgebra.toSubmoduleEquiv (⊥ : Subalgebra F E)).symm.rank_eq.trans <| by
    rw [Algebra.toSubmodule_bot, one_eq_span, rank_span_set, mk_singleton _]
    letI := Module.nontrivial F E
    exact LinearIndepOn.id_singleton _ one_ne_zero

Rank of Trivial Subalgebra is One

Informal description

The rank of the bottom subalgebra (the trivial subalgebra) of a field extension $E$ over $F$ is equal to $1$, i.e., $\text{rank}_F (\bot : \text{Subalgebra } F E) = 1$.

Subalgebra.finrank_bot theorem

: finrank F (⊥ : Subalgebra F E) = 1

Full source

@[simp]
theorem Subalgebra.finrank_bot : finrank F (⊥ : Subalgebra F E) = 1 :=
  finrank_eq_of_rank_eq (by simp)

Finite Rank of Trivial Subalgebra is One

Informal description

The finite rank of the trivial subalgebra (⊥) of a field extension $E$ over $F$ is equal to $1$, i.e., $\text{finrank}_F (\bot) = 1$.

Main statements