NYLL
Module

PrimeOrderFixedField.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Ramification.Splitting.PrimeOrderFixedField
16 declarations indexed from sourceView source ↗

Module documentation

Prime-order fixed fields and complete splitting

This file formalizes a prime-order fixed-field reduction. From a nontrivial finite Galois extension L / K we choose an automorphism σ of prime order p and form

K' = L ^ ⟨σ⟩.

The extension L / K' is an actual cyclic Galois extension of prime degree. We also prove the finite-place bridge used immediately before applying the cyclic prime-power splitting criterion: if a finite place of K splits completely in L and a finite place of K' lies above it, then the latter splits completely in L / K'.

Imports1
Imported by3

Declarations

theorem

exists_prime_order_automorphism_of_one_lt_finrank

L46 ↗
Documentation

A nontrivial finite Galois extension has an automorphism of prime order. Nontriviality is supplied by the actual degree inequality.

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section PrimeOrderConstruction
variable {K L : Type}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
local notation "G" => L ≃ₐ[K] L
Lean source · statement
theorem exists_prime_order_automorphism_of_one_lt_finrank
    (hdegree : 1 < Module.finrank K L) :
    ∃ (p : ℕ) (σ : G),
      p.Prime ∧ orderOf σ = p
def

fixedFieldPrime

L58 ↗
Documentation

The chosen prime order in the nontrivial Galois group.

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section PrimeOrderConstruction
variable {K L : Type}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
local notation "G" => L ≃ₐ[K] L
Lean source · statement
def fixedFieldPrime
    (hdegree : 1 < Module.finrank K L) : ℕ
def

primeOrderAutomorphism

L64 ↗
Documentation

The chosen automorphism of prime order.

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section PrimeOrderConstruction
variable {K L : Type}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
local notation "G" => L ≃ₐ[K] L
Lean source · statement
def primeOrderAutomorphism
    (hdegree : 1 < Module.finrank K L) : G
theorem

fixedFieldPrime_prime

L69 ↗
Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section PrimeOrderConstruction
variable {K L : Type}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
local notation "G" => L ≃ₐ[K] L
Lean source · statement
theorem fixedFieldPrime_prime
    (hdegree : 1 < Module.finrank K L) :
    (fixedFieldPrime
      (K := K) (L := L) hdegree).Prime
theorem

primeOrderAutomorphism_orderOf

L76 ↗
Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section PrimeOrderConstruction
variable {K L : Type}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
local notation "G" => L ≃ₐ[K] L
Lean source · statement
theorem primeOrderAutomorphism_orderOf
    (hdegree : 1 < Module.finrank K L) :
    orderOf
        (primeOrderAutomorphism
          (K := K) (L := L) hdegree) =
      fixedFieldPrime
        (K := K) (L := L) hdegree
def

primeOrderSubgroup

L88 ↗
Documentation

The cyclic subgroup generated by the chosen prime-order automorphism.

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section PrimeOrderConstruction
variable {K L : Type}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
local notation "G" => L ≃ₐ[K] L
Lean source · statement
def primeOrderSubgroup
    (hdegree : 1 < Module.finrank K L) :
    Subgroup G
theorem

primeOrderSubgroup_card

L95 ↗
Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section PrimeOrderConstruction
variable {K L : Type}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
local notation "G" => L ≃ₐ[K] L
Lean source · statement
theorem primeOrderSubgroup_card
    (hdegree : 1 < Module.finrank K L) :
    Nat.card
        (primeOrderSubgroup
          (K := K) (L := L) hdegree) =
      fixedFieldPrime
        (K := K) (L := L) hdegree
def

primeOrderFixedField

L106 ↗
Documentation

The actual intermediate field K' = L ^ ⟨σ⟩.

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section PrimeOrderConstruction
variable {K L : Type}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
local notation "G" => L ≃ₐ[K] L
Lean source · statement
def primeOrderFixedField
    (hdegree : 1 < Module.finrank K L) :
    IntermediateField K L
instance

primeOrderFixedField_isGalois

L115 ↗
Documentation

The ambient field is Galois over the fixed field of the chosen finite subgroup.

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section PrimeOrderConstruction
variable {K L : Type}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
local notation "G" => L ≃ₐ[K] L
Lean source · statement
instance primeOrderFixedField_isGalois
    (hdegree : 1 < Module.finrank K L) :
    IsGalois
      (primeOrderFixedField
        (K := K) (L := L) hdegree)
      L
theorem

primeOrderFixedField_finrank

L128 ↗
Documentation

The constructed relative extension has prime degree p.

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section PrimeOrderConstruction
variable {K L : Type}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
local notation "G" => L ≃ₐ[K] L
Lean source · statement
theorem primeOrderFixedField_finrank
    (hdegree : 1 < Module.finrank K L) :
    Module.finrank
        (primeOrderFixedField
          (K := K) (L := L) hdegree)
        L =
      fixedFieldPrime
        (K := K) (L := L) hdegree
instance

primeOrderFixedField_isCyclic

L142 ↗
Documentation

The relative Galois group is cyclic, transported from the generating subgroup through the finite Galois correspondence.

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section PrimeOrderConstruction
variable {K L : Type}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
local notation "G" => L ≃ₐ[K] L
Lean source · statement
instance primeOrderFixedField_isCyclic
    (hdegree : 1 < Module.finrank K L) :
    IsCyclic
      (L ≃ₐ[
        primeOrderFixedField
          (K := K) (L := L) hdegree] L)
theorem

primeOrderFixedField_card_aut

L164 ↗
Documentation

The order of the relative Galois group is the chosen prime. In particular it is a prime-power order with exponent one, exactly the input expected by the cyclic prime-power splitting criterion.

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section PrimeOrderConstruction
variable {K L : Type}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
local notation "G" => L ≃ₐ[K] L
Lean source · statement
theorem primeOrderFixedField_card_aut
    (hdegree : 1 < Module.finrank K L) :
    Nat.card
        (L ≃ₐ[
          primeOrderFixedField
            (K := K) (L := L) hdegree] L) =
      fixedFieldPrime
        (K := K) (L := L) hdegree
def

FinitePlaceLiesAbove

L186 ↗
Documentation

A finite place of M lies above a finite place of K when its normalized adic absolute value is an exact extension.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section FinitePlaceAscent
variable {K M : Type}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Algebra K M]
Lean source · statement
def FinitePlaceLiesAbove
    (v : HeightOneSpectrum (𝓞 K))
    (v' : HeightOneSpectrum (𝓞 M)) : Prop
theorem

finitePlaceSplitsCompletely_over_intermediate_of_liesAbove

L208 ↗
Documentation

Complete splitting ascends from a base finite place to every finite place of an intermediate field lying above it.

The proof uses the chosen extension above v', regards it as an extension above v, changes from the standard chosen extension over K by valuation-extension counting, and finally restricts the trivial decomposition group from K to M.

Source context 9 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section FinitePlaceAscent
variable {K M : Type}
    [Field K] [NumberField K]
    [Field M] [NumberField M]
    [Algebra K M]
variable {L : Type}
    [Field L] [NumberField L]
    [Algebra K L] [Algebra M L]
    [IsScalarTower K M L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsGalois M L]
omit [NumberField L] [FiniteDimensional K L] in
Lean source · statement
theorem finitePlaceSplitsCompletely_over_intermediate_of_liesAbove
    (v : HeightOneSpectrum (𝓞 K))
    (v' : HeightOneSpectrum (𝓞 M))
    (hAbove : FinitePlaceLiesAbove (K := K) (M := M) v v')
    (hsplit :
      FinitePlaceSplitsCompletely
        (K := K) (L := L) v) :
    FinitePlaceSplitsCompletely
      (K := M) (L := L) v'
theorem

primeOrderFixedField_threeSeven_data

L259 ↗
Documentation

The chosen fixed field supplies all algebraic data needed to apply the cyclic prime-power case with exponent one.

Source context 8 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section PrimeOrderFinitePlaces
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
omit [NumberField K] [NumberField L] in
Lean source · full declaration
theorem primeOrderFixedField_threeSeven_data
    (hdegree : 1 < Module.finrank K L) :
    let K' :=
      primeOrderFixedField
        (K := K) (L := L) hdegree
    let p :=
      fixedFieldPrime
        (K := K) (L := L) hdegree
    p.Prime ∧
      IsGalois K' L ∧
      IsCyclic (L ≃ₐ[K'] L) ∧
      Nat.card (L ≃ₐ[K'] L) = p := by
  dsimp
  exact
    ⟨fixedFieldPrime_prime
        (K := K) (L := L) hdegree,
      inferInstance,
      inferInstance,
      primeOrderFixedField_card_aut
        (K := K) (L := L) hdegree⟩
theorem

finitePlaceSplitsCompletely_over_primeOrderFixedField_of_liesAbove

L282 ↗
Documentation

The finite-place ascent bridge specialized to the chosen prime-order fixed field K'.

Source context 7 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
open AlgebraicNumberTheory.Valuations
open HilbertRamification
section PrimeOrderFinitePlaces
variable {K L : Type}
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
Lean source · statement
theorem finitePlaceSplitsCompletely_over_primeOrderFixedField_of_liesAbove
    (hdegree : 1 < Module.finrank K L)
    (v : HeightOneSpectrum (𝓞 K))
    (v' :
      HeightOneSpectrum
        (𝓞 (primeOrderFixedField
          (K := K) (L := L) hdegree)))
    (hAbove :
      FinitePlaceLiesAbove
        (K := K)
        (M := primeOrderFixedField
          (K := K) (L := L) hdegree)
        v v')
    (hsplit :
      FinitePlaceSplitsCompletely
        (K := K) (L := L) v) :
    FinitePlaceSplitsCompletely
      (K := primeOrderFixedField
        (K := K) (L := L) hdegree)
      (L := L) v'

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