Module

FrattiniClassField.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.Global.FrattiniClassField

20 declarations indexed from sourceView source ↗

Module documentation

The Frattini quotient and the elementary Hilbert class field

This file identifies the power--commutator quotient of the maximal everywhere- unramified pro-p Galois group with the elementary Hilbert class-field layer. For odd p, it then identifies the topological generator rank with the p-class rank.

Imports4

Imported by4

abbrev

M

L37 ↗

ClassFieldTower.Martinet.M

Source context 10 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open Set
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

abbrev M

abbrev

H

L39 ↗

ClassFieldTower.Martinet.H

Source context 10 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open Set
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

abbrev H

instance

(anonymous instance)

L41 ↗

Source context 10 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open Set
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]

Lean source · statement

instance :
    (closedPowerCommutator p
      (MaxEverywhereUnramifiedProPGaloisGroup F p)).Normal

def

maxPowerCommutatorToHilbert

L49 ↗

ClassFieldTower.Martinet.maxPowerCommutatorToHilbert

Documentation

Restriction to the elementary Hilbert layer, factored through the power--commutator quotient.

Source context 11 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open Set
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance :
    (closedPowerCommutator p
      (MaxEverywhereUnramifiedProPGaloisGroup F p)).Normal :=
  closedPowerCommutator_normal p
    (MaxEverywhereUnramifiedProPGaloisGroup F p)

Lean source · statement

def maxPowerCommutatorToHilbert :
    powerCommutatorQuotient p
        (MaxEverywhereUnramifiedProPGaloisGroup F p) →ₜ*
      Gal((H F p) / F)

theorem

maxPowerCommutatorToHilbert_surjective

L61 ↗

ClassFieldTower.Martinet.maxPowerCommutatorToHilbert_surjective

Documentation

Every automorphism of the elementary Hilbert layer extends to the maximal everywhere-unramified pro-p extension.

Source context 11 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open Set
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance :
    (closedPowerCommutator p
      (MaxEverywhereUnramifiedProPGaloisGroup F p)).Normal :=
  closedPowerCommutator_normal p
    (MaxEverywhereUnramifiedProPGaloisGroup F p)

Lean source · statement

theorem maxPowerCommutatorToHilbert_surjective :
    Function.Surjective (maxPowerCommutatorToHilbert F p)

abbrev

powerCommutatorClosed

L71 ↗

ClassFieldTower.Martinet.powerCommutatorClosed

Source context 11 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open Set
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance :
    (closedPowerCommutator p
      (MaxEverywhereUnramifiedProPGaloisGroup F p)).Normal :=
  closedPowerCommutator_normal p
    (MaxEverywhereUnramifiedProPGaloisGroup F p)

Lean source · full declaration

abbrev powerCommutatorClosed : ClosedSubgroup
    Gal((M F p) / F) where
  toSubgroup := closedPowerCommutator p Gal((M F p) / F)
  isClosed' := isClosed_closedPowerCommutator p Gal((M F p) / F)

instance

(anonymous instance)

L76 ↗

Source context 11 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open Set
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance :
    (closedPowerCommutator p
      (MaxEverywhereUnramifiedProPGaloisGroup F p)).Normal :=
  closedPowerCommutator_normal p
    (MaxEverywhereUnramifiedProPGaloisGroup F p)

Lean source · statement

instance : (powerCommutatorClosed F p :
    Subgroup Gal((M F p) / F)).Normal

abbrev

powerCommutatorFixedField

L81 ↗

ClassFieldTower.Martinet.powerCommutatorFixedField

Source context 12 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open Set
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance :
    (closedPowerCommutator p
      (MaxEverywhereUnramifiedProPGaloisGroup F p)).Normal :=
  closedPowerCommutator_normal p
    (MaxEverywhereUnramifiedProPGaloisGroup F p)
local instance : (powerCommutatorClosed F p :
    Subgroup Gal((M F p) / F)).Normal := by
  change (closedPowerCommutator p Gal((M F p) / F)).Normal
  exact closedPowerCommutator_normal p Gal((M F p) / F)

Lean source · statement

abbrev powerCommutatorFixedField : IntermediateField F (M F p)

instance

(anonymous instance)

L84 ↗

Source context 12 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open Set
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance :
    (closedPowerCommutator p
      (MaxEverywhereUnramifiedProPGaloisGroup F p)).Normal :=
  closedPowerCommutator_normal p
    (MaxEverywhereUnramifiedProPGaloisGroup F p)
local instance : (powerCommutatorClosed F p :
    Subgroup Gal((M F p) / F)).Normal := by
  change (closedPowerCommutator p Gal((M F p) / F)).Normal
  exact closedPowerCommutator_normal p Gal((M F p) / F)

Lean source · statement

instance : IsGalois F (powerCommutatorFixedField F p)

instance

(anonymous instance)

L88 ↗

Source context 13 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open Set
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance :
    (closedPowerCommutator p
      (MaxEverywhereUnramifiedProPGaloisGroup F p)).Normal :=
  closedPowerCommutator_normal p
    (MaxEverywhereUnramifiedProPGaloisGroup F p)
local instance : (powerCommutatorClosed F p :
    Subgroup Gal((M F p) / F)).Normal := by
  change (closedPowerCommutator p Gal((M F p) / F)).Normal
  exact closedPowerCommutator_normal p Gal((M F p) / F)
local instance : IsGalois F (powerCommutatorFixedField F p) :=
  IsGalois.of_fixedField_normal_subgroup
    (powerCommutatorClosed F p).toSubgroup

Lean source · full declaration

instance : IsAbelianGalois F (powerCommutatorFixedField F p) where
  is_comm.comm σ τ := by
    let e := InfiniteGalois.normalAutEquivQuotient
      (powerCommutatorClosed F p)
    calc
      σ * τ = e (e.symm σ * e.symm τ) := by simp
      _ = e (e.symm τ * e.symm σ) := by
        congr 1
        exact powerCommutatorQuotient_mul_comm p
          Gal((M F p) / F) _ _
      _ = τ * σ := by simp

theorem

powerCommutatorFixedField_galois_pow_eq_one

L102 ↗

ClassFieldTower.Martinet.powerCommutatorFixedField_galois_pow_eq_one

Source context 14 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open Set
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance :
    (closedPowerCommutator p
      (MaxEverywhereUnramifiedProPGaloisGroup F p)).Normal :=
  closedPowerCommutator_normal p
    (MaxEverywhereUnramifiedProPGaloisGroup F p)
local instance : (powerCommutatorClosed F p :
    Subgroup Gal((M F p) / F)).Normal := by
  change (closedPowerCommutator p Gal((M F p) / F)).Normal
  exact closedPowerCommutator_normal p Gal((M F p) / F)
local instance : IsGalois F (powerCommutatorFixedField F p) :=
  IsGalois.of_fixedField_normal_subgroup
    (powerCommutatorClosed F p).toSubgroup
local instance : IsAbelianGalois F (powerCommutatorFixedField F p) where
  is_comm.comm σ τ := by
    let e := InfiniteGalois.normalAutEquivQuotient
      (powerCommutatorClosed F p)
    calc
      σ * τ = e (e.symm σ * e.symm τ) := by simp
      _ = e (e.symm τ * e.symm σ) := by
        congr 1
        exact powerCommutatorQuotient_mul_comm p
          Gal((M F p) / F) _ _
      _ = τ * σ := by simp

Lean source · statement

theorem powerCommutatorFixedField_galois_pow_eq_one
    (σ : Gal((powerCommutatorFixedField F p)/F)) : σ ^ p = 1

abbrev

liftedPowerCommutatorFixedField

L116 ↗

ClassFieldTower.Martinet.liftedPowerCommutatorFixedField

Source context 14 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open Set
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance :
    (closedPowerCommutator p
      (MaxEverywhereUnramifiedProPGaloisGroup F p)).Normal :=
  closedPowerCommutator_normal p
    (MaxEverywhereUnramifiedProPGaloisGroup F p)
local instance : (powerCommutatorClosed F p :
    Subgroup Gal((M F p) / F)).Normal := by
  change (closedPowerCommutator p Gal((M F p) / F)).Normal
  exact closedPowerCommutator_normal p Gal((M F p) / F)
local instance : IsGalois F (powerCommutatorFixedField F p) :=
  IsGalois.of_fixedField_normal_subgroup
    (powerCommutatorClosed F p).toSubgroup
local instance : IsAbelianGalois F (powerCommutatorFixedField F p) where
  is_comm.comm σ τ := by
    let e := InfiniteGalois.normalAutEquivQuotient
      (powerCommutatorClosed F p)
    calc
      σ * τ = e (e.symm σ * e.symm τ) := by simp
      _ = e (e.symm τ * e.symm σ) := by
        congr 1
        exact powerCommutatorQuotient_mul_comm p
          Gal((M F p) / F) _ _
      _ = τ * σ := by simp

Lean source · statement

abbrev liftedPowerCommutatorFixedField :
    IntermediateField F (AlgebraicClosure F)

instance

(anonymous instance)

L120 ↗

Source context 14 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open Set
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance :
    (closedPowerCommutator p
      (MaxEverywhereUnramifiedProPGaloisGroup F p)).Normal :=
  closedPowerCommutator_normal p
    (MaxEverywhereUnramifiedProPGaloisGroup F p)
local instance : (powerCommutatorClosed F p :
    Subgroup Gal((M F p) / F)).Normal := by
  change (closedPowerCommutator p Gal((M F p) / F)).Normal
  exact closedPowerCommutator_normal p Gal((M F p) / F)
local instance : IsGalois F (powerCommutatorFixedField F p) :=
  IsGalois.of_fixedField_normal_subgroup
    (powerCommutatorClosed F p).toSubgroup
local instance : IsAbelianGalois F (powerCommutatorFixedField F p) where
  is_comm.comm σ τ := by
    let e := InfiniteGalois.normalAutEquivQuotient
      (powerCommutatorClosed F p)
    calc
      σ * τ = e (e.symm σ * e.symm τ) := by simp
      _ = e (e.symm τ * e.symm σ) := by
        congr 1
        exact powerCommutatorQuotient_mul_comm p
          Gal((M F p) / F) _ _
      _ = τ * σ := by simp

Lean source · statement

instance : IsAbelianGalois F (liftedPowerCommutatorFixedField F p)

theorem

liftedPowerCommutatorFixedField_galois_pow_eq_one

L125 ↗

ClassFieldTower.Martinet.liftedPowerCommutatorFixedField_galois_pow_eq_one

Source context 15 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open Set
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance :
    (closedPowerCommutator p
      (MaxEverywhereUnramifiedProPGaloisGroup F p)).Normal :=
  closedPowerCommutator_normal p
    (MaxEverywhereUnramifiedProPGaloisGroup F p)
local instance : (powerCommutatorClosed F p :
    Subgroup Gal((M F p) / F)).Normal := by
  change (closedPowerCommutator p Gal((M F p) / F)).Normal
  exact closedPowerCommutator_normal p Gal((M F p) / F)
local instance : IsGalois F (powerCommutatorFixedField F p) :=
  IsGalois.of_fixedField_normal_subgroup
    (powerCommutatorClosed F p).toSubgroup
local instance : IsAbelianGalois F (powerCommutatorFixedField F p) where
  is_comm.comm σ τ := by
    let e := InfiniteGalois.normalAutEquivQuotient
      (powerCommutatorClosed F p)
    calc
      σ * τ = e (e.symm σ * e.symm τ) := by simp
      _ = e (e.symm τ * e.symm σ) := by
        congr 1
        exact powerCommutatorQuotient_mul_comm p
          Gal((M F p) / F) _ _
      _ = τ * σ := by simp
local instance : IsAbelianGalois F (liftedPowerCommutatorFixedField F p) :=
  IsAbelianGalois.of_algHom
    (IntermediateField.liftAlgEquiv
      (powerCommutatorFixedField F p)).symm.toAlgHom

Lean source · statement

theorem liftedPowerCommutatorFixedField_galois_pow_eq_one
    (σ : Gal((liftedPowerCommutatorFixedField F p)/F)) : σ ^ p = 1

theorem

liftedPowerCommutatorFixedField_le_hilbert

L141 ↗

ClassFieldTower.Martinet.liftedPowerCommutatorFixedField_le_hilbert

Source context 15 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open Set
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance :
    (closedPowerCommutator p
      (MaxEverywhereUnramifiedProPGaloisGroup F p)).Normal :=
  closedPowerCommutator_normal p
    (MaxEverywhereUnramifiedProPGaloisGroup F p)
local instance : (powerCommutatorClosed F p :
    Subgroup Gal((M F p) / F)).Normal := by
  change (closedPowerCommutator p Gal((M F p) / F)).Normal
  exact closedPowerCommutator_normal p Gal((M F p) / F)
local instance : IsGalois F (powerCommutatorFixedField F p) :=
  IsGalois.of_fixedField_normal_subgroup
    (powerCommutatorClosed F p).toSubgroup
local instance : IsAbelianGalois F (powerCommutatorFixedField F p) where
  is_comm.comm σ τ := by
    let e := InfiniteGalois.normalAutEquivQuotient
      (powerCommutatorClosed F p)
    calc
      σ * τ = e (e.symm σ * e.symm τ) := by simp
      _ = e (e.symm τ * e.symm σ) := by
        congr 1
        exact powerCommutatorQuotient_mul_comm p
          Gal((M F p) / F) _ _
      _ = τ * σ := by simp
local instance : IsAbelianGalois F (liftedPowerCommutatorFixedField F p) :=
  IsAbelianGalois.of_algHom
    (IntermediateField.liftAlgEquiv
      (powerCommutatorFixedField F p)).symm.toAlgHom

Lean source · statement

theorem liftedPowerCommutatorFixedField_le_hilbert
    (hpOdd : Odd p) :
    liftedPowerCommutatorFixedField F p ≤
      hilbertElementaryLayerInAlgebraicClosure F p

theorem

powerCommutatorFixedField_le_hilbertInMaximal

L189 ↗

ClassFieldTower.Martinet.powerCommutatorFixedField_le_hilbertInMaximal

Source context 15 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open Set
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance :
    (closedPowerCommutator p
      (MaxEverywhereUnramifiedProPGaloisGroup F p)).Normal :=
  closedPowerCommutator_normal p
    (MaxEverywhereUnramifiedProPGaloisGroup F p)
local instance : (powerCommutatorClosed F p :
    Subgroup Gal((M F p) / F)).Normal := by
  change (closedPowerCommutator p Gal((M F p) / F)).Normal
  exact closedPowerCommutator_normal p Gal((M F p) / F)
local instance : IsGalois F (powerCommutatorFixedField F p) :=
  IsGalois.of_fixedField_normal_subgroup
    (powerCommutatorClosed F p).toSubgroup
local instance : IsAbelianGalois F (powerCommutatorFixedField F p) where
  is_comm.comm σ τ := by
    let e := InfiniteGalois.normalAutEquivQuotient
      (powerCommutatorClosed F p)
    calc
      σ * τ = e (e.symm σ * e.symm τ) := by simp
      _ = e (e.symm τ * e.symm σ) := by
        congr 1
        exact powerCommutatorQuotient_mul_comm p
          Gal((M F p) / F) _ _
      _ = τ * σ := by simp
local instance : IsAbelianGalois F (liftedPowerCommutatorFixedField F p) :=
  IsAbelianGalois.of_algHom
    (IntermediateField.liftAlgEquiv
      (powerCommutatorFixedField F p)).symm.toAlgHom

Lean source · statement

theorem powerCommutatorFixedField_le_hilbertInMaximal
    (hpOdd : Odd p) :
    powerCommutatorFixedField F p ≤ H F p

theorem

maxPowerCommutatorToHilbert_injective

L199 ↗

ClassFieldTower.Martinet.maxPowerCommutatorToHilbert_injective

Documentation

For odd p, restriction to the elementary Hilbert layer is injective on the power--commutator quotient.

Source context 15 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open Set
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance :
    (closedPowerCommutator p
      (MaxEverywhereUnramifiedProPGaloisGroup F p)).Normal :=
  closedPowerCommutator_normal p
    (MaxEverywhereUnramifiedProPGaloisGroup F p)
local instance : (powerCommutatorClosed F p :
    Subgroup Gal((M F p) / F)).Normal := by
  change (closedPowerCommutator p Gal((M F p) / F)).Normal
  exact closedPowerCommutator_normal p Gal((M F p) / F)
local instance : IsGalois F (powerCommutatorFixedField F p) :=
  IsGalois.of_fixedField_normal_subgroup
    (powerCommutatorClosed F p).toSubgroup
local instance : IsAbelianGalois F (powerCommutatorFixedField F p) where
  is_comm.comm σ τ := by
    let e := InfiniteGalois.normalAutEquivQuotient
      (powerCommutatorClosed F p)
    calc
      σ * τ = e (e.symm σ * e.symm τ) := by simp
      _ = e (e.symm τ * e.symm σ) := by
        congr 1
        exact powerCommutatorQuotient_mul_comm p
          Gal((M F p) / F) _ _
      _ = τ * σ := by simp
local instance : IsAbelianGalois F (liftedPowerCommutatorFixedField F p) :=
  IsAbelianGalois.of_algHom
    (IntermediateField.liftAlgEquiv
      (powerCommutatorFixedField F p)).symm.toAlgHom

Lean source · statement

theorem maxPowerCommutatorToHilbert_injective (hpOdd : Odd p) :
    Function.Injective (maxPowerCommutatorToHilbert F p)

def

maxPowerCommutatorEquivHilbert

L232 ↗

ClassFieldTower.Martinet.maxPowerCommutatorEquivHilbert

Documentation

The Frattini quotient of the maximal unramified pro-p Galois group is the Galois group of the elementary Hilbert layer.

Source context 15 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open Set
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance :
    (closedPowerCommutator p
      (MaxEverywhereUnramifiedProPGaloisGroup F p)).Normal :=
  closedPowerCommutator_normal p
    (MaxEverywhereUnramifiedProPGaloisGroup F p)
local instance : (powerCommutatorClosed F p :
    Subgroup Gal((M F p) / F)).Normal := by
  change (closedPowerCommutator p Gal((M F p) / F)).Normal
  exact closedPowerCommutator_normal p Gal((M F p) / F)
local instance : IsGalois F (powerCommutatorFixedField F p) :=
  IsGalois.of_fixedField_normal_subgroup
    (powerCommutatorClosed F p).toSubgroup
local instance : IsAbelianGalois F (powerCommutatorFixedField F p) where
  is_comm.comm σ τ := by
    let e := InfiniteGalois.normalAutEquivQuotient
      (powerCommutatorClosed F p)
    calc
      σ * τ = e (e.symm σ * e.symm τ) := by simp
      _ = e (e.symm τ * e.symm σ) := by
        congr 1
        exact powerCommutatorQuotient_mul_comm p
          Gal((M F p) / F) _ _
      _ = τ * σ := by simp
local instance : IsAbelianGalois F (liftedPowerCommutatorFixedField F p) :=
  IsAbelianGalois.of_algHom
    (IntermediateField.liftAlgEquiv
      (powerCommutatorFixedField F p)).symm.toAlgHom

Lean source · statement

def maxPowerCommutatorEquivHilbert (hpOdd : Odd p) :
    powerCommutatorQuotient p
        (MaxEverywhereUnramifiedProPGaloisGroup F p) ≃*
      Gal((H F p) / F)

theorem

topologicallyFinitelyGenerated_of_finite_powerCommutatorQuotient

L240 ↗

ClassFieldTower.Martinet.topologicallyFinitelyGenerated_of_finite_powerCommutatorQuotient

Source context 15 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open Set
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance :
    (closedPowerCommutator p
      (MaxEverywhereUnramifiedProPGaloisGroup F p)).Normal :=
  closedPowerCommutator_normal p
    (MaxEverywhereUnramifiedProPGaloisGroup F p)
local instance : (powerCommutatorClosed F p :
    Subgroup Gal((M F p) / F)).Normal := by
  change (closedPowerCommutator p Gal((M F p) / F)).Normal
  exact closedPowerCommutator_normal p Gal((M F p) / F)
local instance : IsGalois F (powerCommutatorFixedField F p) :=
  IsGalois.of_fixedField_normal_subgroup
    (powerCommutatorClosed F p).toSubgroup
local instance : IsAbelianGalois F (powerCommutatorFixedField F p) where
  is_comm.comm σ τ := by
    let e := InfiniteGalois.normalAutEquivQuotient
      (powerCommutatorClosed F p)
    calc
      σ * τ = e (e.symm σ * e.symm τ) := by simp
      _ = e (e.symm τ * e.symm σ) := by
        congr 1
        exact powerCommutatorQuotient_mul_comm p
          Gal((M F p) / F) _ _
      _ = τ * σ := by simp
local instance : IsAbelianGalois F (liftedPowerCommutatorFixedField F p) :=
  IsAbelianGalois.of_algHom
    (IntermediateField.liftAlgEquiv
      (powerCommutatorFixedField F p)).symm.toAlgHom

Lean source · statement

theorem topologicallyFinitelyGenerated_of_finite_powerCommutatorQuotient
    {q : ℕ} {G : Type*}
    [TopologicalSpace G] [Group G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    [Fact q.Prime]
    (hqG : ProCGroups.ProC.HasPGroupOpenNormalBasis q G)
    [Finite (powerCommutatorQuotient q G)] :
    TopologicallyFinitelyGenerated G

theorem

generatorRank_maxUnramified_eq_pClassRank

L271 ↗

ClassFieldTower.Martinet.generatorRank_maxUnramified_eq_pClassRank

Documentation

For odd p, the generator rank of the maximal everywhere-unramified pro-p Galois group is the p-class rank.

Source context 15 commands

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

open scoped NumberField IsMulCommutative
noncomputable section
open Set
open GlobalClassFieldTheory GlobalClassFieldTheory.GlobalClassFields
namespace ClassFieldTower.Martinet
open ClassFieldTower.ProP
open ProCGroups.Generation
open ProCGroups.FiniteGeneration
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
local instance :
    (closedPowerCommutator p
      (MaxEverywhereUnramifiedProPGaloisGroup F p)).Normal :=
  closedPowerCommutator_normal p
    (MaxEverywhereUnramifiedProPGaloisGroup F p)
local instance : (powerCommutatorClosed F p :
    Subgroup Gal((M F p) / F)).Normal := by
  change (closedPowerCommutator p Gal((M F p) / F)).Normal
  exact closedPowerCommutator_normal p Gal((M F p) / F)
local instance : IsGalois F (powerCommutatorFixedField F p) :=
  IsGalois.of_fixedField_normal_subgroup
    (powerCommutatorClosed F p).toSubgroup
local instance : IsAbelianGalois F (powerCommutatorFixedField F p) where
  is_comm.comm σ τ := by
    let e := InfiniteGalois.normalAutEquivQuotient
      (powerCommutatorClosed F p)
    calc
      σ * τ = e (e.symm σ * e.symm τ) := by simp
      _ = e (e.symm τ * e.symm σ) := by
        congr 1
        exact powerCommutatorQuotient_mul_comm p
          Gal((M F p) / F) _ _
      _ = τ * σ := by simp
local instance : IsAbelianGalois F (liftedPowerCommutatorFixedField F p) :=
  IsAbelianGalois.of_algHom
    (IntermediateField.liftAlgEquiv
      (powerCommutatorFixedField F p)).symm.toAlgHom

Lean source · statement

theorem generatorRank_maxUnramified_eq_pClassRank (hpOdd : Odd p) :
    topologicalGeneratorRank
        (MaxEverywhereUnramifiedProPGaloisGroup F p) =
      pClassRank F p

Module documentation

The Frattini quotient and the elementary Hilbert class field

Declarations