Module

ReciprocityMapMul.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.MainMultiplicativity.ReciprocityMapMul

1 declaration indexed from sourceView source ↗

Module documentation

Multiplicativity of the abstract reciprocity map

This file assembles the Frobenius conjugation, finite-stage unit, correction sum, and universal norm-descent results into reciprocity-map multiplicativity.

Mathlib's Rep ℤ G requires its coefficient ring and acting group in the same universe, so this representation-bearing portion has G : IntegralRepGroupType.

Imports6

Imported by2

theorem

reciprocityMap_mul

L51 ↗

ClassFormation.DegreeData.reciprocityMap_mul

Documentation

reciprocity multiplicativity. The reciprocity function is multiplicative on Frobenius elements (written additively on the norm-class quotient).

This is the endpoint of the calculation: the group-ring identity (*) supplies the hypothesis of the universal norm-descent lemma, whose universal-unit norm descends the resulting norm relation to K.

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 reciprocityMapMultiplicativity
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem reciprocityMap_mul
    (D : DegreeData G) (A : Rep ℤ G) (v : ValuationData D A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    [TotallyDisconnectedSpace G]
    (hAxiom : v.SatisfiesUnramifiedUnitCohomology D)
    (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)]
    (sigma1 sigma2 : D.FrobeniusElements
      (K.toFiniteResidueAbstractField D) L hLK) :
    D.reciprocityMap A v K L hLK (sigma1 * sigma2) =
      D.reciprocityMap A v K L hLK sigma1 +
        D.reciprocityMap A v K L hLK sigma2

Module documentation

Multiplicativity of the abstract reciprocity map

Declarations

reciprocityMap_mul