Module

MaximalEverywhereUnramifiedProPGalois.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.MaximalEverywhereUnramifiedProPGalois

10 declarations indexed from sourceView source ↗

Module documentation

The Galois group of the maximal everywhere-unramified pro-p extension

The maximal compositum is Galois because each proof-indexed candidate layer is either a finite Galois field or bottom, and arbitrary composita preserve separability and normality. The resulting automorphism group carries only the canonical Krull topology and profinite instances supplied by Mathlib; its pro-p property is deferred to the finite-support argument.

Imports2

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.MaximalEverywhereUnramifiedProP
Mathlib.FieldTheory.Galois.Profinite

Imported by3

theorem

isGalois_candidateLayer

L31 ↗

ClassFieldTower.Martinet.isGalois_candidateLayer

Documentation

For a fixed intermediate field, the proof-indexed candidate layer in the definition of maximalEverywhereUnramifiedProP is Galois. It is the field itself when all candidate properties hold and bottom otherwise.

Source context 4 commands

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

open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet

Lean source · statement

theorem isGalois_candidateLayer
    (F : Type u) [Field F] [NumberField F]
    (p : ℕ) [Fact (Nat.Prime p)]
    (M : IntermediateField F (AlgebraicClosure F)) :
    IsGalois F
      ((⨆ (_ : FiniteDimensional F M)
          (_ : IsGalois F M)
          (_ : IsPGroup p (M ≃ₐ[F] M))
          (_ : NumberField M)
          (_ : IsEverywhereUnramified F M),
        M) : IntermediateField F (AlgebraicClosure F))

theorem

maximalEverywhereUnramifiedProP_isGalois

L68 ↗

ClassFieldTower.Martinet.maximalEverywhereUnramifiedProP_isGalois

Documentation

The maximal everywhere-unramified pro-p compositum is a Galois extension of the base field.

Source context 4 commands

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

open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet

Lean source · statement

theorem maximalEverywhereUnramifiedProP_isGalois
    (F : Type u) [Field F] [NumberField F]
    (p : ℕ) [Fact (Nat.Prime p)] :
    IsGalois F (maximalEverywhereUnramifiedProP F p)

instance

instIsGalois

L93 ↗

ClassFieldTower.Martinet.maximalEverywhereUnramifiedProP.instIsGalois

Documentation

The canonical Galois instance for the maximal compositum.

Source context 4 commands

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

open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet

Lean source · statement

instance maximalEverywhereUnramifiedProP.instIsGalois
    (F : Type u) [Field F] [NumberField F]
    (p : ℕ) [Fact (Nat.Prime p)] :
    IsGalois F (maximalEverywhereUnramifiedProP F p)

def

MaxEverywhereUnramifiedProPGaloisGroup

L101 ↗

ClassFieldTower.Martinet.MaxEverywhereUnramifiedProPGaloisGroup

Documentation

The automorphism group of the maximal everywhere-unramified pro-p compositum. Its pro-p property is established only after finite support.

Source context 4 commands

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

open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet

Lean source · statement

def MaxEverywhereUnramifiedProPGaloisGroup
    (F : Type u) [Field F] [NumberField F]
    (p : ℕ) [Fact (Nat.Prime p)] : Type u

instance

instGroup

L108 ↗

ClassFieldTower.Martinet.MaxEverywhereUnramifiedProPGaloisGroup.instGroup

Documentation

The canonical group structure inherited from algebra automorphisms.

Source context 4 commands

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

open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet

Lean source · statement

instance MaxEverywhereUnramifiedProPGaloisGroup.instGroup
    (F : Type u) [Field F] [NumberField F]
    (p : ℕ) [Fact (Nat.Prime p)] :
    Group (MaxEverywhereUnramifiedProPGaloisGroup F p)

instance

instTopologicalSpace

L117 ↗

ClassFieldTower.Martinet.MaxEverywhereUnramifiedProPGaloisGroup.instTopologicalSpace

Documentation

The canonical Krull topology inherited from algebra automorphisms.

Source context 4 commands

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

open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet

Lean source · statement

instance MaxEverywhereUnramifiedProPGaloisGroup.instTopologicalSpace
    (F : Type u) [Field F] [NumberField F]
    (p : ℕ) [Fact (Nat.Prime p)] :
    TopologicalSpace (MaxEverywhereUnramifiedProPGaloisGroup F p)

instance

instIsTopologicalGroup

L126 ↗

ClassFieldTower.Martinet.MaxEverywhereUnramifiedProPGaloisGroup.instIsTopologicalGroup

Documentation

The canonical topological-group structure for the Krull topology.

Source context 4 commands

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

open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet

Lean source · statement

instance MaxEverywhereUnramifiedProPGaloisGroup.instIsTopologicalGroup
    (F : Type u) [Field F] [NumberField F]
    (p : ℕ) [Fact (Nat.Prime p)] :
    IsTopologicalGroup (MaxEverywhereUnramifiedProPGaloisGroup F p)

instance

instCompactSpace

L135 ↗

ClassFieldTower.Martinet.MaxEverywhereUnramifiedProPGaloisGroup.instCompactSpace

Documentation

Compactness inherited from the profinite Galois-group construction.

Source context 4 commands

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

open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet

Lean source · statement

instance MaxEverywhereUnramifiedProPGaloisGroup.instCompactSpace
    (F : Type u) [Field F] [NumberField F]
    (p : ℕ) [Fact (Nat.Prime p)] :
    CompactSpace (MaxEverywhereUnramifiedProPGaloisGroup F p)

instance

instT2Space

L144 ↗

ClassFieldTower.Martinet.MaxEverywhereUnramifiedProPGaloisGroup.instT2Space

Documentation

Hausdorffness inherited from the Krull topology.

Source context 4 commands

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

open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet

Lean source · statement

instance MaxEverywhereUnramifiedProPGaloisGroup.instT2Space
    (F : Type u) [Field F] [NumberField F]
    (p : ℕ) [Fact (Nat.Prime p)] :
    T2Space (MaxEverywhereUnramifiedProPGaloisGroup F p)

instance

instTotallyDisconnectedSpace

L153 ↗

ClassFieldTower.Martinet.MaxEverywhereUnramifiedProPGaloisGroup.instTotallyDisconnectedSpace

Documentation

Total disconnectedness inherited from the Krull topology.

Source context 4 commands

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

open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet

Lean source · statement

instance MaxEverywhereUnramifiedProPGaloisGroup.instTotallyDisconnectedSpace
    (F : Type u) [Field F] [NumberField F]
    (p : ℕ) [Fact (Nat.Prime p)] :
    TotallyDisconnectedSpace
      (MaxEverywhereUnramifiedProPGaloisGroup F p)

Module documentation

The Galois group of the maximal everywhere-unramified pro-p extension

Declarations