freeOfProfinite — Mathlib

English

The LocallyConstant ℤ-module on any profinite S is a free ℤ-module.

Русский

Модуль LocallyConstant ℤ над любой профинистой S является свободным модулем над целыми числами.

LaTeX

$$$\\text{LocallyConstant.Free }\\mathbb{Z}(\\text{LocallyConstant } S\\mathbb{Z})$$$

Lean4

/-- **Nöbeling's theorem**. The `ℤ`-module `LocallyConstant S ℤ` is free for every
`S : Profinite`. -/
instance freeOfProfinite (S : Profinite.{u}) : Module.Free ℤ (LocallyConstant S ℤ) :=
  by
  obtain ⟨_, _⟩ := exists_wellOrder { C : Set S // IsClopen C }
  exact @Nobeling_aux { C : Set S // IsClopen C } _ _ S (Nobeling.ι S) (Nobeling.isClosedEmbedding S)

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