NYLL
Module

PrimeElements.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Degree.PrimeElements
12 declarations indexed from sourceView source ↗

Module documentation

normalized degree and Frobenius theory: prime elements and units

This file formalizes the prime-element definition and its two immediate consequences for unramified and totally ramified extensions.

Imports1
Imported by4

Declarations

def

fixedFieldInclusion

L31 ↗
ClassFormation.fixedFieldInclusion
Documentation

Inclusion A_K → A_L for an extension L | K.

Source context 6 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
Lean source · full declaration
def fixedFieldInclusion (A : Rep ℤ G) (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup) :
    ambientFixedAddSubgroup A K →+ ambientFixedAddSubgroup A L where
  toFun a := ⟨a.1, fun l => a.2 ⟨l.1, hLK l.2⟩⟩
  map_zero' := rfl
  map_add' _ _ := rfl
theorem

fixedFieldInclusion_coe

L43 ↗
ClassFormation.fixedFieldInclusion_coe
Documentation

Establishes the identity ((fixedFieldInclusion A K L hLK a : ambientFixedAddSubgroup A L) : A.V) = a.1.

Source context 6 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
Lean source · statement
theorem fixedFieldInclusion_coe (A : Rep ℤ G) (K L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.toSubgroup)
    (a : ambientFixedAddSubgroup A K) :
    ((fixedFieldInclusion A K L hLK a : ambientFixedAddSubgroup A L) : A.V) = a.1
theorem

relativeNorm_fixedFieldInclusion

L50 ↗
ClassFormation.relativeNorm_fixedFieldInclusion
Documentation

The norm of an element already fixed over K is its [L:K]-fold sum.

Source context 6 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
Lean source · statement
theorem relativeNorm_fixedFieldInclusion
    (A : Rep ℤ G) (E : DegreeData.FiniteAbstractExtension G)
    (a : ambientFixedAddSubgroup A E.base) :
    relativeNorm A E.base E.field E.below
        (fixedFieldInclusion A E.base E.field E.below a) =
      (E.degree : ℕ) • a
theorem

relativeNorm_self

L79 ↗
ClassFormation.relativeNorm_self
Documentation

The norm of the trivial extension is the identity.

Source context 6 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
Lean source · statement
theorem relativeNorm_self
    (A : Rep ℤ G) (K : ClosedSubgroup G)
    [Finite (K.toSubgroup ⧸ extensionSubgroup K K le_rfl)]
    (a : ambientFixedAddSubgroup A K) :
    relativeNorm A K K le_rfl a = a
def

oneValue

L110 ↗
ClassFormation.ValuationData.oneValue
Documentation

The value 1 belongs to Z, by the valuation-quotient axiom.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace ValuationData
Lean source · statement
def oneValue (v : ValuationData D A) : v.valueGroup
theorem

oneValue_coe

L117 ↗
ClassFormation.ValuationData.oneValue_coe
Documentation

Establishes the identity (v.oneValue : ZHat) = 1.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace ValuationData
Lean source · statement
theorem oneValue_coe (v : ValuationData D A) :
    (v.oneValue : ZHat) = 1
def

IsPrimeElement

L122 ↗
ClassFormation.ValuationData.IsPrimeElement
Documentation

the prime-element definition. A prime element has normalized value 1.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace ValuationData
Lean source · statement
def IsPrimeElement (v : ValuationData D A) (K : FiniteAbstractField G)
    (π : ambientFixedAddSubgroup A K.field) : Prop
def

unitAddSubgroup

L128 ↗
ClassFormation.ValuationData.unitAddSubgroup
Documentation

the prime-element definition. The additive form of the unit group U_K = {u | v_K(u)=0}.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace ValuationData
Lean source · statement
def unitAddSubgroup (v : ValuationData D A) (K : FiniteAbstractField G) :
    AddSubgroup (ambientFixedAddSubgroup A K.field)
theorem

mem_unitAddSubgroup_iff

L134 ↗
ClassFormation.ValuationData.mem_unitAddSubgroup_iff
Documentation

Characterizes u ∈ v.unitAddSubgroup K by the equivalent condition v.valuationAt K u = 0.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace ValuationData
Lean source · statement
theorem mem_unitAddSubgroup_iff (v : ValuationData D A)
    (K : FiniteAbstractField G)
    (u : ambientFixedAddSubgroup A K.field) :
    u ∈ v.unitAddSubgroup K ↔ v.valuationAt K u = 0
theorem

valuationAt_fixedFieldInclusion_of_unramified

L142 ↗
ClassFormation.ValuationData.valuationAt_fixedFieldInclusion_of_unramified
Documentation

Over an unramified extension, the normalized valuation restricts to the valuation below.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace ValuationData
Lean source · statement
theorem valuationAt_fixedFieldInclusion_of_unramified
    (v : ValuationData D A)
    (E : FiniteAbstractFieldExtension G)
    (hUn : E.IsUnramified D)
    (a : ambientFixedAddSubgroup A E.base.field) :
    v.valuationAt E.field
        (fixedFieldInclusion A E.base.field E.field.field E.below a) =
      v.valuationAt E.base a
theorem

prime_of_unramified

L183 ↗
ClassFormation.ValuationData.prime_of_unramified
Documentation

A prime element remains prime in an unramified extension.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace ValuationData
Lean source · statement
theorem prime_of_unramified (v : ValuationData D A)
    (E : FiniteAbstractFieldExtension G)
    (hUn : E.IsUnramified D)
    (π : ambientFixedAddSubgroup A E.base.field)
    (hπ : v.IsPrimeElement E.base π) :
    v.IsPrimeElement E.field
      (fixedFieldInclusion A E.base.field E.field.field E.below π)
theorem

norm_prime_of_totallyRamified

L195 ↗
ClassFormation.ValuationData.norm_prime_of_totallyRamified
Documentation

The norm of a prime element is prime in a totally ramified extension.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
variable {D : DegreeData G} {A : Rep ℤ G}
namespace ValuationData
Lean source · statement
theorem norm_prime_of_totallyRamified (v : ValuationData D A)
    (E : FiniteAbstractFieldExtension G)
    (hTot : E.IsTotallyRamified D)
    (π : ambientFixedAddSubgroup A E.field.field) :
    v.IsPrimeElement E.field π →
      v.IsPrimeElement E.base
        (relativeNorm A E.base.field E.field.field E.below π)

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