NYLL
Module

RealProPDepthStage.lean

Nyll.SawinTotallyRealTowers.RealProPDepthStage
2 declarations indexed from sourceView source ↗

Module documentation

Finite arithmetic stages detecting source depth

An actual quotient of a finitely generated profinite group admits finite arithmetic stages such that every element trivial on that stage has a lift of any prescribed augmentation depth in the source.

Imports6
Imported by2

Declarations

theorem

realProPOpenNormalStageRestriction_eq_one_iff

L33 ↗
ClassFieldTower.Sawin.realProPOpenNormalStageRestriction_eq_one_iff
Documentation

Restriction to the arithmetic stage detects precisely the selected open normal subgroup of the actual maximal real Galois group.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTower.Sawin
open ClassFieldTower.ProP ProCGroups.FiniteGeneration
universe u
Lean source · statement
theorem realProPOpenNormalStageRestriction_eq_one_iff
    (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    (U : OpenNormalSubgroup
      (maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T))
    (g : maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T) :
    realProPOpenNormalStageRestriction p T U g = 1 ↔ g ∈ U
theorem

exists_realProPOpenNormalStage_with_zassenhaus_lifts

L46 ↗
ClassFieldTower.Sawin.exists_realProPOpenNormalStage_with_zassenhaus_lifts
Documentation

A finite arithmetic layer is constructed so that every element trivial on that layer has a source lift of the requested depth.

Source context 5 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace ClassFieldTower.Sawin
open ClassFieldTower.ProP ProCGroups.FiniteGeneration
universe u
Lean source · statement
theorem exists_realProPOpenNormalStage_with_zassenhaus_lifts
    (p : ℕ) [Fact p.Prime] (T : Set (HeightOneSpectrum (𝓞 ℚ)))
    {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
    [CompactSpace F] [T2Space F] [TotallyDisconnectedSpace F]
    (hfg : TopologicallyFinitelyGenerated F)
    (q : F →ₜ* (maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T))
    (hq : Function.Surjective q) (n : ℕ) :
    ∃ U : OpenNormalSubgroup
      (maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T),
      ∀ g : maximalRealProPOutside p T ≃ₐ[ℚ] maximalRealProPOutside p T,
        realProPOpenNormalStageRestriction p T U g = 1 →
          ∃ f : F, q f = g ∧ ZassenhausDepthAtLeast p n f

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