Module

AbsoluteRealProPRestriction.lean

Nyll.SawinTotallyRealTowers.AbsoluteRealProPRestriction

10 declarations indexed from sourceView source ↗

Module documentation

Absolute restriction to the maximal real pro-p compositum

The actual ambient inclusion supplies a continuous surjective restriction homomorphism. Its kernel is exactly the subgroup fixing the constructed compositum. The quotient by this kernel is continuously isomorphic to the relative Galois group, providing the concrete quotient for later factorization. No primality or ramification comparison is needed for this Galois boundary.

Imports9

Nyll.SawinTotallyRealTowers.MaximalRealProPOutside
Nyll.ProCGroups.Topologies.ContinuousMulEquiv
Mathlib.FieldTheory.AbsoluteGaloisGroup
Mathlib.FieldTheory.Galois.Basic
Mathlib.FieldTheory.Galois.Profinite
Mathlib.FieldTheory.Normal.Basic
Mathlib.FieldTheory.Normal.Defs
Mathlib.GroupTheory.QuotientGroup.Basic
Mathlib.Topology.Algebra.Group.Quotient

Imported by6

def

normalAbsoluteRestriction

L34 ↗

ClassFieldTower.Sawin.normalAbsoluteRestriction

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin

Lean source · statement

def normalAbsoluteRestriction (F : Type) [Field F]
    (M : IntermediateField F (AlgebraicClosure F)) (hM : Normal F M) :
    Field.absoluteGaloisGroup F →ₜ* (M ≃ₐ[F] M)

theorem

normalAbsoluteRestriction_surjective

L42 ↗

ClassFieldTower.Sawin.normalAbsoluteRestriction_surjective

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin

Lean source · statement

theorem normalAbsoluteRestriction_surjective (F : Type) [Field F]
    (M : IntermediateField F (AlgebraicClosure F)) (hM : Normal F M) :
    Function.Surjective (normalAbsoluteRestriction F M hM)

theorem

normalAbsoluteRestriction_apply

L48 ↗

ClassFieldTower.Sawin.normalAbsoluteRestriction_apply

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin

Lean source · statement

theorem normalAbsoluteRestriction_apply (F : Type) [Field F]
    (M : IntermediateField F (AlgebraicClosure F)) (hM : Normal F M)
    (σ : Field.absoluteGaloisGroup F) (x : M) :
    (normalAbsoluteRestriction F M hM σ x : AlgebraicClosure F) =
      (AlgEquiv.toAlgHom (R := F) (A₁ := AlgebraicClosure F)
        (A₂ := AlgebraicClosure F) σ) (x : AlgebraicClosure F)

theorem

normalAbsoluteRestriction_ker

L57 ↗

ClassFieldTower.Sawin.normalAbsoluteRestriction_ker

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin

Lean source · statement

theorem normalAbsoluteRestriction_ker (F : Type) [Field F]
    (M : IntermediateField F (AlgebraicClosure F)) (hM : Normal F M) :
    (normalAbsoluteRestriction F M hM).toMonoidHom.ker = M.fixingSubgroup

def

absoluteToMaximalRealProPOutside

L65 ↗

ClassFieldTower.Sawin.absoluteToMaximalRealProPOutside

Documentation

Restriction of absolute automorphisms to the constructed maximal real compositum with the given finite ramification support.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin

Lean source · statement

def absoluteToMaximalRealProPOutside (p : ℕ)
    (T : Set (HeightOneSpectrum (𝓞 ℚ))) :
    Field.absoluteGaloisGroup ℚ →ₜ*
      (maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T)

theorem

absoluteToMaximalRealProPOutside_surjective

L74 ↗

ClassFieldTower.Sawin.absoluteToMaximalRealProPOutside_surjective

Documentation

Every automorphism of the maximal real compositum extends to the fixed algebraic closure.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin

Lean source · statement

theorem absoluteToMaximalRealProPOutside_surjective (p : ℕ)
    (T : Set (HeightOneSpectrum (𝓞 ℚ))) :
    Function.Surjective (absoluteToMaximalRealProPOutside p T)

theorem

absoluteToMaximalRealProPOutside_apply

L82 ↗

ClassFieldTower.Sawin.absoluteToMaximalRealProPOutside_apply

Documentation

The restriction acts by the original absolute automorphism on each element of the constructed intermediate field.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin

Lean source · statement

theorem absoluteToMaximalRealProPOutside_apply (p : ℕ)
    (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (σ : Field.absoluteGaloisGroup ℚ) (x : maximalRealProPOutside p T) :
    (absoluteToMaximalRealProPOutside p T σ x : AlgebraicClosure ℚ) =
      (AlgEquiv.toAlgHom (R := ℚ) (A₁ := AlgebraicClosure ℚ)
        (A₂ := AlgebraicClosure ℚ) σ) (x : AlgebraicClosure ℚ)

theorem

absoluteToMaximalRealProPOutside_ker

L93 ↗

ClassFieldTower.Sawin.absoluteToMaximalRealProPOutside_ker

Documentation

The actual restriction kernel is the fixing subgroup of the actual maximal compositum. No separate kernel structure is introduced.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin

Lean source · statement

theorem absoluteToMaximalRealProPOutside_ker (p : ℕ)
    (T : Set (HeightOneSpectrum (𝓞 ℚ))) :
    (absoluteToMaximalRealProPOutside p T).toMonoidHom.ker =
      (maximalRealProPOutside p T).fixingSubgroup

def

absoluteRealProPOutsideQuotientEquiv

L102 ↗

ClassFieldTower.Sawin.absoluteRealProPOutsideQuotientEquiv

Documentation

The quotient by the actual restriction kernel is the relative Galois group as a topological group.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin

Lean source · statement

def absoluteRealProPOutsideQuotientEquiv (p : ℕ)
    (T : Set (HeightOneSpectrum (𝓞 ℚ))) :
    (Field.absoluteGaloisGroup ℚ ⧸
      (absoluteToMaximalRealProPOutside p T).toMonoidHom.ker) ≃ₜ*
      (maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T)

theorem

absoluteRealProPOutsideQuotientEquiv_mk

L124 ↗

ClassFieldTower.Sawin.absoluteRealProPOutsideQuotientEquiv_mk

Documentation

The quotient equivalence sends the class of an absolute automorphism to its restriction.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin

Lean source · statement

theorem absoluteRealProPOutsideQuotientEquiv_mk (p : ℕ)
    (T : Set (HeightOneSpectrum (𝓞 ℚ))) (σ : Field.absoluteGaloisGroup ℚ) :
    absoluteRealProPOutsideQuotientEquiv p T
      (QuotientGroup.mk' (absoluteToMaximalRealProPOutside p T).toMonoidHom.ker σ) =
        absoluteToMaximalRealProPOutside p T σ

Module documentation

Absolute restriction to the maximal real pro-p compositum

Declarations