NYLL
Module

Valuation.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Degree.Valuation
27 declarations indexed from sourceView source ↗

Module documentation

normalized degree and Frobenius theory: henselian valuations

The multiplicative coefficient module is represented additively, as in . Accordingly a valuation and a norm are additive homomorphisms. This file formalizes the valuation-quotient axiom and constructs the normalized valuations of normalized-valuation functoriality.

Imports2
Imported by5

Declarations

def

normToBase

L35 ↗
ClassFormation.normToBase
Documentation

The norm N_{K|k} on the actual fixed modules.

Source context 6 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · statement
def normToBase (A : Rep ℤ G) (K : ClosedSubgroup G)
    [Finite ((baseField G).toSubgroup ⧸
      extensionSubgroup (baseField G) K (le_baseField K))] :
    ambientFixedAddSubgroup A K →+
      ambientFixedAddSubgroup A (baseField G)
def

nsmulOnAddSubgroup

L43 ↗
ClassFormation.nsmulOnAddSubgroup
Documentation

Multiplication by n on an additive subgroup.

Source context 6 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · full declaration
def nsmulOnAddSubgroup (Z : AddSubgroup ZHat) (n : ℕ) : Z →+ Z where
  toFun z := ⟨n • z.1, Z.nsmul_mem z.2 n⟩
  map_zero' := by ext; simp
  map_add' x y := by ext; simp
def

nsmulWithin

L49 ↗
ClassFormation.nsmulWithin
Documentation

The subgroup nZ inside a value group Z.

Source context 6 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · statement
def nsmulWithin (Z : AddSubgroup ZHat) (n : ℕ) : AddSubgroup Z
def

nsmulImage

L53 ↗
ClassFormation.nsmulImage
Documentation

The ambient subgroup nZ ⊆ ℤ̂.

Source context 6 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · statement
def nsmulImage (Z : AddSubgroup ZHat) (n : ℕ) : AddSubgroup ZHat
theorem

mem_nsmulImage_iff

L62 ↗
ClassFormation.mem_nsmulImage_iff
Documentation

An element belongs to the natural-multiple image exactly when it has a preimage in the subgroup.

Source context 6 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · statement
theorem mem_nsmulImage_iff (Z : AddSubgroup ZHat) (n : ℕ) (z : ZHat) :
    z ∈ nsmulImage Z n ↔ ∃ x ∈ Z, n • x = z
theorem

nsmulImage_top

L69 ↗
ClassFormation.nsmulImage_top
Documentation

Multiples of the full value group are the range of multiplication by the same natural number on ZHat.

Source context 6 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · statement
theorem nsmulImage_top (n : ℕ) :
    nsmulImage (⊤ : AddSubgroup ZHat) n =
      (zHatMulNat n).toAddMonoidHom.range
def

valueGroupReduction

L80 ↗
ClassFormation.valueGroupReduction
Documentation

Restriction of reduction modulo n along the inclusion Z ≤ ℤ̂.

Source context 6 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · statement
def valueGroupReduction (Z : AddSubgroup ZHat) (n : ℕ) (hn : 0 < n) :
    Z →+ ZMod n
def

canonicalValueQuotientMap

L89 ↗
ClassFormation.canonicalValueQuotientMap
Documentation

The canonical map Z/nZ → ℤ/nℤ induced by the inclusion Z ≤ ℤ̂ and reduction modulo n.

This is the specific map required in the valuation-quotient axiom, rather than an arbitrarily chosen abstract equivalence between the two quotients.

Source context 6 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · statement
def canonicalValueQuotientMap (Z : AddSubgroup ZHat)
    (n : ℕ) (hn : 0 < n) : (Z ⧸ nsmulWithin Z n) →+ ZMod n
theorem

canonicalValueQuotientMap_mk

L99 ↗
ClassFormation.canonicalValueQuotientMap_mk
Documentation

The canonical value map evaluates on a quotient representative by reduction modulo n.

Source context 6 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · statement
theorem canonicalValueQuotientMap_mk (Z : AddSubgroup ZHat)
    (n : ℕ) (hn : 0 < n) (z : Z) :
    canonicalValueQuotientMap Z n hn
        (QuotientAddGroup.mk' (nsmulWithin Z n) z) =
      zHatReduction n hn (z : ZHat)
theorem

canonicalValueQuotientMap_top_bijective

L108 ↗
ClassFormation.canonicalValueQuotientMap_top_bijective
Documentation

For the full profinite-integer value group, the canonical inclusion-and-reduction quotient map is bijective.

Source context 6 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · statement
theorem canonicalValueQuotientMap_top_bijective
    (n : ℕ) (hn : 0 < n) :
    Function.Bijective
      (canonicalValueQuotientMap
        (⊤ : AddSubgroup ZHat) n hn)
theorem

normToBase_index_eq_degree

L149 ↗
ClassFormation.FiniteAbstractField.normToBase_index_eq_degree
Documentation

The quotient used by the norm has the positive degree carried by a finite abstract field.

Source context 6 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · statement
theorem FiniteAbstractField.normToBase_index_eq_degree
    {G : Type*} [Group G] [TopologicalSpace G]
    (K : FiniteAbstractField G) :
    (extensionSubgroup (baseField G) K.field
      (le_baseField K.field)).index =
      (K.toFiniteAbstractExtension.degree : ℕ)
structure

ValuationData

L161 ↗
ClassFormation.ValuationData
Documentation

the valuation-quotient axiom. A henselian valuation of A_k with respect to d.

integers_mem and canonical_value_quotient_bijective are precisely condition (i), while norm_range is condition (ii).

Source context 6 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
Lean source · full declaration
structure ValuationData (D : DegreeData G) (A : Rep ℤ G) where
  /-- The additive valuation on the distinguished base-field fixed module. -/
  toAddMonoidHom : ambientFixedAddSubgroup A (baseField G) →+ ZHat
  /-- Every integral value occurs in the image of the valuation. -/
  integers_mem : ∀ m : ℤ,
    (Int.castRingHom ZHat) m ∈
      toAddMonoidHom.range
  /-- Reduction of the value group modulo every positive integer is bijective. -/
  canonical_value_quotient_bijective : ∀ (n : ℕ) (hn : 0 < n),
    Function.Bijective
      (canonicalValueQuotientMap toAddMonoidHom.range n hn)
  /-- Norms from a finite abstract field have the prescribed value-group image. -/
  norm_range : ∀ K : FiniteAbstractField G,
    (toAddMonoidHom.comp (normToBase A K.field)).range =
      nsmulImage toAddMonoidHom.range (K.residueDegree D : ℕ)
def

valueGroup

L182 ↗
ClassFormation.ValuationData.valueGroup
Documentation

The value group Z = v(A_k).

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace ValuationData
variable {D : DegreeData G} {A : Rep ℤ G}
Lean source · statement
def valueGroup (v : ValuationData D A) : AddSubgroup ZHat
def

canonicalQuotientMap

L186 ↗
ClassFormation.ValuationData.canonicalQuotientMap
Documentation

The valuation-quotient axiom's canonical map for a henselian valuation.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace ValuationData
variable {D : DegreeData G} {A : Rep ℤ G}
Lean source · statement
def canonicalQuotientMap (v : ValuationData D A)
    (n : ℕ) (hn : 0 < n) :
    (v.valueGroup ⧸ nsmulWithin v.valueGroup n) →+ ZMod n
def

cyclic_value_quotients

L193 ↗
ClassFormation.ValuationData.cyclic_value_quotients
Documentation

The former equivalence API, now derived from the bijectivity of the canonical inclusion-and-reduction map in the valuation-quotient axiom.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace ValuationData
variable {D : DegreeData G} {A : Rep ℤ G}
Lean source · statement
def cyclic_value_quotients (v : ValuationData D A)
    (n : ℕ) (hn : 0 < n) :
    (v.valueGroup ⧸ nsmulWithin v.valueGroup n) ≃+ ZMod n
def

valueModulo

L200 ↗
ClassFormation.ValuationData.valueModulo
Documentation

Canonical reduction of the value group modulo n.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace ValuationData
variable {D : DegreeData G} {A : Rep ℤ G}
Lean source · statement
def valueModulo (v : ValuationData D A) (n : ℕ) (hn : 0 < n) :
    v.valueGroup →+ ZMod n
theorem

valueModulo_apply

L207 ↗
ClassFormation.ValuationData.valueModulo_apply
Documentation

Value modulo n is profinite-integer reduction of the underlying value.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace ValuationData
variable {D : DegreeData G} {A : Rep ℤ G}
Lean source · statement
theorem valueModulo_apply (v : ValuationData D A)
    (n : ℕ) (hn : 0 < n) (z : v.valueGroup) :
    v.valueModulo n hn z = zHatReduction n hn (z : ZHat)
theorem

valueModulo_surjective

L213 ↗
ClassFormation.ValuationData.valueModulo_surjective
Documentation

Reduction of the value group modulo a positive integer is surjective.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace ValuationData
variable {D : DegreeData G} {A : Rep ℤ G}
Lean source · statement
theorem valueModulo_surjective (v : ValuationData D A)
    (n : ℕ) (hn : 0 < n) :
    Function.Surjective (v.valueModulo n hn)
def

normCompositeAt

L223 ↗
ClassFormation.ValuationData.normCompositeAt
Documentation

The norm composite v ∘ N_{K|k} before division by the residue degree.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace ValuationData
variable {D : DegreeData G} {A : Rep ℤ G}
Lean source · statement
def normCompositeAt (v : ValuationData D A) (K : FiniteAbstractField G) :
    ambientFixedAddSubgroup A K.field →+ ZHat
theorem

normCompositeAt_range

L228 ↗
ClassFormation.ValuationData.normCompositeAt_range
Documentation

The norm-valuation composite has range equal to the residue-degree multiple image.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace ValuationData
variable {D : DegreeData G} {A : Rep ℤ G}
Lean source · statement
theorem normCompositeAt_range (v : ValuationData D A) (K : FiniteAbstractField G) :
    (v.normCompositeAt K).range =
      nsmulImage v.valueGroup (K.residueDegree D : ℕ)
def

normCompositeAtInResidueImage

L234 ↗
ClassFormation.ValuationData.normCompositeAtInResidueImage
Documentation

v(N_{K|k}a) regarded as an element of f_K ℤ̂.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace ValuationData
variable {D : DegreeData G} {A : Rep ℤ G}
Lean source · full declaration
def normCompositeAtInResidueImage (v : ValuationData D A)
    (K : FiniteAbstractField G) :
    ambientFixedAddSubgroup A K.field →+
      (zHatMulNat (K.residueDegree D : ℕ)).toAddMonoidHom.range where
  toFun a := ⟨v.normCompositeAt K a, by
    have ha : v.normCompositeAt K a ∈ (v.normCompositeAt K).range := ⟨a, rfl⟩
    rw [v.normCompositeAt_range K] at ha
    obtain ⟨z, _hz, hz⟩ := ha
    exact ⟨z, hz⟩⟩
  map_zero' := by ext; simp [normCompositeAt]
  map_add' x y := by
    apply Subtype.ext
    exact map_add (v.normCompositeAt K) x y
def

dividedAt

L249 ↗
ClassFormation.ValuationData.dividedAt
Documentation

Division by f_K before restricting the codomain back to Z.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace ValuationData
variable {D : DegreeData G} {A : Rep ℤ G}
Lean source · statement
def dividedAt (v : ValuationData D A) (K : FiniteAbstractField G) :
    ambientFixedAddSubgroup A K.field →+ ZHat
theorem

residueDegree_nsmul_dividedAt

L257 ↗
ClassFormation.ValuationData.residueDegree_nsmul_dividedAt
Documentation

The defining identity f_K v_K = v ∘ N_{K|k} before codomain restriction.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace ValuationData
variable {D : DegreeData G} {A : Rep ℤ G}
Lean source · statement
theorem residueDegree_nsmul_dividedAt (v : ValuationData D A)
    (K : FiniteAbstractField G)
    (a : ambientFixedAddSubgroup A K.field) :
    (K.residueDegree D : ℕ) • v.dividedAt K a = v.normCompositeAt K a
theorem

dividedAt_mem_valueGroup

L266 ↗
ClassFormation.ValuationData.dividedAt_mem_valueGroup
Documentation

The divided value lies in the original value group Z.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace ValuationData
variable {D : DegreeData G} {A : Rep ℤ G}
Lean source · statement
theorem dividedAt_mem_valueGroup (v : ValuationData D A)
    (K : FiniteAbstractField G)
    (a : ambientFixedAddSubgroup A K.field) :
    v.dividedAt K a ∈ v.valueGroup
def

valuationAt

L288 ↗
ClassFormation.ValuationData.valuationAt
Documentation

The normalized valuation v_K = (1/f_K) v ∘ N_{K|k}, with the exact codomain Z from the valuation-quotient axiom.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace ValuationData
variable {D : DegreeData G} {A : Rep ℤ G}
Lean source · statement
def valuationAt (v : ValuationData D A) (K : FiniteAbstractField G) :
    ambientFixedAddSubgroup A K.field →+ v.valueGroup
theorem

valuationAt_coe

L294 ↗
ClassFormation.ValuationData.valuationAt_coe
Documentation

The underlying profinite value of the positive valuation is the divided valuation.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace ValuationData
variable {D : DegreeData G} {A : Rep ℤ G}
Lean source · statement
theorem valuationAt_coe (v : ValuationData D A) (K : FiniteAbstractField G)
    (a : ambientFixedAddSubgroup A K.field) :
    (v.valuationAt K a : ZHat) = v.dividedAt K a
theorem

normalizedValuation_surjective

L301 ↗
ClassFormation.ValuationData.normalizedValuation_surjective
Documentation

normalized-valuation functoriality (surjectivity). The normalized valuation over every finite abstract field maps onto Z.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace ValuationData
variable {D : DegreeData G} {A : Rep ℤ G}
Lean source · statement
theorem normalizedValuation_surjective (v : ValuationData D A)
    (K : FiniteAbstractField G) :
    Function.Surjective (v.valuationAt K)

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