Mathlib.RingTheory.Finiteness.Cardinality

Module.Finite.exists_fin' theorem

[Module.Finite R M] : ∃ (n : ℕ) (f : (Fin n → R) →ₗ[R] M), Surjective f

Full source

/-- A finite module admits a surjective linear map from a finite free module. -/
lemma exists_fin' [Module.Finite R M] : ∃ (n : ℕ) (f : (Fin n → R) →ₗ[R] M), Surjective f := by
  have ⟨n, s, hs⟩ := exists_fin (R := R) (M := M)
  refine ⟨n, Basis.constr (Pi.basisFun R _) ℕ s, ?_⟩
  rw [← LinearMap.range_eq_top, Basis.constr_range, hs]

Existence of Surjective Linear Map from Free Module for Finitely Generated Modules

Informal description

Let $M$ be a finitely generated module over a semiring $R$. Then there exists a natural number $n$ and a surjective linear map $f : R^n \to M$.

Module.finite_of_finite theorem

[Finite R] [Module.Finite R M] : Finite M

Full source

lemma _root_.Module.finite_of_finite [Finite R] [Module.Finite R M] : Finite M := by
  obtain ⟨n, f, hf⟩ := exists_fin' R M; exact .of_surjective f hf

Finitely generated modules over finite semirings are finite

Informal description

Let $R$ be a finite semiring and $M$ a finitely generated module over $R$. Then $M$ is finite as a set.

Module.finite_iff_finite theorem

[Finite R] : Module.Finite R M ↔ Finite M

Full source

/-- A module over a finite ring has finite dimension iff it is finite. -/
lemma _root_.Module.finite_iff_finite [Finite R] : Module.FiniteModule.Finite R M ↔ Finite M :=
  ⟨fun _ ↦ finite_of_finite R, fun _ ↦ .of_finite⟩

Equivalence of Finite Generation and Finiteness for Modules over Finite Semirings

Informal description

Let $R$ be a finite semiring and $M$ a module over $R$. Then $M$ is finitely generated as an $R$-module if and only if $M$ is finite as a set.

Set.Finite.submoduleSpan theorem

[Finite R] {s : Set M} (hs : s.Finite) : (Submodule.span R s : Set M).Finite

Full source

lemma _root_.Set.Finite.submoduleSpan [Finite R] {s : Set M} (hs : s.Finite) :
    (Submodule.span R s : Set M).Finite := by
  lift s to Finset M using hs
  rw [Set.Finite, ← Module.finite_iff_finite (R := R)]
  dsimp
  infer_instance

Finiteness of Submodule Span for Finite Sets over Finite Semirings

Informal description

Let $R$ be a finite semiring and $M$ a module over $R$. For any finite subset $s \subseteq M$, the $R$-linear span of $s$ is finite as a subset of $M$.

Module.Finite.finite_basis theorem

[Nontrivial R] {ι} [Module.Finite R M] (b : Basis ι R M) : _root_.Finite ι

Full source

/-- If a free module is finite, then any arbitrary basis is finite. -/
lemma finite_basis [Nontrivial R] {ι} [Module.Finite R M]
    (b : Basis ι R M) :
    _root_.Finite ι :=
  let ⟨s, hs⟩ := ‹Module.Finite R M›
  basis_finite_of_finite_spans s.finite_toSet hs b

Finiteness of Basis in Finitely Generated Modules

Informal description

Let $R$ be a nontrivial ring and $M$ a finitely generated $R$-module. For any basis $b$ of $M$ indexed by a type $\iota$, the index type $\iota$ is finite.

Module.not_finite_of_infinite_basis theorem

[Nontrivial R] {ι} [Infinite ι] (b : Basis ι R M) : ¬Module.Finite R M

Full source

lemma not_finite_of_infinite_basis [Nontrivial R] {ι} [Infinite ι] (b : Basis ι R M) :
    ¬ Module.Finite R M :=
  fun _ ↦ (Finite.finite_basis b).not_infinite ‹_›

Non-finite generation of modules with infinite bases

Informal description

Let $R$ be a nontrivial ring and $M$ an $R$-module. If $M$ has an infinite basis indexed by a type $\iota$, then $M$ is not finitely generated as an $R$-module.