The field-generic construction is owned by AlgebraicNumberTheory.Galois.AbsoluteAbelianization. This module preserves the established local names as definitional wrappers for downstream users.
Compatibility name for the absolute commutator closure.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
variable (K : Type) [Field K]abbrev localAbsoluteCommutatorClosure :
ClosedSubgroup (intrinsicAbsoluteGalois K)Compatibility instance for normality of the absolute commutator closure.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
variable (K : Type) [Field K]instance localAbsoluteCommutatorClosure_normal :
(localAbsoluteCommutatorClosure K).NormalCompatibility name for the maximal abelian subextension.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
variable (K : Type) [Field K]abbrev localMaximalAbelianExtension :
IntermediateField K (SeparableClosure K)Compatibility instance for the Galois structure on the maximal abelian subextension.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
variable (K : Type) [Field K]instance localMaximalAbelianExtension_isGalois :
IsGalois K (localMaximalAbelianExtension K)Compatibility name for the underlying multiplicative equivalence.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
variable (K : Type) [Field K]abbrev localAbsoluteAbelianizationMulEquiv :
TopologicalAbelianization (intrinsicAbsoluteGalois K) ≃*
Gal(localMaximalAbelianExtension K / K)The compatibility equivalence sends a quotient class to restriction.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
variable (K : Type) [Field K]theorem localAbsoluteAbelianizationMulEquiv_mk
(sigma : intrinsicAbsoluteGalois K) :
localAbsoluteAbelianizationMulEquiv K (QuotientGroup.mk sigma) =
AlgEquiv.restrictNormalHom (localMaximalAbelianExtension K) sigmaCompatibility form of continuity of the multiplicative equivalence.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
variable (K : Type) [Field K]theorem localAbsoluteAbelianizationMulEquiv_continuous :
Continuous (localAbsoluteAbelianizationMulEquiv K)Compatibility name for the canonical topological equivalence.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
variable (K : Type) [Field K]abbrev localAbsoluteAbelianizationEquiv :
TopologicalAbelianization (intrinsicAbsoluteGalois K) ≃ₜ*
Gal(localMaximalAbelianExtension K / K)Compatibility instance for total disconnectedness.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
variable (K : Type) [Field K]instance localAbsoluteTopologicalAbelianization_totallyDisconnectedSpace :
TotallyDisconnectedSpace
(TopologicalAbelianization (intrinsicAbsoluteGalois K))Compatibility instance for the abelian Galois structure.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
variable (K : Type) [Field K]instance localMaximalAbelianExtension_isAbelianGalois :
IsAbelianGalois K (localMaximalAbelianExtension K)