Module

CyclicPrimeDegreeSubextension.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Galois.CyclicPrimeDegreeSubextension

17 declarations indexed from sourceView source ↗

Module documentation

A prime-degree intermediate field of a finite cyclic extension

This file supplies an induction field for finite cyclic extensions. If L / K is a nontrivial finite cyclic Galois extension, choose a prime p ∣ [L : K]. For a generator σ of its Galois group, the subgroup generated by σ ^ p has index p. Its fixed field is therefore an actual cyclic Galois extension of K of degree p, while the remaining extension has degree [L : K] / p.

Imports1

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.ClassGroup.Tower

Imported by2

def

cyclicGaloisGenerator

L32 ↗

Documentation

A fixed generator of the cyclic Galois group.

Source context 3 commands

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

noncomputable section
variable {K L : Type}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
local notation "G" => L ≃ₐ[K] L

Lean source · statement

def cyclicGaloisGenerator : G

theorem

mem_zpowers_cyclicGaloisGenerator

L36 ↗

Source context 4 commands

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

noncomputable section
variable {K L : Type}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
local notation "G" => L ≃ₐ[K] L
omit [FiniteDimensional K L] [IsGalois K L] in

Lean source · statement

theorem mem_zpowers_cyclicGaloisGenerator (σ : G) :
    σ ∈ Subgroup.zpowers
      (cyclicGaloisGenerator (K := K) (L := L))

theorem

orderOf_cyclicGaloisGenerator

L41 ↗

Source context 3 commands

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

noncomputable section
variable {K L : Type}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
local notation "G" => L ≃ₐ[K] L

Lean source · statement

theorem orderOf_cyclicGaloisGenerator :
    orderOf (cyclicGaloisGenerator (K := K) (L := L)) =
      Module.finrank K L

def

cyclicDegreePrime

L49 ↗

Documentation

A prime divisor of the degree of a nontrivial cyclic extension.

Source context 3 commands

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

noncomputable section
variable {K L : Type}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
local notation "G" => L ≃ₐ[K] L

Lean source · statement

def cyclicDegreePrime
    (hdegree : 1 < Module.finrank K L) : ℕ

theorem

cyclicDegreePrime_prime

L56 ↗

Source context 4 commands

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

noncomputable section
variable {K L : Type}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
local notation "G" => L ≃ₐ[K] L
omit [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)] in

Lean source · statement

theorem cyclicDegreePrime_prime
    (hdegree : 1 < Module.finrank K L) :
    (cyclicDegreePrime (K := K) (L := L) hdegree).Prime

theorem

cyclicDegreePrime_dvd_finrank

L64 ↗

Source context 4 commands

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

noncomputable section
variable {K L : Type}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
local notation "G" => L ≃ₐ[K] L
omit [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)] in

Lean source · statement

theorem cyclicDegreePrime_dvd_finrank
    (hdegree : 1 < Module.finrank K L) :
    cyclicDegreePrime (K := K) (L := L) hdegree ∣
      Module.finrank K L

def

cyclicPrimeDegreeSubgroup

L72 ↗

Documentation

The subgroup generated by σ ^ p; it has index p.

Source context 3 commands

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

noncomputable section
variable {K L : Type}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
local notation "G" => L ≃ₐ[K] L

Lean source · statement

def cyclicPrimeDegreeSubgroup
    (hdegree : 1 < Module.finrank K L) :
    Subgroup G

theorem

cyclicPrimeDegreeSubgroup_card

L79 ↗

Source context 3 commands

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

noncomputable section
variable {K L : Type}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
local notation "G" => L ≃ₐ[K] L

Lean source · statement

theorem cyclicPrimeDegreeSubgroup_card
    (hdegree : 1 < Module.finrank K L) :
    Nat.card
        (cyclicPrimeDegreeSubgroup
          (K := K) (L := L) hdegree) =
      Module.finrank K L /
        cyclicDegreePrime (K := K) (L := L) hdegree

theorem

cyclicPrimeDegreeSubgroup_index

L96 ↗

Source context 3 commands

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

noncomputable section
variable {K L : Type}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
local notation "G" => L ≃ₐ[K] L

Lean source · statement

theorem cyclicPrimeDegreeSubgroup_index
    (hdegree : 1 < Module.finrank K L) :
    (cyclicPrimeDegreeSubgroup
      (K := K) (L := L) hdegree).index =
        cyclicDegreePrime (K := K) (L := L) hdegree

instance

cyclicPrimeDegreeSubgroup_normal

L136 ↗

Source context 3 commands

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

noncomputable section
variable {K L : Type}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
local notation "G" => L ≃ₐ[K] L

Lean source · statement

instance cyclicPrimeDegreeSubgroup_normal
    (hdegree : 1 < Module.finrank K L) :
    (cyclicPrimeDegreeSubgroup
      (K := K) (L := L) hdegree).Normal

def

cyclicPrimeDegreeIntermediate

L143 ↗

Documentation

The fixed field of the chosen index-prime subgroup.

Source context 3 commands

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

noncomputable section
variable {K L : Type}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
local notation "G" => L ≃ₐ[K] L

Lean source · statement

def cyclicPrimeDegreeIntermediate
    (hdegree : 1 < Module.finrank K L) :
    IntermediateField K L

instance

cyclicPrimeDegreeIntermediate_isGalois

L150 ↗

Source context 3 commands

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

noncomputable section
variable {K L : Type}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
local notation "G" => L ≃ₐ[K] L

Lean source · statement

instance cyclicPrimeDegreeIntermediate_isGalois
    (hdegree : 1 < Module.finrank K L) :
    IsGalois K
      (cyclicPrimeDegreeIntermediate
        (K := K) (L := L) hdegree)

theorem

cyclicPrimeDegreeIntermediate_finrank

L158 ↗

Source context 3 commands

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

noncomputable section
variable {K L : Type}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
local notation "G" => L ≃ₐ[K] L

Lean source · statement

theorem cyclicPrimeDegreeIntermediate_finrank
    (hdegree : 1 < Module.finrank K L) :
    Module.finrank K
        (cyclicPrimeDegreeIntermediate
          (K := K) (L := L) hdegree) =
      cyclicDegreePrime (K := K) (L := L) hdegree

theorem

cyclicPrimeDegreeIntermediate_top_finrank

L189 ↗

Source context 3 commands

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

noncomputable section
variable {K L : Type}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
local notation "G" => L ≃ₐ[K] L

Lean source · statement

theorem cyclicPrimeDegreeIntermediate_top_finrank
    (hdegree : 1 < Module.finrank K L) :
    Module.finrank
        (cyclicPrimeDegreeIntermediate
          (K := K) (L := L) hdegree)
        L =
      Module.finrank K L /
        cyclicDegreePrime (K := K) (L := L) hdegree

instance

cyclicPrimeDegreeIntermediate_top_isGalois

L201 ↗

Source context 3 commands

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

noncomputable section
variable {K L : Type}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
local notation "G" => L ≃ₐ[K] L

Lean source · statement

instance cyclicPrimeDegreeIntermediate_top_isGalois
    (hdegree : 1 < Module.finrank K L) :
    IsGalois
      (cyclicPrimeDegreeIntermediate
        (K := K) (L := L) hdegree)
      L

instance

cyclicPrimeDegreeIntermediate_base_isCyclic

L213 ↗

Source context 3 commands

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

noncomputable section
variable {K L : Type}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
local notation "G" => L ≃ₐ[K] L

Lean source · statement

instance cyclicPrimeDegreeIntermediate_base_isCyclic
    (hdegree : 1 < Module.finrank K L) :
    IsCyclic
      (cyclicPrimeDegreeIntermediate
          (K := K) (L := L) hdegree ≃ₐ[K]
        cyclicPrimeDegreeIntermediate
          (K := K) (L := L) hdegree)

instance

cyclicPrimeDegreeIntermediate_top_isCyclic

L232 ↗

Source context 3 commands

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

noncomputable section
variable {K L : Type}
    [Field K] [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [IsCyclic (L ≃ₐ[K] L)]
local notation "G" => L ≃ₐ[K] L

Lean source · statement

instance cyclicPrimeDegreeIntermediate_top_isCyclic
    (hdegree : 1 < Module.finrank K L) :
    IsCyclic
      (L ≃ₐ[
        cyclicPrimeDegreeIntermediate
          (K := K) (L := L) hdegree] L)

Module documentation

A prime-degree intermediate field of a finite cyclic extension

Declarations