The normalized valuation of the base local field is transported to the actual fixed coefficient group in the separable closure and then embedded in ℤ̂. Its range is proved to be exactly the ordinary integers inside ℤ̂, and the quotients by nℤ are identified with ZMod n. These are the source-producing parts of the Henselian valuation condition.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation
noncomputable section
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K]abbrev GSurrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation
noncomputable section
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K]abbrev A : Rep ℤ (G K)Kˣ is the coefficient group fixed by the distinguished base subgroup of the absolute separable Galois group.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation
noncomputable section
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K]def baseFieldUnitsEquiv :
Additive Kˣ ≃+ ambientFixedAddSubgroup (A K) (baseField (G K))States the theorem baseFieldUnitsEquiv_val.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation
noncomputable section
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K]
omit [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] intheorem baseFieldUnitsEquiv_val (x : Kˣ) :
((Additive.toMul
((baseFieldUnitsEquiv K (Additive.ofMul x)).1 :
Additive (SeparableClosure K)ˣ) : (SeparableClosure K)ˣ) :
SeparableClosure K) = algebraMap K (SeparableClosure K) (x : K)The normalized valuation v_K : Kˣ → ℤ, embedded in ℤ̂ and written on the actual fixed coefficient group.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation
noncomputable section
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K]def localBaseValuation :
ambientFixedAddSubgroup (A K) (baseField (G K)) →+ ZHatStates the theorem localBaseValuation_baseFieldUnitsEquiv.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation
noncomputable section
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K]theorem localBaseValuation_baseFieldUnitsEquiv (x : Additive Kˣ) :
localBaseValuation K (baseFieldUnitsEquiv K x) =
Int.castRingHom ZHat
(LocalFieldTheory.IsNonarchimedeanLocalField.valuationMap K x)The value group is exactly the image of the ordinary integers in the profinite integers.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation
noncomputable section
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K]theorem localBaseValuation_range :
(localBaseValuation K).range =
(Int.castRingHom ZHat).toAddMonoidHom.rangeEvery ordinary integer occurs as a value, as required in the Henselian valuation condition.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation
noncomputable section
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K]theorem intToProCInteger_mem_localBaseValuation_range (m : ℤ) :
Int.castRingHom ZHat m ∈
(localBaseValuation K).rangeReduction modulo n on the actual value group.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation
noncomputable section
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K]def localValueGroupReduction (n : ℕ) (hn : 0 < n) :
(localBaseValuation K).range →+ ZMod nStates the theorem localValueGroupReduction_surjective.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation
noncomputable section
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K]theorem localValueGroupReduction_surjective (n : ℕ) (hn : 0 < n) :
Function.Surjective (localValueGroupReduction K n hn)The kernel of reduction on the value group is precisely nZ.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation
noncomputable section
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K]theorem localValueGroupReduction_ker (n : ℕ) (hn : 0 < n) :
(localValueGroupReduction K n hn).ker =
nsmulWithin (localBaseValuation K).range nThe cyclic quotient condition in the Henselian valuation condition, for the actual local value group.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation
noncomputable section
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K]def localValueGroupQuotientEquivZMod (n : ℕ) (hn : 0 < n) :
((localBaseValuation K).range ⧸
nsmulWithin (localBaseValuation K).range n) ≃+ ZMod nThe inclusion-and-reduction quotient map of the Henselian valuation condition is bijective for the actual local value group.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalClassFieldTheory
open RamificationTheory KummerTheory
open LocalFieldTheory
open ClassFormation
noncomputable section
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K]theorem localCanonicalValueQuotientMap_bijective (n : ℕ) (hn : 0 < n) :
Function.Bijective
(canonicalValueQuotientMap (localBaseValuation K).range n hn)