For a field containing a primitive n-th root of unity, this file identifies K× / K×ⁿ with continuous characters of the absolute Galois group. The target is first the discrete group of n-th roots of unity and is then identified with the discrete multiplicative group underlying ZMod n.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K]abbrev AbsoluteRadicalDatum (n : ℕ+)Every base-field unit has an n-th root in the algebraic closure.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K]theorem finiteKummerRadicalSubgroup_algebraicClosure_eq_top (n : ℕ+) :
finiteKummerRadicalSubgroup (K := K) (L := AlgebraicClosure K) n = ⊤The full unit group is multiplicatively equivalent to the actual radical subgroup in the algebraic closure.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K]def unitsEquivAbsoluteRadicalCarrier (n : ℕ+) :
Kˣ ≃* (AbsoluteRadicalDatum K n).carrierSurrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K]theorem map_powerRange_unitsEquivAbsoluteRadicalCarrier (n : ℕ+) :
(powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range.map
(unitsEquivAbsoluteRadicalCarrier K n).toMonoidHom =
(AbsoluteRadicalDatum K n).ambientNthPowersSubgroupThe ordinary power-class group is canonically the radical quotient used by the infinite Kummer character theorem over the algebraic closure.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K]def absolutePowerClassEquivRadicalQuotient (n : ℕ+) :
Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range ≃*
(AbsoluteRadicalDatum K n).RadicalQuotientAbsolute Kummer theory with its natural roots-of-unity target.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K]def absoluteKummerContinuousNthRootsCharacterEquiv
[CharZero K]
(n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range ≃*
(Field.absoluteGaloisGroup K →ₜ*
DiscreteNthRootsSubgroup (AlgebraicClosure K) (n : ℕ))Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K]def nthRootsSubgroupEquivMultiplicativeZMod
(n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
nthRootsSubgroup (AlgebraicClosure K) (n : ℕ) ≃*
Multiplicative (ZMod (n : ℕ))Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K]instance discreteMultiplicativeZModTopologicalSpace (n : ℕ) :
TopologicalSpace (Multiplicative (ZMod n))Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K]
local instance discreteMultiplicativeZModTopologicalSpace (n : ℕ) :
TopologicalSpace (Multiplicative (ZMod n)) := ⊥instance discreteMultiplicativeZModDiscreteTopology (n : ℕ) :
DiscreteTopology (Multiplicative (ZMod n))Choosing a primitive root in K identifies discrete roots of unity in its algebraic closure with the discrete multiplicative group underlying ZMod n.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K]
local instance discreteMultiplicativeZModTopologicalSpace (n : ℕ) :
TopologicalSpace (Multiplicative (ZMod n)) := ⊥
local instance discreteMultiplicativeZModDiscreteTopology (n : ℕ) :
DiscreteTopology (Multiplicative (ZMod n)) :=
discreteTopology_bot _def discreteNthRootsContinuousMulEquivMultiplicativeZMod
(n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
DiscreteNthRootsSubgroup (AlgebraicClosure K) (n : ℕ) ≃ₜ*
Multiplicative (ZMod (n : ℕ)) where
__ := nthRootsSubgroupEquivMultiplicativeZMod K n hmu
continuous_toFun := continuous_of_discreteTopology
continuous_invFun := continuous_of_discreteTopologySurrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K]
local instance discreteMultiplicativeZModTopologicalSpace (n : ℕ) :
TopologicalSpace (Multiplicative (ZMod n)) := ⊥
local instance discreteMultiplicativeZModDiscreteTopology (n : ℕ) :
DiscreteTopology (Multiplicative (ZMod n)) :=
discreteTopology_bot _def continuousCharacterCongrRight
{G A B : Type*} [Group G] [TopologicalSpace G]
[CommGroup A] [TopologicalSpace A] [IsTopologicalGroup A]
[CommGroup B] [TopologicalSpace B] [IsTopologicalGroup B]
(e : A ≃ₜ* B) :
(G →ₜ* A) ≃* (G →ₜ* B) where
toFun f :=
⟨e.toMulEquiv.toMonoidHom.comp f.toMonoidHom,
e.continuous.comp f.continuous⟩
invFun f :=
⟨e.symm.toMulEquiv.toMonoidHom.comp f.toMonoidHom,
e.symm.continuous.comp f.continuous⟩
left_inv f := by
ext g
exact e.symm_apply_apply (f g)
right_inv f := by
ext g
exact e.apply_symm_apply (f g)
map_mul' f g := by
ext x
exact map_mul e (f x) (g x)Absolute Kummer theory in the mod-n character convention used by the continuous degree-one cohomology API.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open KummerTheory
variable (K : Type*) [Field K]
local instance discreteMultiplicativeZModTopologicalSpace (n : ℕ) :
TopologicalSpace (Multiplicative (ZMod n)) := ⊥
local instance discreteMultiplicativeZModDiscreteTopology (n : ℕ) :
DiscreteTopology (Multiplicative (ZMod n)) :=
discreteTopology_bot _def absoluteKummerContinuousZModCharacterEquiv
[CharZero K]
(n : ℕ+) (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
Kˣ ⧸ (powMonoidHom (n : ℕ) : Kˣ →* Kˣ).range ≃*
(Field.absoluteGaloisGroup K →ₜ* Multiplicative (ZMod (n : ℕ)))