NYLL
Module

CyclotomicPrimeBaseChange.lean

Nyll.ClassFieldTheory.KummerTheory.Concrete.CyclotomicPrimeBaseChange
16 declarations indexed from sourceView source ↗

Module documentation

Prime cyclotomic base change

This file constructs the roots-of-unity base change for a prime-degree extension. If L / K has prime degree p, the cyclotomic extension K(μ_p) / K has degree strictly smaller than p. The two degrees are therefore coprime, and

K(μ_p) ⊗[K] L

is an actual field, Galois of degree p over K(μ_p).

Imports2
Imported by3

Declarations

theorem

cyclotomicField_finrank_le_totient

L42 ↗
KummerTheory.cyclotomicField_finrank_le_totient
Documentation

Over a characteristic-zero field, the concrete cyclotomic field of order m has degree at most φ(m).

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace KummerTheory
universe u
variable
    (K L : Type u)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [IsGalois K L]
Lean source · statement
theorem cyclotomicField_finrank_le_totient
    (F : Type*) [Field F] [CharZero F]
    (m : ℕ) (hm : 0 < m) :
    Module.finrank F (CyclotomicField m F) ≤
      Nat.totient m
abbrev

PrimeCyclotomicBase

L92 ↗
KummerTheory.PrimeCyclotomicBase
Documentation

The prime cyclotomic base field used for prime-degree base change.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace KummerTheory
universe u
variable
    (K L : Type u)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [IsGalois K L]
Lean source · statement
abbrev PrimeCyclotomicBase (p : ℕ)
abbrev

PrimeCyclotomicPushout

L98 ↗
KummerTheory.PrimeCyclotomicPushout
Documentation

The tensor-product compositum of L and the prime cyclotomic base field. Its field structure is constructed below from coprime degrees.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace KummerTheory
universe u
variable
    (K L : Type u)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [IsGalois K L]
Lean source · statement
abbrev PrimeCyclotomicPushout (p : ℕ)
instance

primeCyclotomicBaseFiniteDimensional

L101 ↗
KummerTheory.primeCyclotomicBaseFiniteDimensional
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace KummerTheory
universe u
variable
    (K L : Type u)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [IsGalois K L]
Lean source · statement
instance primeCyclotomicBaseFiniteDimensional
    (p : ℕ) [NeZero p] :
    FiniteDimensional K (PrimeCyclotomicBase K p)
instance

primeCyclotomicBaseIsGalois

L107 ↗
KummerTheory.primeCyclotomicBaseIsGalois
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace KummerTheory
universe u
variable
    (K L : Type u)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [IsGalois K L]
Lean source · statement
instance primeCyclotomicBaseIsGalois
    (p : ℕ) [NeZero p] :
    IsGalois K (PrimeCyclotomicBase K p)
instance

primeCyclotomicBaseNumberField

L113 ↗
KummerTheory.primeCyclotomicBaseNumberField
Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace KummerTheory
universe u
variable
    (K L : Type u)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [IsGalois K L]
Lean source · statement
instance primeCyclotomicBaseNumberField
    (p : ℕ) [NeZero p] :
    NumberField (PrimeCyclotomicBase K p)
theorem

primeCyclotomicBase_finrank_lt

L121 ↗
KummerTheory.primeCyclotomicBase_finrank_lt
Documentation

Over a characteristic-zero field, the degree of K(μ_p) is strictly smaller than the prime p.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace KummerTheory
universe u
variable
    (K L : Type u)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [IsGalois K L]
Lean source · statement
theorem primeCyclotomicBase_finrank_lt
    (p : ℕ) (hp : p.Prime) :
    Module.finrank K (PrimeCyclotomicBase K p) < p
theorem

primeCyclotomicBase_finrank_coprime

L135 ↗
KummerTheory.primeCyclotomicBase_finrank_coprime
Documentation

The cyclotomic degree is coprime to a prime-degree extension.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace KummerTheory
universe u
variable
    (K L : Type u)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [IsGalois K L]
omit [NumberField L] [IsGalois K L] in
Lean source · statement
theorem primeCyclotomicBase_finrank_coprime
    (p : ℕ) (hp : p.Prime)
    (hdegree : Module.finrank K L = p) :
    (Module.finrank K (PrimeCyclotomicBase K p)).Coprime
      (Module.finrank K L)
def

primeCyclotomicPushoutField

L151 ↗
KummerTheory.primeCyclotomicPushoutField
Documentation

The field structure on the prime cyclotomic pushout, obtained from coprime degrees.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace KummerTheory
universe u
variable
    (K L : Type u)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [IsGalois K L]
Lean source · statement
def primeCyclotomicPushoutField
    (p : ℕ) (hp : p.Prime)
    (hdegree : Module.finrank K L = p) :
    Field (PrimeCyclotomicPushout K L p)
def

primeCyclotomicPushoutAlgebra

L163 ↗
KummerTheory.primeCyclotomicPushoutAlgebra
Documentation

The canonical left-factor algebra structure, restated after installing the field structure on the tensor product.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace KummerTheory
universe u
variable
    (K L : Type u)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [IsGalois K L]
Lean source · full declaration
def primeCyclotomicPushoutAlgebra
    (p : ℕ) (hp : p.Prime)
    (hdegree : Module.finrank K L = p) :
    letI : NeZero p := ⟨hp.ne_zero⟩
    letI : Field (PrimeCyclotomicPushout K L p) :=
      primeCyclotomicPushoutField K L p hp hdegree
    Algebra
      (PrimeCyclotomicBase K p)
      (PrimeCyclotomicPushout K L p) := by
  letI : Field (PrimeCyclotomicPushout K L p) :=
    primeCyclotomicPushoutField K L p hp hdegree
  exact Algebra.TensorProduct.leftAlgebra
theorem

primeCyclotomicPushout_finrank

L178 ↗
KummerTheory.primeCyclotomicPushout_finrank
Documentation

The pushout has the expected degree over the cyclotomic base.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace KummerTheory
universe u
variable
    (K L : Type u)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [IsGalois K L]
omit [IsGalois K L] in
Lean source · full declaration
theorem primeCyclotomicPushout_finrank
    (p : ℕ) (hp : p.Prime)
    (hdegree : Module.finrank K L = p) :
    letI : NeZero p := ⟨hp.ne_zero⟩
    letI : Field (PrimeCyclotomicPushout K L p) :=
      primeCyclotomicPushoutField K L p hp hdegree
    letI : Algebra
        (PrimeCyclotomicBase K p)
        (PrimeCyclotomicPushout K L p) :=
      primeCyclotomicPushoutAlgebra K L p hp hdegree
    Module.finrank
        (PrimeCyclotomicBase K p)
        (PrimeCyclotomicPushout K L p) =
      p := by
  let : NeZero p := ⟨hp.ne_zero⟩
  let : Field (PrimeCyclotomicPushout K L p) :=
    primeCyclotomicPushoutField K L p hp hdegree
  let : Algebra
      (PrimeCyclotomicBase K p)
      (PrimeCyclotomicPushout K L p) :=
    primeCyclotomicPushoutAlgebra K L p hp hdegree
  rw [Module.finrank_baseChange, hdegree]
theorem

primeCyclotomicPushout_isGalois

L202 ↗
KummerTheory.primeCyclotomicPushout_isGalois
Documentation

The prime cyclotomic pushout is Galois over K(μ_p).

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace KummerTheory
universe u
variable
    (K L : Type u)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [IsGalois K L]
Lean source · full declaration
theorem primeCyclotomicPushout_isGalois
    (p : ℕ) (hp : p.Prime)
    (hdegree : Module.finrank K L = p) :
    letI : NeZero p := ⟨hp.ne_zero⟩
    letI : Field (PrimeCyclotomicPushout K L p) :=
      primeCyclotomicPushoutField K L p hp hdegree
    letI : Algebra
        (PrimeCyclotomicBase K p)
        (PrimeCyclotomicPushout K L p) :=
      primeCyclotomicPushoutAlgebra K L p hp hdegree
    IsGalois
      (PrimeCyclotomicBase K p)
      (PrimeCyclotomicPushout K L p) := by
  let : NeZero p := ⟨hp.ne_zero⟩
  let : Field (PrimeCyclotomicPushout K L p) :=
    primeCyclotomicPushoutField K L p hp hdegree
  let : Algebra
      (PrimeCyclotomicBase K p)
      (PrimeCyclotomicPushout K L p) :=
    primeCyclotomicPushoutAlgebra K L p hp hdegree
  exact
    tensorProduct_isGalois_of_finrank_coprime
      K (PrimeCyclotomicBase K p) L
      (primeCyclotomicBase_finrank_coprime
        (K := K) (L := L) p hp hdegree)
theorem

primeCyclotomicPushout_numberField

L230 ↗
KummerTheory.primeCyclotomicPushout_numberField
Documentation

The prime cyclotomic pushout is again a number field.

Source context 7 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace KummerTheory
universe u
variable
    (K L : Type u)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [IsGalois K L]
omit [IsGalois K L] in
Lean source · full declaration
theorem primeCyclotomicPushout_numberField
    (p : ℕ) (hp : p.Prime)
    (hdegree : Module.finrank K L = p) :
    letI : NeZero p := ⟨hp.ne_zero⟩
    letI : Field (PrimeCyclotomicPushout K L p) :=
      primeCyclotomicPushoutField K L p hp hdegree
    letI : Algebra
        (PrimeCyclotomicBase K p)
        (PrimeCyclotomicPushout K L p) :=
      primeCyclotomicPushoutAlgebra K L p hp hdegree
    NumberField (PrimeCyclotomicPushout K L p) := by
  let : NeZero p := ⟨hp.ne_zero⟩
  let : Field (PrimeCyclotomicPushout K L p) :=
    primeCyclotomicPushoutField K L p hp hdegree
  let : Algebra
      (PrimeCyclotomicBase K p)
      (PrimeCyclotomicPushout K L p) :=
    primeCyclotomicPushoutAlgebra K L p hp hdegree
  exact
    NumberField.of_module_finite
      (PrimeCyclotomicBase K p)
      (PrimeCyclotomicPushout K L p)
theorem

primeCyclotomicBase_primitiveRoots_nonempty

L254 ↗
KummerTheory.primeCyclotomicBase_primitiveRoots_nonempty
Documentation

The cyclotomic base contains a primitive p-th root of unity.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace KummerTheory
universe u
variable
    (K L : Type u)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [IsGalois K L]
Lean source · statement
theorem primeCyclotomicBase_primitiveRoots_nonempty
    (p : ℕ) (hp : p.Prime) :
    (primitiveRoots p (PrimeCyclotomicBase K p)).Nonempty
theorem

primeCyclotomicPushout_isCyclic

L265 ↗
KummerTheory.primeCyclotomicPushout_isCyclic
Documentation

The Galois group after cyclotomic base change is cyclic of prime order.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace KummerTheory
universe u
variable
    (K L : Type u)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [IsGalois K L]
Lean source · full declaration
theorem primeCyclotomicPushout_isCyclic
    (p : ℕ) (hp : p.Prime)
    (hdegree : Module.finrank K L = p) :
    letI : NeZero p := ⟨hp.ne_zero⟩
    letI : Field (PrimeCyclotomicPushout K L p) :=
      primeCyclotomicPushoutField K L p hp hdegree
    letI : Algebra
        (PrimeCyclotomicBase K p)
        (PrimeCyclotomicPushout K L p) :=
      primeCyclotomicPushoutAlgebra K L p hp hdegree
    letI : IsGalois
        (PrimeCyclotomicBase K p)
        (PrimeCyclotomicPushout K L p) :=
      primeCyclotomicPushout_isGalois
        K L p hp hdegree
    IsCyclic
      (PrimeCyclotomicPushout K L p ≃ₐ[
        PrimeCyclotomicBase K p]
        PrimeCyclotomicPushout K L p) := by
  let : NeZero p := ⟨hp.ne_zero⟩
  let : Field (PrimeCyclotomicPushout K L p) :=
    primeCyclotomicPushoutField K L p hp hdegree
  let : Algebra
      (PrimeCyclotomicBase K p)
      (PrimeCyclotomicPushout K L p) :=
    primeCyclotomicPushoutAlgebra K L p hp hdegree
  let : IsGalois
      (PrimeCyclotomicBase K p)
      (PrimeCyclotomicPushout K L p) :=
    primeCyclotomicPushout_isGalois
      K L p hp hdegree
  let : Fact p.Prime := ⟨hp⟩
  exact
    isCyclic_of_prime_card (p := p) (by
      rw [IsGalois.card_aut_eq_finrank,
        primeCyclotomicPushout_finrank
          K L p hp hdegree])
def

primeCyclotomicPushoutGalEquivPiZMod

L305 ↗
KummerTheory.primeCyclotomicPushoutGalEquivPiZMod
Documentation

Prime-degree Kummer coordinates for the base-changed Galois group, in the exact one-coordinate form used by the prime-degree Kummer coordinate construction.

Source context 6 commands

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

open scoped NumberField TensorProduct
open NumberField
noncomputable section
namespace KummerTheory
universe u
variable
    (K L : Type u)
    [Field K] [NumberField K]
    [Field L] [NumberField L]
    [Algebra K L] [IsGalois K L]
Lean source · full declaration
def primeCyclotomicPushoutGalEquivPiZMod
    (p : ℕ) (hp : p.Prime)
    (hdegree : Module.finrank K L = p) :
    letI : NeZero p := ⟨hp.ne_zero⟩
    letI : Field (PrimeCyclotomicPushout K L p) :=
      primeCyclotomicPushoutField K L p hp hdegree
    letI : Algebra
        (PrimeCyclotomicBase K p)
        (PrimeCyclotomicPushout K L p) :=
      primeCyclotomicPushoutAlgebra K L p hp hdegree
    letI : IsGalois
        (PrimeCyclotomicBase K p)
        (PrimeCyclotomicPushout K L p) :=
      primeCyclotomicPushout_isGalois
        K L p hp hdegree
    (PrimeCyclotomicPushout K L p ≃ₐ[
        PrimeCyclotomicBase K p]
        PrimeCyclotomicPushout K L p) ≃*
      (Fin 1 → Multiplicative (ZMod p)) := by
  letI : NeZero p := ⟨hp.ne_zero⟩
  letI : Field (PrimeCyclotomicPushout K L p) :=
    primeCyclotomicPushoutField K L p hp hdegree
  letI : Algebra
      (PrimeCyclotomicBase K p)
      (PrimeCyclotomicPushout K L p) :=
    primeCyclotomicPushoutAlgebra K L p hp hdegree
  letI : IsGalois
      (PrimeCyclotomicBase K p)
      (PrimeCyclotomicPushout K L p) :=
    primeCyclotomicPushout_isGalois
      K L p hp hdegree
  let G :=
    PrimeCyclotomicPushout K L p ≃ₐ[
      PrimeCyclotomicBase K p]
      PrimeCyclotomicPushout K L p
  letI : IsCyclic G :=
    primeCyclotomicPushout_isCyclic
      K L p hp hdegree
  have hcardG : Nat.card G = p := by
    dsimp only [G]
    rw [IsGalois.card_aut_eq_finrank,
      primeCyclotomicPushout_finrank
        K L p hp hdegree]
  exact
    (hcardG ▸ (zmodCyclicMulEquiv
      (inferInstance : IsCyclic G)).symm).trans
      (MulEquiv.piUnique
        (fun _ : Fin 1 => Multiplicative (ZMod p))).symm

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