rank_R — Mathlib

English

If σ is finite, then the K-rank (dimension) of R(σ, K) equals card(σ → K).

Русский

Если σ — конечный, тогда размерность (ранг) R(σ, K) как K-пространства равна кардиналу множества функций σ → K.

LaTeX

$$$\\\\operatorname{rank}_K(R(\\\\sigma, K)) = |\\\\sigma \\to K|.$$$

Lean4

theorem rank_R [Fintype σ] : Module.rank K (R σ K) = Fintype.card (σ → K) :=
  calc
    Module.rank K (R σ K) = Module.rank K (↥{s : σ →₀ ℕ | ∀ n : σ, s n ≤ Fintype.card K - 1} →₀ K) :=
      LinearEquiv.rank_eq (Finsupp.supportedEquivFinsupp {s : σ →₀ ℕ | ∀ n : σ, s n ≤ Fintype.card K - 1})
    _ = #{s : σ →₀ ℕ | ∀ n : σ, s n ≤ Fintype.card K - 1} := by rw [rank_finsupp_self']
    _ = #{s : σ → ℕ | ∀ n : σ, s n < Fintype.card K} :=
      by
      refine Quotient.sound ⟨Equiv.subtypeEquiv Finsupp.equivFunOnFinite fun f => ?_⟩
      refine forall_congr' fun n => le_tsub_iff_right ?_
      exact Fintype.card_pos_iff.2 ⟨0⟩
    _ = #(σ → { n // n < Fintype.card K }) :=
      (@Equiv.subtypePiEquivPi σ (fun _ => ℕ) fun _ n => n < Fintype.card K).cardinal_eq
    _ = #(σ → Fin (Fintype.card K)) := (Equiv.arrowCongr (Equiv.refl σ) Fin.equivSubtype.symm).cardinal_eq
    _ = #(σ → K) := (Equiv.arrowCongr (Equiv.refl σ) (Fintype.equivFin K).symm).cardinal_eq
    _ = Fintype.card (σ → K) := Cardinal.mk_fintype _

Похожие утверждения