Module

UnramifiedNormQuotient.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.UnramifiedNormQuotient

15 declarations indexed from sourceView source ↗

Module documentation

The abstract reciprocity construction, the unramified norm-quotient equivalence: the

unramified norm quotient

For a finite unramified Galois extension L / K, normalized valuation identifies the actual norm quotient A_K / N_{L/K} A_L with ℤ / [L : K]ℤ. The only non-formal part of injectivity is the unit correction: the unit-cohomology axiom (H⁰ = 0) makes every unit of K the norm of a unit of L.

Imports2

Imported by2

def

chosenUnramifiedFrobeniusLift

L40 ↗

ClassFormation.DegreeData.chosenUnramifiedFrobeniusLift

Documentation

The degree-one lift φ_K used in the unramified norm-quotient equivalence.

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 unramifiedFrobenius
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

def chosenUnramifiedFrobeniusLift
    (D : DegreeData G) (K : FiniteResidueAbstractField D)
    (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hnormal : (extensionSubgroup K.field L hLK).Normal] :
    D.FrobeniusElements K L hLK

theorem

chosenUnramifiedFrobeniusLift_exponent

L62 ↗

ClassFormation.DegreeData.chosenUnramifiedFrobeniusLift_exponent

Documentation

Establishes the identity D.frobeniusExponent K L hLK (D.chosenUnramifiedFrobeniusLift K L hLK) = 1.

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 unramifiedFrobenius
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem chosenUnramifiedFrobeniusLift_exponent
    (D : DegreeData G) (K : FiniteResidueAbstractField D)
    (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hnormal : (extensionSubgroup K.field L hLK).Normal] :
    D.frobeniusExponent K L hLK
      (D.chosenUnramifiedFrobeniusLift K L hLK) = 1

def

unramifiedFrobenius

L89 ↗

ClassFormation.DegreeData.unramifiedFrobenius

Documentation

The arithmetic Frobenius φ_{L/K}, obtained by restricting φ_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 unramifiedFrobenius
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

def unramifiedFrobenius
    (D : DegreeData G) (K : FiniteResidueAbstractField D)
    (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hnormal : (extensionSubgroup K.field L hLK).Normal] :
    K.field.toSubgroup ⧸ extensionSubgroup K.field L hLK

theorem

unramifiedFrobenius_generates

L100 ↗

ClassFormation.DegreeData.unramifiedFrobenius_generates

Documentation

In an unramified extension, arithmetic Frobenius generates the actual finite Galois quotient.

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 unramifiedFrobenius
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem unramifiedFrobenius_generates
    (D : DegreeData G) (K : FiniteResidueAbstractField D)
    (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hnormal : (extensionSubgroup K.field L hLK).Normal]
    [Finite (K.field.toSubgroup ⧸ extensionSubgroup K.field L hLK)]
    (hUnramified :
      (DegreeData.AbstractExtension.mk L K.field hLK).IsUnramified D) :
    ∀ x : K.field.toSubgroup ⧸ extensionSubgroup K.field L hLK,
      x ∈ Subgroup.zpowers (D.unramifiedFrobenius K L hLK)

theorem

unramifiedFrobenius_zmultiples_eq_top

L125 ↗

ClassFormation.DegreeData.unramifiedFrobenius_zmultiples_eq_top

Documentation

Additive form of the preceding generator statement, matching the domain of the reciprocity homomorphism in the finite reciprocity equivalence.

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 unramifiedFrobenius
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace DegreeData

Lean source · statement

theorem unramifiedFrobenius_zmultiples_eq_top
    (D : DegreeData G) (K : FiniteResidueAbstractField D)
    (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hnormal : (extensionSubgroup K.field L hLK).Normal]
    [Finite (K.field.toSubgroup ⧸ extensionSubgroup K.field L hLK)]
    (hUnramified :
      (DegreeData.AbstractExtension.mk L K.field hLK).IsUnramified D) :
    AddSubgroup.zmultiples
      (Additive.ofMul (D.unramifiedFrobenius K L hLK)) = ⊤

theorem

valueModulo_eq_zero_iff

L160 ↗

ClassFormation.ValuationData.valueModulo_eq_zero_iff

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 valuationQuotient

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

Lean source · statement

theorem valueModulo_eq_zero_iff
    (v : ValuationData D A) (n : ℕ) (hn : 0 < n)
    (z : v.valueGroup) :
    v.valueModulo n hn z = 0 ↔ ∃ w : v.valueGroup, z = n • w

def

unramifiedValuationHom

L183 ↗

ClassFormation.ValuationData.unramifiedValuationHom

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 valuationQuotient

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

Lean source · statement

def unramifiedValuationHom
    (v : ValuationData D A) (K : FiniteAbstractField G)
    (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [Finite (K.field.toSubgroup ⧸ extensionSubgroup K.field L hLK)] :
    ambientFixedAddSubgroup A K.field →+
      ZMod ((FiniteAbstractFieldExtension.ofInclusion L K hLK).degree : ℕ)

theorem

finiteNormSubgroup_le_unramifiedValuationHom_ker

L195 ↗

ClassFormation.ValuationData.finiteNormSubgroup_le_unramifiedValuationHom_ker

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 valuationQuotient

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

Lean source · statement

theorem finiteNormSubgroup_le_unramifiedValuationHom_ker
    (v : ValuationData D A)
    (K : FiniteAbstractField G) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [Finite (K.field.toSubgroup ⧸ extensionSubgroup K.field L hLK)]
    (hUnramified :
      (DegreeData.AbstractExtension.mk L K.field hLK).IsUnramified D) :
    finiteNormSubgroup A K.field L hLK ≤
      (v.unramifiedValuationHom K L hLK).ker

def

unramifiedNormQuotientValuation

L224 ↗

ClassFormation.ValuationData.unramifiedNormQuotientValuation

Documentation

The valuation map induced on the finite norm quotient.

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 valuationQuotient

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

Lean source · statement

def unramifiedNormQuotientValuation
    (v : ValuationData D A)
    (K : FiniteAbstractField G) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [Finite (K.field.toSubgroup ⧸ extensionSubgroup K.field L hLK)]
    (hUnramified :
      (DegreeData.AbstractExtension.mk L K.field hLK).IsUnramified D) :
    FiniteNormQuotient A K.field L hLK →+
      ZMod ((FiniteAbstractFieldExtension.ofInclusion L K hLK).degree : ℕ)

theorem

unramifiedNormQuotientValuation_finiteNormClass

L242 ↗

ClassFormation.ValuationData.unramifiedNormQuotientValuation_finiteNormClass

Documentation

Establishes the identity v.unramifiedNormQuotientValuation K L hLK hUnramified (finiteNormClass A K.field L hLK a) = v.unramifiedValuationHom K L hLK a.

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 valuationQuotient

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

Lean source · statement

theorem unramifiedNormQuotientValuation_finiteNormClass
    (v : ValuationData D A)
    (K : FiniteAbstractField G) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [Finite (K.field.toSubgroup ⧸ extensionSubgroup K.field L hLK)]
    (hUnramified :
      (DegreeData.AbstractExtension.mk L K.field hLK).IsUnramified D)
    (a : ambientFixedAddSubgroup A K.field) :
    v.unramifiedNormQuotientValuation K L hLK hUnramified
        (finiteNormClass A K.field L hLK a) =
      v.unramifiedValuationHom K L hLK a

theorem

unramifiedNormQuotientValuation_surjective

L259 ↗

ClassFormation.ValuationData.unramifiedNormQuotientValuation_surjective

Documentation

The specified map is surjective: Function.Surjective (v.unramifiedNormQuotientValuation K L hLK hUnramified).

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 valuationQuotient

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

Lean source · statement

theorem unramifiedNormQuotientValuation_surjective
    (v : ValuationData D A)
    (K : FiniteAbstractField G) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [Finite (K.field.toSubgroup ⧸ extensionSubgroup K.field L hLK)]
    (hUnramified :
      (DegreeData.AbstractExtension.mk L K.field hLK).IsUnramified D) :
    Function.Surjective
      (v.unramifiedNormQuotientValuation K L hLK hUnramified)

theorem

unramifiedNormQuotientValuation_injective

L283 ↗

ClassFormation.ValuationData.unramifiedNormQuotientValuation_injective

Documentation

The unit argument: modulo valuation, the unit-cohomology axiom makes the remaining unit an actual norm.

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 valuationQuotient

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

Lean source · statement

theorem unramifiedNormQuotientValuation_injective
    (v : ValuationData D A) (hAxiom : SatisfiesUnramifiedUnitCohomology D v)
    (K : FiniteAbstractField G) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hnormal : (extensionSubgroup K.field L hLK).Normal]
    [hfinite : Finite
      (K.field.toSubgroup ⧸ extensionSubgroup K.field L hLK)]
    (hUnramified :
      (DegreeData.AbstractExtension.mk L K.field hLK).IsUnramified D) :
    Function.Injective
      (v.unramifiedNormQuotientValuation K L hLK hUnramified)

def

unramifiedReciprocity_valuationEquiv

L374 ↗

ClassFormation.ValuationData.unramifiedReciprocity_valuationEquiv

Documentation

the unramified norm-quotient equivalence (valuation part). For finite unramified L / K, valuation induces A_K / N_{L/K}A_L ≃ ℤ/[L:K]ℤ.

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 valuationQuotient

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

Lean source · statement

def unramifiedReciprocity_valuationEquiv
    (v : ValuationData D A) (hAxiom : SatisfiesUnramifiedUnitCohomology D v)
    (K : FiniteAbstractField G) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hnormal : (extensionSubgroup K.field L hLK).Normal]
    [Finite (K.field.toSubgroup ⧸ extensionSubgroup K.field L hLK)]
    (hUnramified :
      (DegreeData.AbstractExtension.mk L K.field hLK).IsUnramified D) :
    FiniteNormQuotient A K.field L hLK ≃+
      ZMod ((FiniteAbstractFieldExtension.ofInclusion L K hLK).degree : ℕ)

theorem

primeClass_addOrderOf

L393 ↗

ClassFormation.ValuationData.primeClass_addOrderOf

Documentation

A prime class has exact additive order [L : K] in an unramified norm quotient. The lower bound is read after reduction in ℤ̂/nℤ̂; the upper bound is the norm of the included prime.

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 valuationQuotient

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

Lean source · statement

theorem primeClass_addOrderOf
    (v : ValuationData D A)
    (K : FiniteAbstractField G) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [Finite (K.field.toSubgroup ⧸ extensionSubgroup K.field L hLK)]
    (hUnramified :
      (DegreeData.AbstractExtension.mk L K.field hLK).IsUnramified D)
    (π : ambientFixedAddSubgroup A K.field) (hπ : v.IsPrimeElement K π) :
    addOrderOf
      (finiteNormClass A K.field L hLK π) =
      ((FiniteAbstractFieldExtension.ofInclusion L K hLK).degree : ℕ)

theorem

primeClass_zmultiples_eq_top

L463 ↗

ClassFormation.ValuationData.primeClass_zmultiples_eq_top

Documentation

The prime class generates the full unramified norm quotient, as in the last sentence of the proof of the unramified norm-quotient equivalence.

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 valuationQuotient

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

Lean source · statement

theorem primeClass_zmultiples_eq_top
    (v : ValuationData D A) (hAxiom : SatisfiesUnramifiedUnitCohomology D v)
    (K : FiniteAbstractField G) (L : ClosedSubgroup G)
    (hLK : L.toSubgroup ≤ K.field.toSubgroup)
    [hnormal : (extensionSubgroup K.field L hLK).Normal]
    [Finite (K.field.toSubgroup ⧸ extensionSubgroup K.field L hLK)]
    (hUnramified :
      (DegreeData.AbstractExtension.mk L K.field hLK).IsUnramified D)
    (π : ambientFixedAddSubgroup A K.field) (hπ : v.IsPrimeElement K π) :
    AddSubgroup.zmultiples
      (finiteNormClass A K.field L hLK π) = ⊤

Module documentation

The abstract reciprocity construction, the unramified norm-quotient equivalence: the

Declarations