English
If v and v' are bases of the same module M, then the index sets have the same cardinality.
Русский
Если v и v' являются базисами одного модуля M, то мощности индексов совпадают.
LaTeX
$$$\lvert ι \rvert = \lvert ι' \rvert$ for bases $v$ and $v'$ of the same module.$$
Lean4
/-- The dimension theorem: if `v` and `v'` are two bases, their index types
have the same cardinalities. -/
theorem mk_eq_mk_of_basis (v : Basis ι R M) (v' : Basis ι' R M) : Cardinal.lift.{w'} #ι = Cardinal.lift.{w} #ι' := by
classical
haveI := nontrivial_of_invariantBasisNumber R
cases fintypeOrInfinite ι
· -- `v` is a finite basis, so by `basis_finite_of_finite_spans` so is `v'`.
-- haveI : Finite (range v) := Set.finite_range v
haveI := basis_finite_of_finite_spans (Set.finite_range v) v.span_eq v'
cases nonempty_fintype ι'
rw [Cardinal.mk_fintype, Cardinal.mk_fintype]
simp only [Cardinal.lift_natCast, Nat.cast_inj]
-- Now we can use invariant basis number to show they have the same cardinality.
apply card_eq_of_linearEquiv R
exact
(Finsupp.linearEquivFunOnFinite R R ι).symm.trans v.repr.symm ≪≫ₗ v'.repr ≪≫ₗ
Finsupp.linearEquivFunOnFinite R R ι'
· -- `v` is an infinite basis,
-- so by `infinite_basis_le_maximal_linearIndependent`, `v'` is at least as big,
-- and then applying `infinite_basis_le_maximal_linearIndependent` again
-- we see they have the same cardinality.
have w₁ := infinite_basis_le_maximal_linearIndependent' v _ v'.linearIndependent v'.maximal
rcases Cardinal.lift_mk_le'.mp w₁ with ⟨f⟩
haveI : Infinite ι' := Infinite.of_injective f f.2
have w₂ := infinite_basis_le_maximal_linearIndependent' v' _ v.linearIndependent v.maximal
exact le_antisymm w₁ w₂
