NYLL
Module

RealProPStageRestriction.lean

Nyll.SawinTotallyRealTowers.RealProPStageRestriction
5 declarations indexed from sourceView source ↗

Module documentation

Absolute restriction and finite arithmetic stages

The actual finite quotient is continuously identified with the Galois group of its lifted fixed field. Its restriction map agrees with restriction from the fixed algebraic closure, by the actions of both maps on every field element.

Imports11
Imported by5

Declarations

def

quotientToDiscreteMap

L36 ↗
ClassFieldTower.Sawin.quotientToDiscreteMap
Source context 5 commands

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

open scoped NumberField Topology
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich ClassFieldTower.Cohomology ProCGroups
Lean source · statement
def quotientToDiscreteMap
    {G H : Type} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G]
    [Group H] [TopologicalSpace H]
    (U : OpenNormalSubgroup G) (f : (G ⧸ (U : Subgroup G)) →* H) : G →ₜ* H
def

quotientDiscreteEquiv

L47 ↗
ClassFieldTower.Sawin.quotientDiscreteEquiv
Source context 5 commands

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

open scoped NumberField Topology
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich ClassFieldTower.Cohomology ProCGroups
Lean source · statement
def quotientDiscreteEquiv
    {G H : Type} [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G]
    [Group H] [TopologicalSpace H] [DiscreteTopology H]
    (U : OpenNormalSubgroup G) (e : (G ⧸ (U : Subgroup G)) ≃* H) :
    (G ⧸ (U : Subgroup G)) ≃ₜ* H
def

realProPOpenNormalQuotientContinuousEquivStage

L61 ↗
ClassFieldTower.Sawin.realProPOpenNormalQuotientContinuousEquivStage
Documentation

The finite open normal quotient and its actual arithmetic Galois group are continuously isomorphic.

Source context 5 commands

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

open scoped NumberField Topology
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich ClassFieldTower.Cohomology ProCGroups
Lean source · statement
def realProPOpenNormalQuotientContinuousEquivStage
    (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (U : OpenNormalSubgroup
      (maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T)) :
    ((maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T) ⧸
      (U : Subgroup _)) ≃ₜ* ((realProPOpenNormalStage p T U).val ≃ₐ[ℚ]
        (realProPOpenNormalStage p T U).val)
def

realProPOpenNormalStageRestriction

L71 ↗
ClassFieldTower.Sawin.realProPOpenNormalStageRestriction
Documentation

Restriction to the actual finite arithmetic layer of an open normal subgroup.

Source context 5 commands

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

open scoped NumberField Topology
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich ClassFieldTower.Cohomology ProCGroups
Lean source · statement
def realProPOpenNormalStageRestriction
    (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (U : OpenNormalSubgroup
      (maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T)) :
    (maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T) →ₜ*
      ((realProPOpenNormalStage p T U).val ≃ₐ[ℚ]
        (realProPOpenNormalStage p T U).val)
theorem

realProPOpenNormalStageRestriction_comp_absolute

L82 ↗
ClassFieldTower.Sawin.realProPOpenNormalStageRestriction_comp_absolute
Documentation

Restriction through the actual maximal field agrees with absolute restriction on its finite arithmetic layer.

Source context 5 commands

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

open scoped NumberField Topology
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
open ClassFieldTower.Martinet.Shafarevich ClassFieldTower.Cohomology ProCGroups
Lean source · statement
theorem realProPOpenNormalStageRestriction_comp_absolute
    (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (U : OpenNormalSubgroup
      (maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T)) :
    (realProPOpenNormalStageRestriction p T U).comp
      (absoluteToMaximalRealProPOutside p T) =
    absoluteFiniteGaloisRestriction ℚ (realProPOpenNormalStage p T U).val

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.