Module

FixedTowerUnitCorrection.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.FixedTowerUnitCorrection

3 declarations indexed from sourceView source ↗

Module documentation

Fixed-tower unit correction

This module constructs the unit-valued correction term on a Frobenius fixed-field tower and proves its coefficient and relative-norm identities.

Imports1

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.FiniteFieldUnitMaps

Imported by2

def

fixedTowerCorrection

L38 ↗

ClassFormation.ValuationData.fixedTowerCorrection

Documentation

The unit-valued correction term on the upper Frobenius fixed field. This is the additive form of the right-hand side of the corrected equation.

Source context 10 commands

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

universe u v
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
open scoped BigOperators
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace ValuationData
variable {D : DegreeData G} {A : Rep ℤ G}

Lean source · statement

def fixedTowerCorrection
    (v : ValuationData D A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (K : DegreeData.FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    (σn : D.FrobeniusElements K L hLK)
    [Finite ((baseField G).toSubgroup ⧸
      extensionSubgroup (baseField G)
        (D.frobeniusFixedField K L hLK σn)
        (le_baseField (D.frobeniusFixedField K L hLK σn)))]
    {ι : Type v} (s : Finset ι)
    (φ : K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK)
    (hφσn : φ * σn.1 = σn.1 * φ)
    (τ : ι → K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK)
    (hτσn : ∀ i, τ i * σn.1 = σn.1 * τ i)
    (uBar :
      v.unitAddSubgroup (D.frobeniusFixedAbstractField K L hLK σn))
    (uBarᵢ : ι →
      v.unitAddSubgroup (D.frobeniusFixedAbstractField K L hLK σn)) :
    v.unitAddSubgroup (D.frobeniusFixedAbstractField K L hLK σn)

theorem

fixedTowerCorrection_coe

L70 ↗

ClassFormation.ValuationData.fixedTowerCorrection_coe

Documentation

The underlying fixed-tower correction is the Frobenius difference minus the prescribed finite sum of correction terms.

Source context 10 commands

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

universe u v
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
open scoped BigOperators
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace ValuationData
variable {D : DegreeData G} {A : Rep ℤ G}

Lean source · statement

theorem fixedTowerCorrection_coe
    (v : ValuationData D A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (K : DegreeData.FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    (σn : D.FrobeniusElements K L hLK)
    [Finite ((baseField G).toSubgroup ⧸
      extensionSubgroup (baseField G)
        (D.frobeniusFixedField K L hLK σn)
        (le_baseField (D.frobeniusFixedField K L hLK σn)))]
    {ι : Type v} (s : Finset ι)
    (φ : K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK)
    (hφσn : φ * σn.1 = σn.1 * φ)
    (τ : ι → K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK)
    (hτσn : ∀ i, τ i * σn.1 = σn.1 * τ i)
    (uBar :
      v.unitAddSubgroup (D.frobeniusFixedAbstractField K L hLK σn))
    (uBarᵢ : ι →
      v.unitAddSubgroup (D.frobeniusFixedAbstractField K L hLK σn)) :
    (v.fixedTowerCorrection K L hLK σn s φ hφσn
      τ hτσn uBar uBarᵢ).1 =
        (v.frobeniusFixedFieldUnitAction K L hLK σn
            φ hφσn uBar).1 -
          uBar.1 -
          ∑ i ∈ s,
            ((v.frobeniusFixedFieldUnitAction K L hLK σn
                (τ i) (hτσn i) (uBarᵢ i)).1 - (uBarᵢ i).1)

theorem

fixedTowerCorrection_relativeNorm_eq_zero

L111 ↗

ClassFormation.ValuationData.fixedTowerCorrection_relativeNorm_eq_zero

Documentation

Applying the lower norm to the correction term gives zero. This is the norm calculation immediately before the use of H⁻¹ = 0.

Source context 10 commands

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

universe u v
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
open scoped BigOperators
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace ValuationData
variable {D : DegreeData G} {A : Rep ℤ G}

Lean source · statement

theorem fixedTowerCorrection_relativeNorm_eq_zero
    (v : ValuationData D A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (K : DegreeData.FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    (σ σn : D.FrobeniusElements K L hLK)
    (hTS : (D.frobeniusFixedField K L hLK σn).toSubgroup ≤
      (D.frobeniusFixedField K L hLK σ).toSubgroup)
    [Finite ((D.frobeniusFixedField K L hLK σ).toSubgroup ⧸
      extensionSubgroup (D.frobeniusFixedField K L hLK σ)
        (D.frobeniusFixedField K L hLK σn) hTS)]
    [Finite ((baseField G).toSubgroup ⧸
      extensionSubgroup (baseField G)
        (D.frobeniusFixedField K L hLK σ)
        (le_baseField (D.frobeniusFixedField K L hLK σ)))]
    [Finite ((baseField G).toSubgroup ⧸
      extensionSubgroup (baseField G)
        (D.frobeniusFixedField K L hLK σn)
        (le_baseField (D.frobeniusFixedField K L hLK σn)))]
    {ι : Type v} (s : Finset ι)
    (φ : K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK)
    (hφσ : φ * σ.1 = σ.1 * φ)
    (hφσn : φ * σn.1 = σn.1 * φ)
    (τ : ι → K.field.toSubgroup ⧸ D.extensionInertiaWithin K.field L hLK)
    (hτσ : ∀ i, τ i * σ.1 = σ.1 * τ i)
    (hτσn : ∀ i, τ i * σn.1 = σn.1 * τ i)
    (u :
      v.unitAddSubgroup (D.frobeniusFixedAbstractField K L hLK σ))
    (uᵢ : ι →
      v.unitAddSubgroup (D.frobeniusFixedAbstractField K L hLK σ))
    (uBar :
      v.unitAddSubgroup (D.frobeniusFixedAbstractField K L hLK σn))
    (uBarᵢ : ι →
      v.unitAddSubgroup (D.frobeniusFixedAbstractField K L hLK σn))
    (huBar : relativeNorm A (D.frobeniusFixedField K L hLK σ)
      (D.frobeniusFixedField K L hLK σn) hTS uBar.1 = u.1)
    (huBarᵢ : ∀ i,
      relativeNorm A (D.frobeniusFixedField K L hLK σ)
        (D.frobeniusFixedField K L hLK σn) hTS
          (uBarᵢ i).1 = (uᵢ i).1)
    (hstar :
      A.ρ (Quotient.out φ).1 u.1.1 - u.1.1 =
        ∑ i ∈ s,
          (A.ρ (Quotient.out (τ i)).1 (uᵢ i).1.1 - (uᵢ i).1.1)) :
    relativeNorm A (D.frobeniusFixedField K L hLK σ)
      (D.frobeniusFixedField K L hLK σn) hTS
        (v.fixedTowerCorrection K L hLK σn s φ hφσn
          τ hτσn uBar uBarᵢ).1 = 0

Module documentation

Fixed-tower unit correction

Declarations

fixedTowerCorrection

fixedTowerCorrection_coe

fixedTowerCorrection_relativeNorm_eq_zero