Module

PrimeChoice.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.PrimeChoice

5 declarations indexed from sourceView source ↗

Module documentation

The abstract reciprocity construction: choosing prime elements

Surjectivity of the normalized valuation supplies a prime element in every finite abstract field. Any two choices differ by a unit (additively, their difference has value zero).

Imports1

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Degree.PrimeElements

Imported by2

def

chosenPrimeElement

L35 ↗

ClassFormation.ValuationData.chosenPrimeElement

Documentation

A chosen prime element of a finite abstract field. Later independence lemmas show that the reciprocity class does not depend on this choice.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
namespace ValuationData

-- 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

def chosenPrimeElement (v : ValuationData D A) (K : FiniteAbstractField G) :
    ambientFixedAddSubgroup A K.field

theorem

valuationAt_chosenPrimeElement

L41 ↗

ClassFormation.ValuationData.valuationAt_chosenPrimeElement

Documentation

Establishes the identity v.valuationAt K (v.chosenPrimeElement K) = v.oneValue.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
namespace ValuationData

-- 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 valuationAt_chosenPrimeElement (v : ValuationData D A)
    (K : FiniteAbstractField G) :
    v.valuationAt K (v.chosenPrimeElement K) = v.oneValue

theorem

chosenPrimeElement_isPrime

L47 ↗

ClassFormation.ValuationData.chosenPrimeElement_isPrime

Documentation

The chosen prime element has valuation equal to the distinguished degree-one value.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
namespace ValuationData

-- 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 chosenPrimeElement_isPrime (v : ValuationData D A)
    (K : FiniteAbstractField G) :
    v.IsPrimeElement K (v.chosenPrimeElement K)

theorem

sub_mem_unitAddSubgroup_of_prime

L53 ↗

ClassFormation.ValuationData.sub_mem_unitAddSubgroup_of_prime

Documentation

In additive notation, two prime elements differ by a unit.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
namespace ValuationData

-- 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 sub_mem_unitAddSubgroup_of_prime
    (v : ValuationData D A) (K : FiniteAbstractField G)
    {π π' : ambientFixedAddSubgroup A K.field}
    (hπ : v.IsPrimeElement K π) (hπ' : v.IsPrimeElement K π') :
    π' - π ∈ v.unitAddSubgroup K

theorem

sub_chosenPrimeElement_mem_unitAddSubgroup

L62 ↗

ClassFormation.ValuationData.sub_chosenPrimeElement_mem_unitAddSubgroup

Documentation

Establishes the membership statement π - v.chosenPrimeElement K ∈ v.unitAddSubgroup K.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
namespace ValuationData

-- 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 sub_chosenPrimeElement_mem_unitAddSubgroup
    (v : ValuationData D A) (K : FiniteAbstractField G)
    {π : ambientFixedAddSubgroup A K.field}
    (hπ : v.IsPrimeElement K π) :
    π - v.chosenPrimeElement K ∈ v.unitAddSubgroup K

Module documentation

The abstract reciprocity construction: choosing prime elements

Declarations

chosenPrimeElement

valuationAt_chosenPrimeElement

chosenPrimeElement_isPrime

sub_mem_unitAddSubgroup_of_prime

sub_chosenPrimeElement_mem_unitAddSubgroup