Restriction from the absolute Galois group to the maximal everywhere-unramified pro-p extension is a continuous quotient map. Its closed normal kernel is the subgroup fixing that extension, and quotienting by the kernel gives a continuous group equivalence with the relative Galois group.
The construction is valid for every prime p; no oddness assumption is needed for this Galois- theoretic step.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]abbrev MSurrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]instance absoluteGaloisGroup_compactSpace :
CompactSpace (Field.absoluteGaloisGroup F)Restriction of absolute automorphisms to the maximal everywhere-unramified pro-p extension.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]def absoluteToMaxEverywhereUnramifiedProP :
Field.absoluteGaloisGroup F →ₜ*
MaxEverywhereUnramifiedProPGaloisGroup F p where
toMonoidHom := AlgEquiv.restrictNormalHom (M F p)
continuous_toFun := InfiniteGalois.restrictNormalHom_continuous (M F p)Absolute restriction onto the maximal everywhere-unramified pro-p Galois group is surjective.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]theorem absoluteToMaxEverywhereUnramifiedProP_surjective :
Function.Surjective (absoluteToMaxEverywhereUnramifiedProP F p)The closed subgroup of the absolute Galois group fixing the maximal everywhere-unramified pro-p extension.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]def absoluteUnramifiedKernel : ClosedSubgroup (Field.absoluteGaloisGroup F) where
toSubgroup := (M F p).fixingSubgroup
isClosed' := InfiniteGalois.fixingSubgroup_isClosed (M F p)The kernel of absolute restriction is exactly the fixing subgroup of the maximal everywhere-unramified pro-p extension.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]theorem absoluteToMaxEverywhereUnramifiedProP_ker :
(absoluteToMaxEverywhereUnramifiedProP F p).toMonoidHom.ker =
(absoluteUnramifiedKernel F p).toSubgroupThe absolute unramified kernel is normal.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]instance absoluteUnramifiedKernel_normal :
(absoluteUnramifiedKernel F p).NormalContinuous inclusion of the absolute unramified kernel.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]def absoluteUnramifiedKernelInclusion :
absoluteUnramifiedKernel F p →ₜ* Field.absoluteGaloisGroup F where
toMonoidHom := (absoluteUnramifiedKernel F p).toSubgroup.subtype
continuous_toFun := continuous_subtype_valInclusion of the absolute unramified kernel is injective.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]theorem absoluteUnramifiedKernelInclusion_injective :
Function.Injective (absoluteUnramifiedKernelInclusion F p)The kernel inclusion followed by absolute restriction is exact in the multiplicative sense.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]theorem absoluteUnramifiedGaloisSequence_mulExact :
Function.MulExact (absoluteUnramifiedKernelInclusion F p)
(absoluteToMaxEverywhereUnramifiedProP F p)Algebraic quotient equivalence induced by absolute restriction.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]def absoluteUnramifiedQuotientMulEquiv :
Field.absoluteGaloisGroup F ⧸
(absoluteUnramifiedKernel F p).toSubgroup ≃*
MaxEverywhereUnramifiedProPGaloisGroup F pThe quotient equivalence sends the class of an absolute automorphism to its restriction.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]theorem absoluteUnramifiedQuotientMulEquiv_mk
(σ : Field.absoluteGaloisGroup F) :
absoluteUnramifiedQuotientMulEquiv F p (QuotientGroup.mk σ) =
absoluteToMaxEverywhereUnramifiedProP F p σThe algebraic quotient equivalence is continuous.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]theorem absoluteUnramifiedQuotientMulEquiv_continuous :
Continuous (absoluteUnramifiedQuotientMulEquiv F p)The quotient of the absolute Galois group by the closed fixing subgroup is continuously equivalent to the maximal everywhere-unramified pro-p Galois group.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]def absoluteUnramifiedQuotientContinuousMulEquiv :
Field.absoluteGaloisGroup F ⧸
(absoluteUnramifiedKernel F p).toSubgroup ≃ₜ*
MaxEverywhereUnramifiedProPGaloisGroup F p