NYLL
Module

MaximalUnramifiedSymbol.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.MaximalUnramifiedSymbol
22 declarations indexed from sourceView source ↗

Module documentation

Abstract reciprocity: the maximal-unramified symbol

This file constructs the source maps used in maximal-unramified reciprocity. In particular, the maximal unramified quotient is projected to every finite unramified Galois quotient, and its Frobenius is sent to the finite arithmetic Frobenius. The valuation--Frobenius map below is kept as a candidate until its compatibility with the finite norm-residue symbols has been proved from the unramified norm-quotient equivalence.

Imports1
Imported by2

Declarations

def

maximalUnramifiedExtensionRestriction

L39 ↗
ClassFormation.DegreeData.maximalUnramifiedExtensionRestriction
Documentation

Restriction from the maximal unramified Galois group over K to the actual quotient of an unramified Galois extension L / K. This construction does not require the quotient to be finite.

Source context 7 commands

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

noncomputable section
namespace ClassFormation
open ClassFormation CyclicCohomology KummerTheory
universe u
section DegreeOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
def maximalUnramifiedExtensionRestriction
    (D : DegreeData G) (K : FiniteResidueAbstractField D)
    (L : GaloisSubextension K.field)
    (hUnramified : L.IsUnramified D) :
    (K.field.toSubgroup ⧸ D.fieldInertiaWithin K.field) →*
      L.extensionQuotient
theorem

maximalUnramifiedExtensionRestriction_mk

L58 ↗
ClassFormation.DegreeData.maximalUnramifiedExtensionRestriction_mk
Documentation

Establishes the identity maximalUnramifiedExtensionRestriction D K L hUnramified (QuotientGroup.mk k) = L.extensionQuotientMk k.

Source context 7 commands

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

noncomputable section
namespace ClassFormation
open ClassFormation CyclicCohomology KummerTheory
universe u
section DegreeOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem maximalUnramifiedExtensionRestriction_mk
    (D : DegreeData G) (K : FiniteResidueAbstractField D)
    (L : GaloisSubextension K.field)
    (hUnramified : L.IsUnramified D)
    (k : K.field.toSubgroup) :
    maximalUnramifiedExtensionRestriction D K L hUnramified
        (QuotientGroup.mk k) =
      L.extensionQuotientMk k
theorem

maximalUnramifiedRestriction_frobenius

L73 ↗
ClassFormation.DegreeData.maximalUnramifiedRestriction_frobenius
Documentation

Restriction sends the maximal-unramified Frobenius to the arithmetic Frobenius of every finite unramified quotient.

Source context 7 commands

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

noncomputable section
namespace ClassFormation
open ClassFormation CyclicCohomology KummerTheory
universe u
section DegreeOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem maximalUnramifiedRestriction_frobenius
    (D : DegreeData G) (K : FiniteResidueAbstractField D)
    (L : GaloisSubextension K.field)
    (hUnramified : L.IsUnramified D) :
    maximalUnramifiedExtensionRestriction D K L hUnramified
        (D.frobenius K) =
      L.extensionQuotientMulEquiv.symm
        (D.unramifiedFrobenius K L.field L.below)
def

finiteUnramifiedRestriction

L103 ↗
ClassFormation.DegreeData.finiteUnramifiedRestriction
Documentation

Restriction to a bundled finite Galois extension. The named comparison between the finite and non-finite Galois quotient boundaries is applied here, once, rather than left to definitional unfolding in every consumer.

Source context 7 commands

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

noncomputable section
namespace ClassFormation
open ClassFormation CyclicCohomology KummerTheory
universe u
section DegreeOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
def finiteUnramifiedRestriction
    (D : DegreeData G) (K : FiniteResidueAbstractField D)
    (L : FiniteGaloisSubextension K.field)
    (hUnramified : L.IsUnramified D) :
    (K.field.toSubgroup ⧸ D.fieldInertiaWithin K.field) →*
      L.extensionQuotient
theorem

finiteUnramifiedRestriction_mk

L118 ↗
ClassFormation.DegreeData.finiteUnramifiedRestriction_mk
Documentation

Establishes the identity finiteUnramifiedRestriction D K L hUnramified (QuotientGroup.mk k) = L.extensionQuotientMk k.

Source context 7 commands

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

noncomputable section
namespace ClassFormation
open ClassFormation CyclicCohomology KummerTheory
universe u
section DegreeOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem finiteUnramifiedRestriction_mk
    (D : DegreeData G) (K : FiniteResidueAbstractField D)
    (L : FiniteGaloisSubextension K.field)
    (hUnramified : L.IsUnramified D) (k : K.field.toSubgroup) :
    finiteUnramifiedRestriction D K L hUnramified (QuotientGroup.mk k) =
      L.extensionQuotientMk k
theorem

finiteUnramifiedRestriction_frobenius

L133 ↗
ClassFormation.DegreeData.finiteUnramifiedRestriction_frobenius
Documentation

Establishes the identity finiteUnramifiedRestriction D K L hUnramified (D.frobenius K) = L.extensionQuotientMulEquiv.symm (D.unramifiedFrobenius K L.field L.below).

Source context 7 commands

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

noncomputable section
namespace ClassFormation
open ClassFormation CyclicCohomology KummerTheory
universe u
section DegreeOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem finiteUnramifiedRestriction_frobenius
    (D : DegreeData G) (K : FiniteResidueAbstractField D)
    (L : FiniteGaloisSubextension K.field)
    (hUnramified : L.IsUnramified D) :
    finiteUnramifiedRestriction D K L hUnramified (D.frobenius K) =
      L.extensionQuotientMulEquiv.symm
        (D.unramifiedFrobenius K L.field L.below)
theorem

finiteUnramifiedDegreeHom_killsExtension

L149 ↗
ClassFormation.DegreeData.finiteUnramifiedDegreeHom_killsExtension
Source context 7 commands

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

noncomputable section
namespace ClassFormation
open ClassFormation CyclicCohomology KummerTheory
universe u
section DegreeOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem finiteUnramifiedDegreeHom_killsExtension
    (D : DegreeData G) (K : FiniteResidueAbstractField D)
    (L : FiniteGaloisSubextension K.field)
    (hUnramified : L.IsUnramified D) :
    extensionSubgroup K.field L.field L.below ≤
      (((zHatReductionMul
        (L.toFiniteAbstractExtension.degree : ℕ)
        L.toFiniteAbstractExtension.degree.property).comp
        (D.normalizedDegree K)).toMonoidHom).ker
def

finiteUnramifiedDegreeHom

L212 ↗
ClassFormation.DegreeData.finiteUnramifiedDegreeHom
Documentation

Normalized degree modulo [L : K] on a finite unramified Galois quotient.

Source context 7 commands

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

noncomputable section
namespace ClassFormation
open ClassFormation CyclicCohomology KummerTheory
universe u
section DegreeOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
def finiteUnramifiedDegreeHom
    (D : DegreeData G) (K : FiniteResidueAbstractField D)
    (L : FiniteGaloisSubextension K.field)
    (hUnramified : L.IsUnramified D) :
    L.extensionQuotient →*
      Multiplicative
        (ZMod (L.toFiniteAbstractExtension.degree : ℕ))
theorem

finiteUnramifiedDegreeHom_mk

L233 ↗
ClassFormation.DegreeData.finiteUnramifiedDegreeHom_mk
Documentation

Establishes the identity finiteUnramifiedDegreeHom D K L hUnramified (L.extensionQuotientMk k) = zHatReductionMul (L.toFiniteAbstractExtension.degree : ℕ) L.toFiniteAbstractExtension.degree.property (D.normalizedDegree K k).

Source context 7 commands

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

noncomputable section
namespace ClassFormation
open ClassFormation CyclicCohomology KummerTheory
universe u
section DegreeOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem finiteUnramifiedDegreeHom_mk
    (D : DegreeData G) (K : FiniteResidueAbstractField D)
    (L : FiniteGaloisSubextension K.field)
    (hUnramified : L.IsUnramified D)
    (k : K.field.toSubgroup) :
    finiteUnramifiedDegreeHom D K L hUnramified
        (L.extensionQuotientMk k) =
      zHatReductionMul
        (L.toFiniteAbstractExtension.degree : ℕ)
        L.toFiniteAbstractExtension.degree.property
        (D.normalizedDegree K k)
theorem

finiteUnramifiedDegreeHom_surjective

L251 ↗
ClassFormation.DegreeData.finiteUnramifiedDegreeHom_surjective
Documentation

The specified map is surjective: Function.Surjective (finiteUnramifiedDegreeHom D K L hUnramified).

Source context 7 commands

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

noncomputable section
namespace ClassFormation
open ClassFormation CyclicCohomology KummerTheory
universe u
section DegreeOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem finiteUnramifiedDegreeHom_surjective
    (D : DegreeData G) (K : FiniteResidueAbstractField D)
    (L : FiniteGaloisSubextension K.field)
    (hUnramified : L.IsUnramified D) :
    Function.Surjective
      (finiteUnramifiedDegreeHom D K L hUnramified)
def

finiteUnramifiedDegreeEquiv

L273 ↗
ClassFormation.DegreeData.finiteUnramifiedDegreeEquiv
Documentation

For an unramified finite extension, normalized degree modulo the extension degree is an isomorphism.

Source context 7 commands

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

noncomputable section
namespace ClassFormation
open ClassFormation CyclicCohomology KummerTheory
universe u
section DegreeOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
def finiteUnramifiedDegreeEquiv
    (D : DegreeData G) (K : FiniteResidueAbstractField D)
    (L : FiniteGaloisSubextension K.field)
    (hUnramified : L.IsUnramified D) :
    L.extensionQuotient ≃*
      Multiplicative (ZMod (L.toFiniteAbstractExtension.degree : ℕ))
theorem

finiteUnramifiedDegreeEquiv_restriction

L312 ↗
ClassFormation.DegreeData.finiteUnramifiedDegreeEquiv_restriction
Documentation

The maximal and finite normalized-degree isomorphisms commute with restriction and reduction modulo [L : K].

Source context 7 commands

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

noncomputable section
namespace ClassFormation
open ClassFormation CyclicCohomology KummerTheory
universe u
section DegreeOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem finiteUnramifiedDegreeEquiv_restriction
    (D : DegreeData G) (K : FiniteResidueAbstractField D)
    (L : FiniteGaloisSubextension K.field)
    (hUnramified : L.IsUnramified D)
    (x : K.field.toSubgroup ⧸ D.fieldInertiaWithin K.field) :
    finiteUnramifiedDegreeEquiv D K L hUnramified
        (finiteUnramifiedRestriction D K L hUnramified x) =
      zHatReductionMul
        (L.toFiniteAbstractExtension.degree : ℕ)
        L.toFiniteAbstractExtension.degree.property
        (D.maximalUnramifiedDegreeEquiv K x)
theorem

finiteUnramifiedDegreeEquiv_unramifiedFrobenius

L332 ↗
ClassFormation.DegreeData.finiteUnramifiedDegreeEquiv_unramifiedFrobenius
Documentation

The arithmetic Frobenius has finite normalized degree one.

Source context 7 commands

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

noncomputable section
namespace ClassFormation
open ClassFormation CyclicCohomology KummerTheory
universe u
section DegreeOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem finiteUnramifiedDegreeEquiv_unramifiedFrobenius
    (D : DegreeData G) (K : FiniteResidueAbstractField D)
    (L : FiniteGaloisSubextension K.field)
    (hUnramified : L.IsUnramified D) :
    finiteUnramifiedDegreeEquiv D K L hUnramified
        (L.extensionQuotientMulEquiv.symm
          (D.unramifiedFrobenius K L.field L.below)) =
      Multiplicative.ofAdd
        (1 : ZMod (L.toFiniteAbstractExtension.degree : ℕ))
def

maximalUnramifiedFrobeniusPower

L349 ↗
ClassFormation.DegreeData.maximalUnramifiedFrobeniusPower
Documentation

Profinite exponentiation of the maximal-unramified Frobenius, expressed through the canonical degree isomorphism with ℤ̂.

Source context 7 commands

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

noncomputable section
namespace ClassFormation
open ClassFormation CyclicCohomology KummerTheory
universe u
section DegreeOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
def maximalUnramifiedFrobeniusPower
    (D : DegreeData G) (K : FiniteResidueAbstractField D) (z : ZHat) :
    Additive (K.field.toSubgroup ⧸ D.fieldInertiaWithin K.field)
theorem

maximalUnramifiedFrobeniusPower_one

L358 ↗
ClassFormation.DegreeData.maximalUnramifiedFrobeniusPower_one
Documentation

Establishes the identity maximalUnramifiedFrobeniusPower D K 1 = Additive.ofMul (D.frobenius K).

Source context 7 commands

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

noncomputable section
namespace ClassFormation
open ClassFormation CyclicCohomology KummerTheory
universe u
section DegreeOnly
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData
Lean source · statement
theorem maximalUnramifiedFrobeniusPower_one
    (D : DegreeData G) (K : FiniteResidueAbstractField D) :
    maximalUnramifiedFrobeniusPower D K 1 =
      Additive.ofMul (D.frobenius K)
theorem

canonicalUnramifiedReciprocity_degree_of_generator

L382 ↗
ClassFormation.ValuationData.canonicalUnramifiedReciprocity_degree_of_generator
Documentation

A finite unramified reciprocity homomorphism which sends Frobenius to the prime class intertwines the canonical valuation and normalized-degree isomorphisms. This is the generator calculation in the unramified norm-quotient equivalence, expressed in the normalization needed.

Source context 9 commands

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

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

-- 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}
open DegreeData
namespace ValuationData
Lean source · full declaration
theorem canonicalUnramifiedReciprocity_degree_of_generator
    (v : ValuationData D A)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    (K : FiniteAbstractField G) (L : FiniteGaloisSubextension K.field) :
    letI : Finite
        (K.field.toSubgroup ⧸
          extensionSubgroup K.field L.field L.below) := L.finite
    ∀ (hUnramified : L.IsUnramified D)
      (r : Additive L.extensionQuotient →+
        FiniteNormQuotient A K.field L.field L.below)
      (_hr : r (Additive.ofMul (D.unramifiedFrobenius
          (K.toFiniteResidueAbstractField D) L.field L.below)) =
        finiteNormClass A K.field L.field L.below (v.chosenPrimeElement K))
      (q : Additive L.extensionQuotient),
    v.canonicalUnramifiedNormQuotientValuation
        L.toFiniteAbstractFieldExtension hUnramified
        (r q) =
      (finiteUnramifiedDegreeEquiv D (K.toFiniteResidueAbstractField D)
        L hUnramified
        q.toMul).toAdd := by
  let : Finite
      (K.field.toSubgroup ⧸
        extensionSubgroup K.field L.field L.below) := L.finite
  intro hUnramified r hr q
  let KR := K.toFiniteResidueAbstractField D
  let g : Additive L.extensionQuotient :=
    Additive.ofMul (D.unramifiedFrobenius KR L.field L.below)
  let lhs : Additive L.extensionQuotient →+
      ZMod (L.toFiniteAbstractFieldExtension.degree : ℕ) :=
    (v.canonicalUnramifiedNormQuotientValuation
      L.toFiniteAbstractFieldExtension hUnramified).comp r
  let rhs : Additive L.extensionQuotient →+
      ZMod (L.toFiniteAbstractFieldExtension.degree : ℕ) :=
    (finiteUnramifiedDegreeEquiv D
      KR L hUnramified).toAdditive.toAddMonoidHom
  change lhs q = rhs q
  have hgen : lhs g = rhs g := by
    change v.canonicalUnramifiedNormQuotientValuation
        L.toFiniteAbstractFieldExtension hUnramified
        (r g) =
      (finiteUnramifiedDegreeEquiv D KR L hUnramified
        g.toMul).toAdd
    rw [show r g = finiteNormClass A K.field L.field L.below
        (v.chosenPrimeElement K) from hr]
    change v.canonicalUnramifiedValuationHom
      L.toFiniteAbstractFieldExtension
      (v.chosenPrimeElement K) = _
    change v.canonicalValueReduction
        (L.toFiniteAbstractFieldExtension.degree : ℕ)
        _ (v.valuationAt K (v.chosenPrimeElement K)) = _
    exact (congrArg
      (v.canonicalValueReduction (L.toFiniteAbstractFieldExtension.degree : ℕ)
        L.toFiniteAbstractFieldExtension.degree.property)
      (v.valuationAt_chosenPrimeElement K)).trans <|
      (v.canonicalValueReduction_one (L.toFiniteAbstractFieldExtension.degree : ℕ)
        L.toFiniteAbstractFieldExtension.degree.property).trans <|
        congrArg Multiplicative.toAdd
          (finiteUnramifiedDegreeEquiv_unramifiedFrobenius D
            KR L hUnramified).symm
  have hqmem : q ∈ AddSubgroup.zmultiples g := by
    rw [show AddSubgroup.zmultiples g = ⊤ from
      D.unramifiedFrobenius_zmultiples_eq_top
        KR L.field L.below hUnramified]
    trivial
  obtain ⟨m, hm⟩ := AddSubgroup.mem_zmultiples_iff.mp hqmem
  rw [← hm, map_zsmul, map_zsmul, hgen]
def

maximalUnramifiedNormResidueSymbol

L451 ↗
ClassFormation.ValuationData.maximalUnramifiedNormResidueSymbol
Documentation

The maximal-unramified norm-residue symbol, given by the valuation--Frobenius homomorphism.

Source context 9 commands

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

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

-- 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}
open DegreeData
namespace ValuationData
Lean source · statement
def maximalUnramifiedNormResidueSymbol
    (v : ValuationData D A)
    (K : FiniteAbstractField G) :
    ambientFixedAddSubgroup A K.field →+
      Additive (K.field.toSubgroup ⧸ D.fieldInertiaWithin K.field)
theorem

maximalUnramifiedNormResidue_degree

L462 ↗
ClassFormation.ValuationData.maximalUnramifiedNormResidue_degree
Documentation

Applying normalized degree to the maximal-unramified symbol recovers the valuation.

Source context 9 commands

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

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

-- 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}
open DegreeData
namespace ValuationData
Lean source · statement
theorem maximalUnramifiedNormResidue_degree
    (v : ValuationData D A)
    (K : FiniteAbstractField G)
    (a : ambientFixedAddSubgroup A K.field) :
    ((D.maximalUnramifiedDegreeEquiv (K.toFiniteResidueAbstractField D)
      (maximalUnramifiedNormResidueSymbol v K a).toMul).toAdd : ZHat) =
        (v.valuationAt K a : ZHat)
theorem

maximalUnramifiedNormResidue_eq_frobeniusPower

L481 ↗
ClassFormation.ValuationData.maximalUnramifiedNormResidue_eq_frobeniusPower
Documentation

The maximal-unramified symbol is literally the profinite power φ_K ^ v_K(a).

Source context 9 commands

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

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

-- 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}
open DegreeData
namespace ValuationData
Lean source · statement
theorem maximalUnramifiedNormResidue_eq_frobeniusPower
    (v : ValuationData D A)
    (K : FiniteAbstractField G)
    (a : ambientFixedAddSubgroup A K.field) :
    maximalUnramifiedNormResidueSymbol v K a =
      maximalUnramifiedFrobeniusPower D (K.toFiniteResidueAbstractField D)
        (v.valuationAt K a : ZHat)
theorem

maximalUnramifiedNormResidueSymbol_finiteDegree

L492 ↗
ClassFormation.ValuationData.maximalUnramifiedNormResidueSymbol_finiteDegree
Documentation

At every finite unramified quotient, normalized degree of the maximal-unramified symbol is valuation reduced modulo the extension degree.

Source context 9 commands

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

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

-- 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}
open DegreeData
namespace ValuationData
Lean source · statement
theorem maximalUnramifiedNormResidueSymbol_finiteDegree
    (v : ValuationData D A)
    (K : FiniteAbstractField G) (L : FiniteGaloisSubextension K.field)
    (hUnramified : L.IsUnramified D)
    (a : ambientFixedAddSubgroup A K.field) :
    (finiteUnramifiedDegreeEquiv D (K.toFiniteResidueAbstractField D)
      L hUnramified
      (finiteUnramifiedRestriction D
        (K.toFiniteResidueAbstractField D) L hUnramified
        (maximalUnramifiedNormResidueSymbol v K a).toMul)).toAdd =
      zHatReduction
        (L.toFiniteAbstractFieldExtension.degree : ℕ)
        L.toFiniteAbstractFieldExtension.degree.property
        (v.valuationAt K a : ZHat)
theorem

maximalUnramifiedNormResidueSymbol_finiteReciprocity_of_generator

L523 ↗
ClassFormation.ValuationData.maximalUnramifiedNormResidueSymbol_finiteReciprocity_of_generator
Documentation

The maximal-unramified symbol extends every finite unramified reciprocity map: after restriction to G(L/K), applying finite reciprocity gives the class of the original element. This is the non-circular compatibility statement which identifies the symbol with the inverse-limit norm-residue map.

Source context 9 commands

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

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

-- 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}
open DegreeData
namespace ValuationData
Lean source · full declaration
theorem maximalUnramifiedNormResidueSymbol_finiteReciprocity_of_generator
    (v : ValuationData D A) (hAxiom : v.SatisfiesUnramifiedUnitCohomology D)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    (K : FiniteAbstractField G) (L : FiniteGaloisSubextension K.field) :
    letI : Finite
        (K.field.toSubgroup ⧸
          extensionSubgroup K.field L.field L.below) := L.finite
    ∀ (hUnramified : L.IsUnramified D)
      (r : Additive L.extensionQuotient →+
        FiniteNormQuotient A K.field L.field L.below)
      (_hr : r (Additive.ofMul (D.unramifiedFrobenius
          (K.toFiniteResidueAbstractField D) L.field L.below)) =
        finiteNormClass A K.field L.field L.below (v.chosenPrimeElement K))
      (a : ambientFixedAddSubgroup A K.field),
    r (Additive.ofMul
        (finiteUnramifiedRestriction D
          (K.toFiniteResidueAbstractField D) L hUnramified
          (maximalUnramifiedNormResidueSymbol v K a).toMul)) =
      finiteNormClass A K.field L.field L.below a := by
  let : Finite
      (K.field.toSubgroup ⧸
        extensionSubgroup K.field L.field L.below) := L.finite
  intro hUnramified r hr a
  apply v.canonicalUnramifiedNormQuotientValuation_injective
    hAxiom L.toFiniteAbstractFieldExtension L.normal hUnramified
  rw [canonicalUnramifiedReciprocity_degree_of_generator v
    K L hUnramified r hr]
  change _ = v.canonicalUnramifiedValuationHom
    L.toFiniteAbstractFieldExtension a
  exact maximalUnramifiedNormResidueSymbol_finiteDegree v
    K L hUnramified a
theorem

maximalUnramifiedNormResidueSymbol_finiteRestriction_of_generator

L562 ↗
ClassFormation.ValuationData.maximalUnramifiedNormResidueSymbol_finiteRestriction_of_generator
Documentation

The finite restriction of the maximal-unramified symbol is the inverse of finite unramified reciprocity. The map r is kept explicit here so this statement records the uniqueness argument of maximal-unramified reciprocity without anticipating the final name of the finite reciprocity equivalence: the unramified norm-quotient equivalence promotes any reciprocity map with the Frobenius--prime value to an equivalence, and the preceding compatibility identifies its inverse.

Source context 9 commands

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

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

-- 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}
open DegreeData
namespace ValuationData
Lean source · full declaration
theorem maximalUnramifiedNormResidueSymbol_finiteRestriction_of_generator
    (v : ValuationData D A) (hAxiom : v.SatisfiesUnramifiedUnitCohomology D)
    [IsTopologicalGroup G] [CompactSpace G] [T2Space G]
    (K : FiniteAbstractField G) (L : FiniteGaloisSubextension K.field) :
    letI : Finite
        (K.field.toSubgroup ⧸
          extensionSubgroup K.field L.field L.below) := L.finite
    ∀ (hUnramified : L.IsUnramified D)
      (r : Additive L.extensionQuotient →+
        FiniteNormQuotient A K.field L.field L.below)
      (hr : r (Additive.ofMul (D.unramifiedFrobenius
          (K.toFiniteResidueAbstractField D) L.field L.below)) =
        finiteNormClass A K.field L.field L.below (v.chosenPrimeElement K))
      (a : ambientFixedAddSubgroup A K.field),
    (v.unramifiedReciprocity_equiv_of_generator hAxiom K L.field L.below
        hUnramified r hr).symm
        (finiteNormClass A K.field L.field L.below a) =
      Additive.ofMul
        (finiteUnramifiedRestriction D
          (K.toFiniteResidueAbstractField D) L hUnramified
          (maximalUnramifiedNormResidueSymbol v K a).toMul) := by
  let : Finite
      (K.field.toSubgroup ⧸
        extensionSubgroup K.field L.field L.below) := L.finite
  intro hUnramified r hr a
  apply (v.unramifiedReciprocity_equiv_of_generator hAxiom K L.field L.below
    hUnramified r hr).injective
  rw [AddEquiv.apply_symm_apply]
  exact (maximalUnramifiedNormResidueSymbol_finiteReciprocity_of_generator v hAxiom
    K L hUnramified r hr a).symm

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.