Module

RealProPOpenNormalStage.lean

Nyll.SawinTotallyRealTowers.RealProPOpenNormalStage

9 declarations indexed from sourceView source ↗

Module documentation

Finite arithmetic stages of the real pro-p compositum

An open normal subgroup determines an actual finite Galois fixed field. Lifting it to the chosen algebraic closure gives an admissible finite layer. The quotient is identified with that layer's Galois group. No rank estimate, finite presentation, or infiniteness hypothesis enters this construction.

Imports4

Nyll.SawinTotallyRealTowers.MaximalRealProPOutside
Mathlib.FieldTheory.Galois.Infinite
Mathlib.FieldTheory.Galois.GaloisClosure
Nyll.ProCGroups.Profinite.OpenSubgroups

Imported by8

def

openNormalFiniteGaloisField

L31 ↗

ClassFieldTower.Sawin.openNormalFiniteGaloisField

Documentation

The finite Galois fixed field supplied by an open normal subgroup.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
universe u v
namespace ClassFieldTower.Sawin

Lean source · statement

def openNormalFiniteGaloisField
    (K : Type u) (M : Type v) [Field K] [Field M] [Algebra K M] [IsGalois K M]
    (U : OpenNormalSubgroup (M ≃ₐ[K] M)) : FiniteGaloisIntermediateField K M

theorem

openNormalFiniteGaloisField_toIntermediateField

L49 ↗

ClassFieldTower.Sawin.openNormalFiniteGaloisField_toIntermediateField

Documentation

The constructed intermediate field is the fixed field of the subgroup.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
universe u v
namespace ClassFieldTower.Sawin

Lean source · statement

theorem openNormalFiniteGaloisField_toIntermediateField
    (K : Type u) (M : Type v) [Field K] [Field M] [Algebra K M] [IsGalois K M]
    (U : OpenNormalSubgroup (M ≃ₐ[K] M)) :
    (openNormalFiniteGaloisField K M U).toIntermediateField =
      IntermediateField.fixedField (U : Subgroup (M ≃ₐ[K] M))

def

openNormalQuotientEquivFiniteGaloisField

L56 ↗

ClassFieldTower.Sawin.openNormalQuotientEquivFiniteGaloisField

Documentation

The open normal quotient acts faithfully and fully on its finite fixed field.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
universe u v
namespace ClassFieldTower.Sawin

Lean source · statement

def openNormalQuotientEquivFiniteGaloisField
    (K : Type u) (M : Type v) [Field K] [Field M] [Algebra K M] [IsGalois K M]
    (U : OpenNormalSubgroup (M ≃ₐ[K] M)) :
    ((M ≃ₐ[K] M) ⧸ (U : Subgroup (M ≃ₐ[K] M))) ≃*
      (openNormalFiniteGaloisField K M U ≃ₐ[K] openNormalFiniteGaloisField K M U)

theorem

openNormalQuotientEquivFiniteGaloisField_apply

L67 ↗

ClassFieldTower.Sawin.openNormalQuotientEquivFiniteGaloisField_apply

Documentation

The quotient action agrees with the original automorphism on the fixed field.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
universe u v
namespace ClassFieldTower.Sawin

Lean source · statement

theorem openNormalQuotientEquivFiniteGaloisField_apply
    (K : Type u) (M : Type v) [Field K] [Field M] [Algebra K M] [IsGalois K M]
    (U : OpenNormalSubgroup (M ≃ₐ[K] M)) (σ : M ≃ₐ[K] M)
    (x : openNormalFiniteGaloisField K M U) :
    ((openNormalQuotientEquivFiniteGaloisField K M U
      (QuotientGroup.mk' (U : Subgroup (M ≃ₐ[K] M)) σ) x :
        openNormalFiniteGaloisField K M U) : M) = σ (x : M)

instance

realCompositumGalois

L81 ↗

ClassFieldTower.Sawin.realCompositumGalois

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
universe u v
namespace ClassFieldTower.Sawin

Lean source · statement

instance realCompositumGalois
    (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ))) :
    IsGalois ℚ (maximalRealProPOutside p T)

def

realProPOpenNormalStage

L87 ↗

ClassFieldTower.Sawin.realProPOpenNormalStage

Documentation

The concrete arithmetic layer attached to an open normal subgroup of the maximal real compositum. Its local conditions follow from containment.

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
universe u v
namespace ClassFieldTower.Sawin
private local instance realCompositumGalois
    (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ))) :
    IsGalois ℚ (maximalRealProPOutside p T) := maximalRealProPOutside_isGalois p T

Lean source · statement

def realProPOpenNormalStage
    (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (U : OpenNormalSubgroup
      (maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T)) :
    FiniteRealPExtension p T

theorem

realProPOpenNormalStage_field

L105 ↗

ClassFieldTower.Sawin.realProPOpenNormalStage_field

Documentation

The stage is the lift of the finite fixed field, with no auxiliary choice.

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
universe u v
namespace ClassFieldTower.Sawin
private local instance realCompositumGalois
    (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ))) :
    IsGalois ℚ (maximalRealProPOutside p T) := maximalRealProPOutside_isGalois p T

Lean source · statement

theorem realProPOpenNormalStage_field
    (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (U : OpenNormalSubgroup
      (maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T)) :
    (realProPOpenNormalStage p T U).val.toIntermediateField =
      IntermediateField.lift
        (IntermediateField.fixedField
          (U : Subgroup
            (maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T)))

def

realProPOpenNormalQuotientEquivStage

L116 ↗

ClassFieldTower.Sawin.realProPOpenNormalQuotientEquivStage

Documentation

The quotient group is the Galois group of the constructed admissible layer.

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
universe u v
namespace ClassFieldTower.Sawin
private local instance realCompositumGalois
    (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ))) :
    IsGalois ℚ (maximalRealProPOutside p T) := maximalRealProPOutside_isGalois p T

Lean source · statement

def realProPOpenNormalQuotientEquivStage
    (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (U : OpenNormalSubgroup
      (maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T)) :
    ((maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T) ⧸
      (U : Subgroup
        (maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T))) ≃*
      ((realProPOpenNormalStage p T U).val ≃ₐ[ℚ] (realProPOpenNormalStage p T U).val)

theorem

realProPOpenNormalQuotientEquivStage_apply

L131 ↗

ClassFieldTower.Sawin.realProPOpenNormalQuotientEquivStage_apply

Documentation

The quotient action on the arithmetic stage is the restriction of the original automorphism, transported through the canonical lift.

Source context 6 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
universe u v
namespace ClassFieldTower.Sawin
private local instance realCompositumGalois
    (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ))) :
    IsGalois ℚ (maximalRealProPOutside p T) := maximalRealProPOutside_isGalois p T

Lean source · statement

theorem realProPOpenNormalQuotientEquivStage_apply
    (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (U : OpenNormalSubgroup
      (maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T))
    (σ : maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T)
    (x : (realProPOpenNormalStage p T U).val) :
    ((realProPOpenNormalQuotientEquivStage p T U
      (QuotientGroup.mk' (U : Subgroup
        (maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T)) σ) x :
          (realProPOpenNormalStage p T U).val) : AlgebraicClosure ℚ) =
      (σ ⟨(x : AlgebraicClosure ℚ),
        le_maximalRealProPOutside (realProPOpenNormalStage p T U) x.property⟩ :
          AlgebraicClosure ℚ)

Module documentation

Finite arithmetic stages of the real pro-p compositum

Declarations