NYLL
Module

QuotientReps.lean

Nyll.GaloisCohomology.Cyclic.Herbrand.PrincipalUnits.QuotientReps
11 declarations indexed from sourceView source ↗

Module documentation

Representatives of integer units modulo principal units

This file defines the integer-unit quotient by a principal-unit subgroup and compares it with the concrete quotient used in the normal-basis calculations.

Imports1
Imported by2

Declarations

def

IntegerUnitsModPrincipalUnitsAtLevel

L31 ↗
CyclicCohomology.IntegerUnitsModPrincipalUnitsAtLevel
Documentation

Integer units modulo the n-th principal-unit subgroup.

This named type is the representation boundary: downstream code uses its quotient interface rather than unfolding the concrete quotient.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
Lean source · statement
def IntegerUnitsModPrincipalUnitsAtLevel
    (K : Type u) [Field K] [ValuativeRel K] (n : Nat) : Type u
instance

integerUnitsModPrincipalUnitsAtLevelCommGroup

L36 ↗
CyclicCohomology.integerUnitsModPrincipalUnitsAtLevelCommGroup
Documentation

Integer units modulo level principal units form a commutative group.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
Lean source · statement
instance integerUnitsModPrincipalUnitsAtLevelCommGroup
    (K : Type u) [Field K] [ValuativeRel K] (n : Nat) :
    CommGroup (IntegerUnitsModPrincipalUnitsAtLevel K n)
def

integerUnitsModPrincipalUnitsAtLevelConcreteEquiv

L43 ↗
CyclicCohomology.integerUnitsModPrincipalUnitsAtLevelConcreteEquiv
Documentation

Explicit comparison with the concrete quotient implementation.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
Lean source · statement
def integerUnitsModPrincipalUnitsAtLevelConcreteEquiv
    (K : Type u) [Field K] [ValuativeRel K] (n : Nat) :
    IntegerUnitsModPrincipalUnitsAtLevel K n ≃*
      (𝒪[K]ˣ ⧸ principalUnits K n)
def

integerUnitsModPrincipalUnitsAtLevelMk

L52 ↗
CyclicCohomology.integerUnitsModPrincipalUnitsAtLevelMk
Documentation

The canonical class of an integer unit modulo U_K^n.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
Lean source · statement
def integerUnitsModPrincipalUnitsAtLevelMk
    (K : Type u) [Field K] [ValuativeRel K] (n : Nat) :
    𝒪[K]ˣ →* IntegerUnitsModPrincipalUnitsAtLevel K n
theorem

integerUnitsModPrincipalUnitsAtLevelConcreteEquiv_mk

L60 ↗
CyclicCohomology.integerUnitsModPrincipalUnitsAtLevelConcreteEquiv_mk
Documentation

The concrete quotient equivalence sends a unit to its canonical class.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
Lean source · statement
theorem integerUnitsModPrincipalUnitsAtLevelConcreteEquiv_mk
    (K : Type u) [Field K] [ValuativeRel K] (n : Nat) (x : 𝒪[K]ˣ) :
    integerUnitsModPrincipalUnitsAtLevelConcreteEquiv K n
        (integerUnitsModPrincipalUnitsAtLevelMk K n x) =
      QuotientGroup.mk x
theorem

integerUnitsModPrincipalUnitsAtLevelMk_surjective

L68 ↗
CyclicCohomology.integerUnitsModPrincipalUnitsAtLevelMk_surjective
Documentation

Every integer-unit quotient class has a representative.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
Lean source · statement
theorem integerUnitsModPrincipalUnitsAtLevelMk_surjective
    (K : Type u) [Field K] [ValuativeRel K] (n : Nat) :
    Function.Surjective (integerUnitsModPrincipalUnitsAtLevelMk K n)
theorem

inductionOn

L75 ↗
CyclicCohomology.IntegerUnitsModPrincipalUnitsAtLevel.inductionOn
Documentation

Eliminate a level quotient through its canonical representatives.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
Lean source · statement
theorem IntegerUnitsModPrincipalUnitsAtLevel.inductionOn
    {K : Type u} [Field K] [ValuativeRel K] (n : Nat)
    {motive : IntegerUnitsModPrincipalUnitsAtLevel K n → Prop}
    (q : IntegerUnitsModPrincipalUnitsAtLevel K n)
    (h : ∀ x : 𝒪[K]ˣ,
      motive (integerUnitsModPrincipalUnitsAtLevelMk K n x)) :
    motive q
def

integerUnitsModPrincipalUnitsAtLevelLift

L88 ↗
CyclicCohomology.integerUnitsModPrincipalUnitsAtLevelLift
Documentation

Descend a homomorphism that kills U_K^n.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
Lean source · statement
def integerUnitsModPrincipalUnitsAtLevelLift
    {K : Type u} {M : Type*} [Field K] [ValuativeRel K] [Group M]
    (n : Nat) (f : 𝒪[K]ˣ →* M) (h : principalUnits K n ≤ f.ker) :
    IntegerUnitsModPrincipalUnitsAtLevel K n →* M
theorem

integerUnitsModPrincipalUnitsAtLevelLift_mk

L97 ↗
CyclicCohomology.integerUnitsModPrincipalUnitsAtLevelLift_mk
Documentation

A map lifted from the integer-unit quotient agrees on representatives.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
Lean source · statement
theorem integerUnitsModPrincipalUnitsAtLevelLift_mk
    {K : Type u} {M : Type*} [Field K] [ValuativeRel K] [Group M]
    (n : Nat) (f : 𝒪[K]ˣ →* M) (h : principalUnits K n ≤ f.ker)
    (x : 𝒪[K]ˣ) :
    integerUnitsModPrincipalUnitsAtLevelLift n f h
        (integerUnitsModPrincipalUnitsAtLevelMk K n x) = f x
theorem

integerUnitsModPrincipalUnitsAtLevelMk_eq_one_iff

L106 ↗
CyclicCohomology.integerUnitsModPrincipalUnitsAtLevelMk_eq_one_iff
Documentation

A unit represents the identity exactly when it lies in the level principal-unit subgroup.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
Lean source · statement
theorem integerUnitsModPrincipalUnitsAtLevelMk_eq_one_iff
    (K : Type u) [Field K] [ValuativeRel K] (n : Nat) (x : 𝒪[K]ˣ) :
    integerUnitsModPrincipalUnitsAtLevelMk K n x = 1 ↔
      x ∈ principalUnits K n
theorem

integerUnitsModPrincipalUnitsAtLevelMk_eq_iff_div_mem

L115 ↗
CyclicCohomology.integerUnitsModPrincipalUnitsAtLevelMk_eq_iff_div_mem
Documentation

Two units represent the same class exactly when their quotient is a level principal unit.

Source context 5 commands

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

namespace CyclicCohomology
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
Lean source · statement
theorem integerUnitsModPrincipalUnitsAtLevelMk_eq_iff_div_mem
    (K : Type u) [Field K] [ValuativeRel K] (n : Nat) (x y : 𝒪[K]ˣ) :
    integerUnitsModPrincipalUnitsAtLevelMk K n x =
        integerUnitsModPrincipalUnitsAtLevelMk K n y ↔
      x / y ∈ principalUnits K n

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