Module

ReciprocityDefinition.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.ReciprocityDefinition

5 declarations indexed from sourceView source ↗

Module documentation

The abstract reciprocity construction, the reciprocity construction: the reciprocity map

For a Frobenius element σ, let Σ be its fixed field. The reciprocity class is the class of N_{Σ|K}(π_Σ) in A_K / N_{\widetilde L|K} A_{\widetilde L}. Independence of the prime element is proved separately from the unit-cohomology axiom.

Imports4

Imported by3

def

frobeniusFixedIntermediateField

L41 ↗

ClassFormation.DegreeData.frobeniusFixedIntermediateField

Documentation

A finite intermediate-field package for the fixed field Σ of a Frobenius element.

Source context 8 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section frobeniusFixedFields
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · full declaration

def frobeniusFixedIntermediateField (D : DegreeData G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    [hLfinite : Finite
      (K.field.toSubgroup ⧸ extensionSubgroup K.field L hLK)]
    (σ : D.FrobeniusElements K L hLK) :
    FiniteIntermediateField (D.maximalUnramifiedField L) K.field where
  field := D.frobeniusFixedField K L hLK σ
  above := D.fieldInertia_le_frobeniusFixedField K L hLK σ
  below := D.frobeniusFixedField_le K L hLK σ
  finite := D.frobeniusFixedField_finite K L hLK σ

theorem

frobeniusFixedField_absoluteFinite

L56 ↗

ClassFormation.DegreeData.frobeniusFixedField_absoluteFinite

Documentation

Finiteness of Σ | k, obtained from the finite tower Σ | K | k.

Source context 8 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section frobeniusFixedFields
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · full declaration

theorem frobeniusFixedField_absoluteFinite (D : DegreeData G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    (K : FiniteAbstractField G) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    [hLfinite : Finite
      (K.field.toSubgroup ⧸ extensionSubgroup K.field L hLK)]
    (σ : D.FrobeniusElements (K.toFiniteResidueAbstractField D) L hLK
      (hLnormal := by
        simpa only [FiniteAbstractField.toFiniteResidueAbstractField] using hLnormal)) :
    Finite ((baseField G).toSubgroup ⧸
      extensionSubgroup (baseField G)
        (D.frobeniusFixedField (K.toFiniteResidueAbstractField D) L hLK
          (hLnormal := by
            simpa only [FiniteAbstractField.toFiniteResidueAbstractField] using hLnormal) σ)
        (le_baseField
          (D.frobeniusFixedField (K.toFiniteResidueAbstractField D) L hLK
            (hLnormal := by
              simpa only [FiniteAbstractField.toFiniteResidueAbstractField] using hLnormal) σ)))
                := by
  let KR := K.toFiniteResidueAbstractField D
  let hLnormalKR : (extensionSubgroup KR.field L hLK).Normal := by
    simpa only [KR, FiniteAbstractField.toFiniteResidueAbstractField] using hLnormal
  let hLfiniteKR : Finite
      (KR.field.toSubgroup ⧸ extensionSubgroup KR.field L hLK) := by
    simpa only [KR, FiniteAbstractField.toFiniteResidueAbstractField] using hLfinite
  let : Finite (K.field.toSubgroup ⧸
      extensionSubgroup K.field (D.frobeniusFixedField KR L hLK σ)
        (D.frobeniusFixedField_le KR L hLK σ)) :=
    D.frobeniusFixedField_finite KR L hLK σ
  exact relativeTowerQuotientFinite (baseField G) K.field
    (D.frobeniusFixedField KR L hLK σ)
    (D.frobeniusFixedField_le KR L hLK σ) (le_baseField K.field)

def

reciprocityValueOfPrime

L103 ↗

ClassFormation.DegreeData.reciprocityValueOfPrime

Documentation

The reciprocity construction with an explicit prime element π_Σ.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section reciprocityValues

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

Lean source · statement

def reciprocityValueOfPrime (D : DegreeData G) (A : Rep ℤ G)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    [hLfinite : Finite
      (K.field.toSubgroup ⧸ extensionSubgroup K.field L hLK)]
    (σ : D.FrobeniusElements K L hLK)
    (π : ambientFixedAddSubgroup A
      (D.frobeniusFixedField K L hLK σ)) :
    D.MaximalUnramifiedNormQuotient A K.field L

def

reciprocityMap

L126 ↗

ClassFormation.DegreeData.reciprocityMap

Documentation

the reciprocity construction. The reciprocity map on the Frobenius semigroup, using the canonical chosen prime supplied by surjectivity of v_Σ. The following independence theorem identifies this value with the formula for every prime element.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section reciprocityValues

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

Lean source · full declaration

def reciprocityMap (D : DegreeData G) (A : Rep ℤ G)
    (v : ValuationData D A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    (K : FiniteAbstractField G) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    [hLfinite : Finite
      (K.field.toSubgroup ⧸ extensionSubgroup K.field L hLK)] :
    D.FrobeniusElements (K.toFiniteResidueAbstractField D) L hLK
        (hLnormal := by
          simpa only [FiniteAbstractField.toFiniteResidueAbstractField] using hLnormal) →
      D.MaximalUnramifiedNormQuotient A K.field L :=
  fun σ => by
    let KR := K.toFiniteResidueAbstractField D
    letI hLnormalKR : (extensionSubgroup KR.field L hLK).Normal := by
      simpa only [KR, FiniteAbstractField.toFiniteResidueAbstractField] using hLnormal
    letI hLfiniteKR : Finite
        (KR.field.toSubgroup ⧸ extensionSubgroup KR.field L hLK) := by
      simpa only [KR, FiniteAbstractField.toFiniteResidueAbstractField] using hLfinite
    letI : Finite ((baseField G).toSubgroup ⧸
        extensionSubgroup (baseField G)
          (D.frobeniusFixedField KR L hLK σ)
          (le_baseField (D.frobeniusFixedField KR L hLK σ))) :=
      D.frobeniusFixedField_absoluteFinite K L hLK σ
    let Sigma : FiniteAbstractField G :=
      ⟨D.frobeniusFixedField KR L hLK σ, inferInstance⟩
    exact D.reciprocityValueOfPrime A KR L hLK σ
      (v.chosenPrimeElement Sigma)

theorem

reciprocityMap_eq_chosenPrime

L159 ↗

ClassFormation.DegreeData.reciprocityMap_eq_chosenPrime

Documentation

The reciprocity map at a Frobenius element is represented by the chosen prime element in its Frobenius fixed field.

Source context 9 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
section reciprocityValues

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

Lean source · full declaration

theorem reciprocityMap_eq_chosenPrime (D : DegreeData G) (A : Rep ℤ G)
    (v : ValuationData D A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    (K : FiniteAbstractField G) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    [hLfinite : Finite
      (K.field.toSubgroup ⧸ extensionSubgroup K.field L hLK)]
    (σ : D.FrobeniusElements (K.toFiniteResidueAbstractField D) L hLK
      (hLnormal := by
        simpa only [FiniteAbstractField.toFiniteResidueAbstractField] using hLnormal)) :
    D.reciprocityMap A v K L hLK σ = by
      let KR := K.toFiniteResidueAbstractField D
      letI : (extensionSubgroup KR.field L hLK).Normal := by
        simpa only [KR, FiniteAbstractField.toFiniteResidueAbstractField] using hLnormal
      letI hLfiniteKR : Finite
          (KR.field.toSubgroup ⧸ extensionSubgroup KR.field L hLK) := by
        simpa only [KR, FiniteAbstractField.toFiniteResidueAbstractField] using hLfinite
      letI : Finite ((baseField G).toSubgroup ⧸
          extensionSubgroup (baseField G)
            (D.frobeniusFixedField KR L hLK σ)
            (le_baseField (D.frobeniusFixedField KR L hLK σ))) :=
        D.frobeniusFixedField_absoluteFinite K L hLK σ
      let Sigma : FiniteAbstractField G :=
        ⟨D.frobeniusFixedField KR L hLK σ, inferInstance⟩
      simpa only [Sigma, KR, FiniteAbstractField.toFiniteResidueAbstractField] using
        (D.reciprocityValueOfPrime A KR L hLK σ
          (v.chosenPrimeElement Sigma)) :=
  rfl

Module documentation

The abstract reciprocity construction, the reciprocity construction: the reciprocity map

Declarations

frobeniusFixedIntermediateField

frobeniusFixedField_absoluteFinite

reciprocityValueOfPrime

reciprocityMap

reciprocityMap_eq_chosenPrime