Module

MaximalEverywhereUnramifiedProP.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.MaximalEverywhereUnramifiedProP

5 declarations indexed from sourceView source ↗

Module documentation

The maximal everywhere-unramified pro-p subextension

Inside a fixed algebraic closure of a number field, this file forms the compositum of all finite Galois everywhere-unramified intermediate fields whose automorphism group is a p-group. The results here are the lattice universal properties of that compositum; finite-support and Galois properties of the resulting infinite extension belong to later leaves.

Imports2

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.EverywhereUnramifiedBridge
Mathlib.GroupTheory.PGroup

Imported by4

def

maximalEverywhereUnramifiedProP

L32 ↗

ClassFieldTower.Martinet.maximalEverywhereUnramifiedProP

Documentation

The compositum, inside AlgebraicClosure F, of all finite Galois everywhere-unramified extensions of F with p-group Galois group.

The binder order matches the corresponding trusted LeanEval definition.

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 maximalEverywhereUnramifiedProP
    (F : Type u) [Field F] [NumberField F]
    (p : ℕ) [Fact (Nat.Prime p)] :
    IntermediateField F (AlgebraicClosure F)

theorem

le_maximalEverywhereUnramifiedProP

L46 ↗

ClassFieldTower.Martinet.le_maximalEverywhereUnramifiedProP

Documentation

Every finite Galois everywhere-unramified p-extension contained in the chosen algebraic closure lies in 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

theorem le_maximalEverywhereUnramifiedProP
    (F : Type u) [Field F] [NumberField F]
    (p : ℕ) [Fact (Nat.Prime p)]
    (M : IntermediateField F (AlgebraicClosure F))
    [FiniteDimensional F M]
    [IsGalois F M]
    (hP : IsPGroup p (M ≃ₐ[F] M))
    [NumberField M]
    (hM : IsEverywhereUnramified F M) :
    M ≤ maximalEverywhereUnramifiedProP F p

theorem

maximalEverywhereUnramifiedProP_le_iff

L65 ↗

ClassFieldTower.Martinet.maximalEverywhereUnramifiedProP_le_iff

Documentation

The maximal compositum lies in an intermediate field exactly when every candidate used to form it lies in that 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_le_iff
    (F : Type u) [Field F] [NumberField F]
    (p : ℕ) [Fact (Nat.Prime p)]
    (N : IntermediateField F (AlgebraicClosure F)) :
    maximalEverywhereUnramifiedProP F p ≤ N ↔
      ∀ (M : IntermediateField F (AlgebraicClosure F))
        [FiniteDimensional F M]
        [IsGalois F M]
        (_ : IsPGroup p (M ≃ₐ[F] M))
        [NumberField M],
        IsEverywhereUnramified F M → M ≤ N

theorem

maximalEverywhereUnramifiedProP_le_of_forall_le

L80 ↗

ClassFieldTower.Martinet.maximalEverywhereUnramifiedProP_le_of_forall_le

Documentation

The maximal compositum is the least upper bound of all finite Galois everywhere-unramified p-extensions in the chosen algebraic closure.

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_le_of_forall_le
    (F : Type u) [Field F] [NumberField F]
    (p : ℕ) [Fact (Nat.Prime p)]
    (N : IntermediateField F (AlgebraicClosure F))
    (hN : ∀ (M : IntermediateField F (AlgebraicClosure F))
      [FiniteDimensional F M]
      [IsGalois F M]
      (_ : IsPGroup p (M ≃ₐ[F] M))
      [NumberField M],
      IsEverywhereUnramified F M → M ≤ N) :
    maximalEverywhereUnramifiedProP F p ≤ N

theorem

maximalEverywhereUnramifiedProP_eq_iff

L95 ↗

ClassFieldTower.Martinet.maximalEverywhereUnramifiedProP_eq_iff

Documentation

An intermediate field is the maximal compositum exactly when it is an upper bound for every candidate and is itself contained in the 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

theorem maximalEverywhereUnramifiedProP_eq_iff
    (F : Type u) [Field F] [NumberField F]
    (p : ℕ) [Fact (Nat.Prime p)]
    (N : IntermediateField F (AlgebraicClosure F)) :
    maximalEverywhereUnramifiedProP F p = N ↔
      (∀ (M : IntermediateField F (AlgebraicClosure F))
        [FiniteDimensional F M]
        [IsGalois F M]
        (_ : IsPGroup p (M ≃ₐ[F] M))
        [NumberField M],
        IsEverywhereUnramified F M → M ≤ N) ∧
      N ≤ maximalEverywhereUnramifiedProP F p

Module documentation

The maximal everywhere-unramified pro-p subextension

Declarations

maximalEverywhereUnramifiedProP

le_maximalEverywhereUnramifiedProP

maximalEverywhereUnramifiedProP_le_iff

maximalEverywhereUnramifiedProP_le_of_forall_le

maximalEverywhereUnramifiedProP_eq_iff