`Definitions/Def_Mathlib_LinearAlgebra_Countable.lean`

definition moduleadapted from the Imperial College London FLT project: FLT/Mathlib/LinearAlgebra/Countable.lean

Countability of finite modules; number fields are countable

Two general-purpose facts about countability are recorded. The first, Countable.of_module_finite, asserts that for a semiring R with countable underlying type and an additive commutative monoid M carrying an R-module structure which is module-finite over R (i.e. finitely generated as an R-module), the type M is countable. The argument takes a finite spanning family s : \mathrm{Fin}\,n \to M whose R-span is all of M, observes that the span of the range of such a family is countable, and transports this along the equality of the span with the whole module; concretely, every element of M is an R-linear combination of finitely many fixed generators, and there are only countably many such combinations when R is countable.

The second declaration is an instance deducing from this that the underlying type of any number field K is countable: a number field is by definition a field of characteristic zero which is finite-dimensional over \mathbb{Q}, so K is a module-finite \mathbb{Q}-module and \mathbb{Q} is countable. Being an instance, it makes countability of number fields available to typeclass inference throughout, for instance when a construction requires a countable index set or a countable coefficient field.

Relation to Mathlib

Both declarations are stated in Mathlib's namespaces and rely only on Mathlib notions (Module.Finite, Countable, NumberField); they are auxiliary lemmas of the kind intended for eventual inclusion in Mathlib rather than project-specific definitions.

Where it is used

The countability instance for number fields is used as ambient infrastructure by many later modules, where countability of a field or of a set of arithmetic data is needed for measure-theoretic, topological or cardinality side conditions.

English text generated automatically from the Lean source; the Lean statement is authoritative.

16 lines
2 declarations
used in the statements of 13 theorems and imported by 52 proofs
imports 0 definition modules

Source file: Definitions/Def_Mathlib_LinearAlgebra_Countable.lean

Imports

only Mathlib

Imported by

Def_NumberField_Completion_Finite

Declarations

lemmaCountable.of_module_finite

Source

import Mathlib

section

lemma Countable.of_module_finite (R M : Type*) [Semiring R] [Countable R]
    [AddCommMonoid M] [Module R M] [Module.Finite R M] : Countable M := by
  obtain ⟨n, s, h⟩ := Module.Finite.exists_fin (R := R) (M := M)
  rw [← Set.countable_univ_iff]
  have : Countable (Submodule.span R (Set.range s)) := inferInstance
  rwa [h] at this

instance (K : Type*) [Field K] [NumberField K] : Countable K :=
  Countable.of_module_finite ℚ K

end

Definitions/Def_Mathlib_LinearAlgebra_Countable.lean