NYLL
Module

CanonicalUnramifiedNormQuotient.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.CanonicalUnramifiedNormQuotient
14 declarations indexed from sourceView source ↗

Module documentation

The abstract reciprocity construction: the canonical unramified valuation quotient

the valuation-quotient axiom supplies the order of Z / nZ. The construction then uses the canonical reduction inherited from Z ⊆ ℤ̂, rather than an arbitrary isomorphism with ℤ / nℤ. This file constructs that canonical map and proves directly that it induces the unramified norm-quotient isomorphism used in the unramified norm-quotient equivalence.

Imports2
Imported by2

Declarations

def

canonicalValueReduction

L38 ↗
ClassFormation.ValuationData.canonicalValueReduction
Documentation

Reduction modulo n restricted to the actual value subgroup Z ⊆ ℤ̂.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section

-- 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 canonicalValueReduction
    (v : ValuationData D A) (n : ℕ) (hn : 0 < n) :
    v.valueGroup →+ ZMod n
theorem

canonicalValueReduction_one

L45 ↗
ClassFormation.ValuationData.canonicalValueReduction_one
Documentation

The canonical value reduction sends the unit element to zero.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section

-- 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 canonicalValueReduction_one
    (v : ValuationData D A) (n : ℕ) (hn : 0 < n) :
    v.canonicalValueReduction n hn v.oneValue = 1
theorem

canonicalValueReduction_surjective

L52 ↗
ClassFormation.ValuationData.canonicalValueReduction_surjective
Documentation

The canonical value reduction onto the residue-degree quotient is surjective.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section

-- 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 canonicalValueReduction_surjective
    (v : ValuationData D A) (n : ℕ) (hn : 0 < n) :
    Function.Surjective (v.canonicalValueReduction n hn)
def

canonicalValueQuotientHom

L58 ↗
ClassFormation.ValuationData.canonicalValueQuotientHom
Documentation

Canonical reduction descended to Z / nZ.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section

-- 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 canonicalValueQuotientHom
    (v : ValuationData D A) (n : ℕ) (hn : 0 < n) :
    (v.valueGroup ⧸ nsmulWithin v.valueGroup n) →+ ZMod n
theorem

canonicalValueQuotientHom_mk

L65 ↗
ClassFormation.ValuationData.canonicalValueQuotientHom_mk
Documentation

The quotient homomorphism evaluates on a coset through canonical value reduction.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section

-- 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 canonicalValueQuotientHom_mk
    (v : ValuationData D A) (n : ℕ) (hn : 0 < n)
    (z : v.valueGroup) :
    v.canonicalValueQuotientHom n hn
      (QuotientAddGroup.mk' (nsmulWithin v.valueGroup n) z) =
        v.canonicalValueReduction n hn z
theorem

canonicalValueQuotientHom_surjective

L74 ↗
ClassFormation.ValuationData.canonicalValueQuotientHom_surjective
Documentation

The induced canonical value map on the quotient is surjective.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section

-- 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 canonicalValueQuotientHom_surjective
    (v : ValuationData D A) (n : ℕ) (hn : 0 < n) :
    Function.Surjective (v.canonicalValueQuotientHom n hn)
def

canonicalValueQuotientEquiv

L80 ↗
ClassFormation.ValuationData.canonicalValueQuotientEquiv
Documentation

The canonical isomorphism Z / nZ ≃ ℤ / nℤ from the valuation-quotient axiom.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section

-- 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 canonicalValueQuotientEquiv
    (v : ValuationData D A) (n : ℕ) (hn : 0 < n) :
    (v.valueGroup ⧸ nsmulWithin v.valueGroup n) ≃+ ZMod n
def

canonicalUnramifiedValuationHom

L86 ↗
ClassFormation.ValuationData.canonicalUnramifiedValuationHom
Documentation

Canonical valuation modulo [L : K] on A_K.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section

-- 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 canonicalUnramifiedValuationHom
    (v : ValuationData D A) (E : FiniteAbstractFieldExtension G) :
    ambientFixedAddSubgroup A E.base.field →+ ZMod (E.degree : ℕ)
theorem

finiteNormSubgroup_le_canonicalUnramifiedValuationHom_ker

L92 ↗
ClassFormation.ValuationData.finiteNormSubgroup_le_canonicalUnramifiedValuationHom_ker
Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section

-- 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_canonicalUnramifiedValuationHom_ker
    (v : ValuationData D A) (E : FiniteAbstractFieldExtension G)
    (hUnramified : E.IsUnramified D) :
    finiteNormSubgroup A E.base.field E.field.field E.below ≤
      (v.canonicalUnramifiedValuationHom E).ker
def

canonicalUnramifiedNormQuotientValuation

L121 ↗
ClassFormation.ValuationData.canonicalUnramifiedNormQuotientValuation
Documentation

The canonical valuation induced on the finite unramified norm quotient.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section

-- 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 canonicalUnramifiedNormQuotientValuation
    (v : ValuationData D A) (E : FiniteAbstractFieldExtension G)
    (hUnramified : E.IsUnramified D) :
    FiniteNormQuotient A E.base.field E.field.field E.below →+
      ZMod (E.degree : ℕ)
theorem

canonicalUnramifiedNormQuotientValuation_finiteNormClass

L133 ↗
ClassFormation.ValuationData.canonicalUnramifiedNormQuotientValuation_finiteNormClass
Documentation

Valuation sends a finite norm class to its canonical unramified quotient value.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section

-- 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 canonicalUnramifiedNormQuotientValuation_finiteNormClass
    (v : ValuationData D A) (E : FiniteAbstractFieldExtension G)
    (hUnramified : E.IsUnramified D)
    (a : ambientFixedAddSubgroup A E.base.field) :
    v.canonicalUnramifiedNormQuotientValuation E hUnramified
      (finiteNormClass A E.base.field E.field.field E.below a) =
        v.canonicalUnramifiedValuationHom E a
theorem

canonicalUnramifiedNormQuotientValuation_surjective

L143 ↗
ClassFormation.ValuationData.canonicalUnramifiedNormQuotientValuation_surjective
Documentation

The valuation map from the unramified norm quotient is surjective.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section

-- 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 canonicalUnramifiedNormQuotientValuation_surjective
    (v : ValuationData D A) (E : FiniteAbstractFieldExtension G)
    (hUnramified : E.IsUnramified D) :
    Function.Surjective
      (v.canonicalUnramifiedNormQuotientValuation E hUnramified)
theorem

canonicalUnramifiedNormQuotientValuation_injective

L160 ↗
ClassFormation.ValuationData.canonicalUnramifiedNormQuotientValuation_injective
Documentation

The valuation map separates classes in the unramified norm quotient.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section

-- 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 canonicalUnramifiedNormQuotientValuation_injective
    (v : ValuationData D A) (hAxiom : SatisfiesUnramifiedUnitCohomology D v)
    (E : FiniteAbstractFieldExtension G)
    (hnormal : (extensionSubgroup
      E.base.field E.field.field E.below).Normal)
    (hUnramified : E.IsUnramified D) :
    Function.Injective
      (v.canonicalUnramifiedNormQuotientValuation E hUnramified)
def

canonicalUnramifiedNormQuotientEquiv

L264 ↗
ClassFormation.ValuationData.canonicalUnramifiedNormQuotientEquiv
Documentation

Canonical form of the valuation isomorphism in the unramified norm-quotient equivalence.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section

-- 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 canonicalUnramifiedNormQuotientEquiv
    (v : ValuationData D A) (hAxiom : SatisfiesUnramifiedUnitCohomology D v)
    (E : FiniteAbstractFieldExtension G)
    (hnormal : (extensionSubgroup
      E.base.field E.field.field E.below).Normal)
    (hUnramified : E.IsUnramified D) :
    FiniteNormQuotient A E.base.field E.field.field E.below ≃+
      ZMod (E.degree : ℕ)

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