The dense copy of the infinite cyclic group in ZHat has the expected universal property. A map to a finite discrete group factors through the cyclic quotient determined by the order of the image of 1; the finite-quotient criterion then gives the full pro-all-finite completion and free-profinite properties.
This production leaf is independent of every Progress module.
The canonical topological generator 1 of the multiplicative profinite integers.
Surrounding namespaces, section variables, and local commands at this declaration.
open Set
open scoped Topology
noncomputable section
namespace ClassFieldTower.Cohomology.ProfiniteInteger
open ProCGroups
open ProCGroups.FreeProCabbrev generator : ClassFormation.ZHatMulThe dense homomorphism from the infinite cyclic group to the profinite integers.
Surrounding namespaces, section variables, and local commands at this declaration.
open Set
open scoped Topology
noncomputable section
namespace ClassFieldTower.Cohomology.ProfiniteInteger
open ProCGroups
open ProCGroups.FreeProCdef integersMap : Multiplicative ℤ →ₜ* ClassFormation.ZHatMul where
toMonoidHom := AddMonoidHom.toMultiplicative
(Int.castRingHom ClassFormation.ZHat).toAddMonoidHom
continuous_toFun := continuous_of_discreteTopologyThe integer map sends n to the n-th power of the canonical generator.
Surrounding namespaces, section variables, and local commands at this declaration.
open Set
open scoped Topology
noncomputable section
namespace ClassFieldTower.Cohomology.ProfiniteInteger
open ProCGroups
open ProCGroups.FreeProCtheorem integersMap_apply (n : ℤ) :
integersMap (Multiplicative.ofAdd n) = generator ^ nThe image of the integers is dense in the profinite integers.
Surrounding namespaces, section variables, and local commands at this declaration.
open Set
open scoped Topology
noncomputable section
namespace ClassFieldTower.Cohomology.ProfiniteInteger
open ProCGroups
open ProCGroups.FreeProCtheorem denseRange_integersMap : DenseRange integersMapSurrounding namespaces, section variables, and local commands at this declaration.
open Set
open scoped Topology
noncomputable section
namespace ClassFieldTower.Cohomology.ProfiniteInteger
open ProCGroups
open ProCGroups.FreeProCdef reductionMul (n : ℕ) (hn : 0 < n) :
ClassFormation.ZHatMul →ₜ* Multiplicative (ZMod n) where
toFun z := Multiplicative.ofAdd (ClassFormation.zHatReduction n hn z.toAdd)
map_one' := by
apply Multiplicative.ext
exact map_zero (ClassFormation.zHatReduction n hn)
map_mul' x y := by
apply Multiplicative.ext
exact map_add (ClassFormation.zHatReduction n hn) x.toAdd y.toAdd
continuous_toFun := map_continuous (ClassFormation.zHatReduction n hn)Surrounding namespaces, section variables, and local commands at this declaration.
open Set
open scoped Topology
noncomputable section
namespace ClassFieldTower.Cohomology.ProfiniteInteger
open ProCGroups
open ProCGroups.FreeProCdef cyclicIntHom {K : Type} [Group K] (k : K) :
ℤ →+ Additive (Subgroup.zpowers k) where
toFun z := Additive.ofMul ⟨k ^ z, z, rfl⟩
map_zero' := by
apply Additive.ext
ext
simp only [zpow_zero, toMul_ofMul, toMul_zero, OneMemClass.coe_one]
map_add' := by
intro a b
apply Additive.ext
ext
simp only [zpow_add, toMul_ofMul, toMul_add, Subgroup.coe_mul]Surrounding namespaces, section variables, and local commands at this declaration.
open Set
open scoped Topology
noncomputable section
namespace ClassFieldTower.Cohomology.ProfiniteInteger
open ProCGroups
open ProCGroups.FreeProCtheorem cyclicIntHom_order {K : Type} [Group K] (k : K) :
cyclicIntHom k (orderOf k) = 0Surrounding namespaces, section variables, and local commands at this declaration.
open Set
open scoped Topology
noncomputable section
namespace ClassFieldTower.Cohomology.ProfiniteInteger
open ProCGroups
open ProCGroups.FreeProCdef cyclicZModHom {K : Type} [Group K] (k : K) :
ZMod (orderOf k) →+ Additive (Subgroup.zpowers k)Surrounding namespaces, section variables, and local commands at this declaration.
open Set
open scoped Topology
noncomputable section
namespace ClassFieldTower.Cohomology.ProfiniteInteger
open ProCGroups
open ProCGroups.FreeProCdef cyclicStageHom {K : Type} [Group K] (k : K) :
Multiplicative (ZMod (orderOf k)) →* KSurrounding namespaces, section variables, and local commands at this declaration.
open Set
open scoped Topology
noncomputable section
namespace ClassFieldTower.Cohomology.ProfiniteInteger
open ProCGroups
open ProCGroups.FreeProCtheorem cyclicStageHom_generator {K : Type} [Group K] (k : K) :
cyclicStageHom k (Multiplicative.ofAdd (1 : ZMod (orderOf k))) = kSurrounding namespaces, section variables, and local commands at this declaration.
open Set
open scoped Topology
noncomputable section
namespace ClassFieldTower.Cohomology.ProfiniteInteger
open ProCGroups
open ProCGroups.FreeProCtheorem reductionMul_generator (n : ℕ) (hn : 0 < n) :
reductionMul n hn generator = Multiplicative.ofAdd (1 : ZMod n)Surrounding namespaces, section variables, and local commands at this declaration.
open Set
open scoped Topology
noncomputable section
namespace ClassFieldTower.Cohomology.ProfiniteInteger
open ProCGroups
open ProCGroups.FreeProCdef finiteLift
{Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
[Finite Q] [DiscreteTopology Q]
(φ : Multiplicative ℤ →ₜ* Q) : ClassFormation.ZHatMul →ₜ* QSurrounding namespaces, section variables, and local commands at this declaration.
open Set
open scoped Topology
noncomputable section
namespace ClassFieldTower.Cohomology.ProfiniteInteger
open ProCGroups
open ProCGroups.FreeProCtheorem finiteLift_generator
{Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
[Finite Q] [DiscreteTopology Q]
(φ : Multiplicative ℤ →ₜ* Q) :
finiteLift φ generator = φ (Multiplicative.ofAdd (1 : ℤ))Surrounding namespaces, section variables, and local commands at this declaration.
open Set
open scoped Topology
noncomputable section
namespace ClassFieldTower.Cohomology.ProfiniteInteger
open ProCGroups
open ProCGroups.FreeProCtheorem hom_from_multiplicativeInt_apply
{Q : Type} [Group Q] (φ : Multiplicative ℤ →* Q) (n : ℤ) :
φ (Multiplicative.ofAdd n) =
(φ (Multiplicative.ofAdd (1 : ℤ))) ^ nSurrounding namespaces, section variables, and local commands at this declaration.
open Set
open scoped Topology
noncomputable section
namespace ClassFieldTower.Cohomology.ProfiniteInteger
open ProCGroups
open ProCGroups.FreeProCtheorem finiteLift_comp_integersMap
{Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
[Finite Q] [DiscreteTopology Q]
(φ : Multiplicative ℤ →ₜ* Q) :
(finiteLift φ).comp integersMap = φEvery map from the infinite cyclic group to a finite discrete group extends uniquely over the profinite integers.
Surrounding namespaces, section variables, and local commands at this declaration.
open Set
open scoped Topology
noncomputable section
namespace ClassFieldTower.Cohomology.ProfiniteInteger
open ProCGroups
open ProCGroups.FreeProCtheorem existsUnique_finiteLift
{Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q]
[Finite Q] [DiscreteTopology Q]
(φ : Multiplicative ℤ →ₜ* Q) :
∃! f : ClassFormation.ZHatMul →ₜ* Q, f.comp integersMap = φThe concrete profinite integers are the pro-all-finite completion of the infinite cyclic group.
Surrounding namespaces, section variables, and local commands at this declaration.
open Set
open scoped Topology
noncomputable section
namespace ClassFieldTower.Cohomology.ProfiniteInteger
open ProCGroups
open ProCGroups.FreeProCtheorem isProfiniteCompletion :
ProCGroups.Completion.IsProCCompletion
ProCGroups.FiniteGroupClass.allFinite (Multiplicative ℤ)
ClassFormation.ZHatMul integersMapThe multiplicative profinite integers are free on their canonical generator for the all-finite class.
Surrounding namespaces, section variables, and local commands at this declaration.
open Set
open scoped Topology
noncomputable section
namespace ClassFieldTower.Cohomology.ProfiniteInteger
open ProCGroups
open ProCGroups.FreeProCtheorem isFreeProfinite :
IsFreeProCGroup
(C := ProCGroups.FiniteGroupClass.allFinite)
(Function.const PUnit generator)