Module

CorrectionSum.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.MainMultiplicativity.CorrectionSum

4 declarations indexed from sourceView source ↗

Module documentation

Correction sums for reciprocity multiplicativity

This file packages the three correction coefficients and action elements, proves their degree-zero property, and identifies their action-difference sum.

Imports1

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.MainMultiplicativity.FrobeniusActionRemainder

Imported by3

def

frobeniusMultiplicativityCorrectionTerm

L32 ↗

ClassFormation.frobeniusMultiplicativityCorrectionTerm

Documentation

Correction coefficients in the order produced by the left-action translation of the Frobenius multiplicativity identity.

Source context 7 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
open scoped BigOperators

Lean source · statement

def frobeniusMultiplicativityCorrectionTerm
    {R : IntegralRepGroupType} [Group R]
    (B : Rep ℤ R) (τ₁ : R) (p₁ p₃ p₄ : B.V) : Fin 3 → B.V

def

frobeniusMultiplicativityCorrectionAction

L40 ↗

ClassFormation.frobeniusMultiplicativityCorrectionAction

Documentation

The corresponding left-action elements are τ₄,τ₁,τ₄. The last action is τ₄ because the product in the actual (*) identity is τ₄τ₁.

Source context 7 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
open scoped BigOperators

Lean source · statement

def frobeniusMultiplicativityCorrectionAction {R : Type*} [Group R]
    (τ₁ τ₄ : R) : Fin 3 → R

theorem

frobeniusMultiplicativityCorrectionAction_mem_degreeKernel

L52 ↗

ClassFormation.DegreeData.frobeniusMultiplicativityCorrectionAction_mem_degreeKernel

Documentation

All three actual correction actions have normalized degree zero, as required by the universal norm-descent lemma.

Source context 10 commands

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

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

Lean source · full declaration

theorem frobeniusMultiplicativityCorrectionAction_mem_degreeKernel
    (D : DegreeData G)
    (K : FiniteResidueAbstractField D) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hLnormal : (extensionSubgroup K.field L hLK).Normal]
    (φ σ₁ σ₂ : D.FrobeniusElements K L hLK)
    (hφ : D.frobeniusExponent K L hLK φ = 1) :
    let σ₄ := D.frobeniusActionConjugate K L hLK φ σ₂
      (D.frobeniusExponent K L hLK σ₁)
    let τ₁ := D.frobeniusActionRemainder K L hLK φ σ₁
    let τ₄ := D.frobeniusActionRemainder K L hLK φ σ₄
    ∀ i : Fin 3,
      frobeniusMultiplicativityCorrectionAction τ₁ τ₄ i ∈
        (D.extensionNormalizedDegreeContinuous K L hLK).toMonoidHom.ker := by
  dsimp only
  let σ₄ := D.frobeniusActionConjugate K L hLK φ σ₂
    (D.frobeniusExponent K L hLK σ₁)
  let τ₁ := D.frobeniusActionRemainder K L hLK φ σ₁
  let τ₄ := D.frobeniusActionRemainder K L hLK φ σ₄
  have hτ₁ := D.frobeniusActionRemainder_mem_degreeKernel
    K L hLK φ σ₁ hφ
  have hτ₄ := D.frobeniusActionRemainder_mem_degreeKernel
    K L hLK φ σ₄ hφ
  intro i
  fin_cases i
  · exact hτ₄
  · exact hτ₁
  · exact hτ₄

theorem

frobeniusMultiplicativity_actionDifference_eq_correctionSum

L87 ↗

ClassFormation.frobeniusMultiplicativity_actionDifference_eq_correctionSum

Documentation

Explicit left-action form of the group-ring identity, with the factor order and the first two terms arranged as they occur in (*).

Source context 7 commands

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

universe u
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
open scoped BigOperators

Lean source · statement

theorem frobeniusMultiplicativity_actionDifference_eq_correctionSum
    {R : IntegralRepGroupType} [Group R] (B : Rep ℤ R)
    (τ₁ τ₄ : R) (p₁ p₃ p₄ : B.V) :
    (B.ρ τ₄ p₄ - p₄) + (B.ρ τ₁ p₁ - p₁) +
        (p₃ - B.ρ (τ₄ * τ₁) p₃) =
      ∑ i : Fin 3,
        (B.ρ (frobeniusMultiplicativityCorrectionAction τ₁ τ₄ i)
          (frobeniusMultiplicativityCorrectionTerm B τ₁ p₁ p₃ p₄ i) -
          frobeniusMultiplicativityCorrectionTerm B τ₁ p₁ p₃ p₄ i)

Module documentation

Correction sums for reciprocity multiplicativity

Declarations

frobeniusMultiplicativityCorrectionTerm

frobeniusMultiplicativityCorrectionAction

frobeniusMultiplicativityCorrectionAction_mem_degreeKernel

frobeniusMultiplicativity_actionDifference_eq_correctionSum