Every open normal subgroup of the profinite topological abelianization of the absolute Galois group determines a finite abelian subextension of the fixed separable closure. The corresponding finite quotient is canonically identified, as a topological group, with the actual Galois group of that subextension.
The absolute topological abelianization, regarded as a stable profinite group.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K]def localAbsoluteAbelianProfinite : ProfiniteGrpSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K]instance localAbsoluteAbelianProfiniteCommGroup :
CommGroup (localAbsoluteAbelianProfinite K)The quotient map from the absolute Galois group to its topological abelianization.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K]
local instance localAbsoluteAbelianProfiniteCommGroup :
CommGroup (localAbsoluteAbelianProfinite K) := by
change CommGroup (TopologicalAbelianization (intrinsicAbsoluteGalois K))
infer_instancedef localAbsoluteAbelianizationQuotientMap :
intrinsicAbsoluteGalois K →*
localAbsoluteAbelianProfinite KThe open normal preimage in the absolute Galois group of an open normal subgroup of its topological abelianization.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K]
local instance localAbsoluteAbelianProfiniteCommGroup :
CommGroup (localAbsoluteAbelianProfinite K) := by
change CommGroup (TopologicalAbelianization (intrinsicAbsoluteGalois K))
infer_instancedef absoluteFiniteQuotientPreimage
(N : OpenNormalSubgroup (localAbsoluteAbelianProfinite K)) :
OpenNormalSubgroup (intrinsicAbsoluteGalois K) where
toSubgroup := N.toSubgroup.comap
(localAbsoluteAbelianizationQuotientMap K)
isOpen' := N.isOpen'.preimage QuotientGroup.continuous_mk
isNormal' := by infer_instanceThe same preimage, packaged as a closed subgroup for infinite Galois correspondence.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K]
local instance localAbsoluteAbelianProfiniteCommGroup :
CommGroup (localAbsoluteAbelianProfinite K) := by
change CommGroup (TopologicalAbelianization (intrinsicAbsoluteGalois K))
infer_instancedef absoluteFiniteQuotientClosedPreimage
(N : OpenNormalSubgroup (localAbsoluteAbelianProfinite K)) :
ClosedSubgroup (intrinsicAbsoluteGalois K) where
toSubgroup := (absoluteFiniteQuotientPreimage K N).toSubgroup
isClosed' := Subgroup.isClosed_of_isOpen _
(absoluteFiniteQuotientPreimage K N).isOpen'The closed preimage of an open normal subgroup in the abelianization is normal.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K]
local instance localAbsoluteAbelianProfiniteCommGroup :
CommGroup (localAbsoluteAbelianProfinite K) := by
change CommGroup (TopologicalAbelianization (intrinsicAbsoluteGalois K))
infer_instanceinstance absoluteFiniteQuotientClosedPreimage_normal
(N : OpenNormalSubgroup (localAbsoluteAbelianProfinite K)) :
(absoluteFiniteQuotientClosedPreimage K N).NormalThe finite subextension cut out by an open normal subgroup of the absolute topological abelianization.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K]
local instance localAbsoluteAbelianProfiniteCommGroup :
CommGroup (localAbsoluteAbelianProfinite K) := by
change CommGroup (TopologicalAbelianization (intrinsicAbsoluteGalois K))
infer_instancedef absoluteFiniteQuotientField
(N : OpenNormalSubgroup (localAbsoluteAbelianProfinite K)) :
IntermediateField K (SeparableClosure K)The fixed field attached to an open finite abelian quotient is Galois over K.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K]
local instance localAbsoluteAbelianProfiniteCommGroup :
CommGroup (localAbsoluteAbelianProfinite K) := by
change CommGroup (TopologicalAbelianization (intrinsicAbsoluteGalois K))
infer_instanceinstance absoluteFiniteQuotientField_isGalois
(N : OpenNormalSubgroup (localAbsoluteAbelianProfinite K)) :
IsGalois K (absoluteFiniteQuotientField K N)The fixed field attached to an open finite quotient is finite-dimensional over K.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K]
local instance localAbsoluteAbelianProfiniteCommGroup :
CommGroup (localAbsoluteAbelianProfinite K) := by
change CommGroup (TopologicalAbelianization (intrinsicAbsoluteGalois K))
infer_instanceinstance absoluteFiniteQuotientField_finiteDimensional
(N : OpenNormalSubgroup (localAbsoluteAbelianProfinite K)) :
FiniteDimensional K (absoluteFiniteQuotientField K N)The topological commutator closure is contained in every pulled-back open normal subgroup.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K]
local instance localAbsoluteAbelianProfiniteCommGroup :
CommGroup (localAbsoluteAbelianProfinite K) := by
change CommGroup (TopologicalAbelianization (intrinsicAbsoluteGalois K))
infer_instancetheorem localAbsoluteCommutatorClosure_le_finiteQuotientPreimage
(N : OpenNormalSubgroup (localAbsoluteAbelianProfinite K)) :
(commutator (intrinsicAbsoluteGalois K)).topologicalClosure ≤
(absoluteFiniteQuotientPreimage K N).toSubgroupPullback followed by image under the abelianization quotient recovers the original open normal subgroup.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K]
local instance localAbsoluteAbelianProfiniteCommGroup :
CommGroup (localAbsoluteAbelianProfinite K) := by
change CommGroup (TopologicalAbelianization (intrinsicAbsoluteGalois K))
infer_instancetheorem finiteQuotientPreimage_map_eq
(N : OpenNormalSubgroup (localAbsoluteAbelianProfinite K)) :
(absoluteFiniteQuotientPreimage K N).toSubgroup.map
(localAbsoluteAbelianizationQuotientMap K) =
N.toSubgroupMapping the quotient preimage into the abelianization produces a normal subgroup.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K]
local instance localAbsoluteAbelianProfiniteCommGroup :
CommGroup (localAbsoluteAbelianProfinite K) := by
change CommGroup (TopologicalAbelianization (intrinsicAbsoluteGalois K))
infer_instanceinstance absoluteFiniteQuotientPreimageMap_normal
(N : OpenNormalSubgroup (localAbsoluteAbelianProfinite K)) :
((absoluteFiniteQuotientPreimage K N).toSubgroup.map
(localAbsoluteAbelianizationQuotientMap K)).NormalThe algebraic finite quotient identification, obtained from the third isomorphism theorem and infinite Galois correspondence.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K]
local instance localAbsoluteAbelianProfiniteCommGroup :
CommGroup (localAbsoluteAbelianProfinite K) := by
change CommGroup (TopologicalAbelianization (intrinsicAbsoluteGalois K))
infer_instancedef absoluteFiniteQuotientMulEquiv
(N : OpenNormalSubgroup (localAbsoluteAbelianProfinite K)) :
localAbsoluteAbelianProfinite K ⧸ N.toSubgroup ≃*
Gal(absoluteFiniteQuotientField K N / K)The canonical topological finite quotient identification.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K]
local instance localAbsoluteAbelianProfiniteCommGroup :
CommGroup (localAbsoluteAbelianProfinite K) := by
change CommGroup (TopologicalAbelianization (intrinsicAbsoluteGalois K))
infer_instancedef absoluteFiniteQuotientEquiv
(N : OpenNormalSubgroup (localAbsoluteAbelianProfinite K)) :
localAbsoluteAbelianProfinite K ⧸ N.toSubgroup ≃ₜ*
Gal(absoluteFiniteQuotientField K N / K)On representatives, the finite quotient identification is literal restriction to the corresponding fixed field.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K]
local instance localAbsoluteAbelianProfiniteCommGroup :
CommGroup (localAbsoluteAbelianProfinite K) := by
change CommGroup (TopologicalAbelianization (intrinsicAbsoluteGalois K))
infer_instancetheorem absoluteFiniteQuotientEquiv_mk_mk
(N : OpenNormalSubgroup (localAbsoluteAbelianProfinite K))
(σ : intrinsicAbsoluteGalois K) :
absoluteFiniteQuotientEquiv K N
(QuotientGroup.mk
(QuotientGroup.mk σ : localAbsoluteAbelianProfinite K)) =
AlgEquiv.restrictNormalHom (absoluteFiniteQuotientField K N) σThe fixed field attached to a finite quotient of the abelianization is abelian Galois.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace LocalClassFieldTheory
open LocalFieldTheory RamificationTheory
variable (K : Type) [Field K]
local instance localAbsoluteAbelianProfiniteCommGroup :
CommGroup (localAbsoluteAbelianProfinite K) := by
change CommGroup (TopologicalAbelianization (intrinsicAbsoluteGalois K))
infer_instanceinstance absoluteFiniteQuotientField_isAbelianGalois
(N : OpenNormalSubgroup (localAbsoluteAbelianProfinite K)) :
IsAbelianGalois K (absoluteFiniteQuotientField K N)