This module packages the absolute Galois group of a field, its integral unit representation, and its distinguished abstract base field using the chosen separable closure.
The absolute Galois group of a field, formed using its chosen separable closure.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open RamificationTheory CyclicCohomology KummerTheory
open ClassFormationabbrev intrinsicAbsoluteGalois
(F : Type) [Field F]The integral representation of the intrinsic absolute Galois group on the units of the chosen separable closure.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open RamificationTheory CyclicCohomology KummerTheory
open ClassFormationabbrev intrinsicAbsoluteUnits
(F : Type) [Field F] :
Rep ℤ (intrinsicAbsoluteGalois F)The closed base subgroup of the intrinsic absolute Galois group, expressed as the fixing subgroup of the bottom intermediate field.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open RamificationTheory CyclicCohomology KummerTheory
open ClassFormationabbrev intrinsicAbstractBase
(F : Type) [Field F] :
ClosedSubgroup (intrinsicAbsoluteGalois F)The canonical equivalence from the intrinsic abstract base subgroup to the full absolute Galois group.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open RamificationTheory CyclicCohomology KummerTheory
open ClassFormationdef intrinsicAbstractBaseEquivAbsolute
(F : Type) [Field F] :
(intrinsicAbstractBase F).toSubgroup ≃*
intrinsicAbsoluteGalois FThe inverse intrinsic-base equivalence has underlying automorphism equal to the supplied absolute Galois automorphism.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open RamificationTheory CyclicCohomology KummerTheory
open ClassFormationtheorem intrinsicAbstractBaseEquivAbsolute_symm_apply_val
(F : Type) [Field F] (σ : intrinsicAbsoluteGalois F) :
((intrinsicAbstractBaseEquivAbsolute F).symm σ).1 = σThe intrinsic abstract base packaged as a finite abstract field; its defining quotient is the trivial finite quotient.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open RamificationTheory CyclicCohomology KummerTheory
open ClassFormationdef intrinsicFiniteAbstractBase
(F : Type) [Field F] :
FiniteAbstractField (intrinsicAbsoluteGalois F) where
field := intrinsicAbstractBase F
finite := by
rw [intrinsicAbstractBase, closedFixingSubgroup_bot_eq_baseField]
exact (FiniteAbstractField.base (intrinsicAbsoluteGalois F)).finiteThe finite intrinsic base is the distinguished finite base of the abstract class formation.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open RamificationTheory CyclicCohomology KummerTheory
open ClassFormationtheorem intrinsicFiniteAbstractBase_eq_base
(F : Type) [Field F] :
intrinsicFiniteAbstractBase F =
FiniteAbstractField.base (intrinsicAbsoluteGalois F)