NYLL
Module

PrincipalUnits.lean

Nyll.ValuedFieldTheory.LocalField.NonarchimedeanLocalField.PrincipalUnits
21 declarations indexed from sourceView source β†—

Module documentation

Principal units

Defines the filtration U^n = 1 + 𝓂^n, proves its basic order properties, and constructs the quotient of valuation-ring units by the first filtration step.

Imports1
Imported by3

Declarations

def

principalUnits

L24 β†—
LocalFieldTheory.principalUnits
Documentation

The actual principal-unit filtration U^n = {u ∈ π’ͺ[K]Λ£ | u - 1 ∈ 𝓂[K]^n}.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
Lean source Β· full declaration
def principalUnits (K : Type u) [Field K] [ValuativeRel K] (n : Nat) :
    Subgroup π’ͺ[K]Λ£ where
  carrier := {u | ((u : π’ͺ[K]) - 1) ∈ (𝓂[K] ^ n : Ideal π’ͺ[K])}
  one_mem' := by
    simp
  mul_mem' := by
    intro a b ha hb
    change ((a : π’ͺ[K]) * (b : π’ͺ[K]) - 1) ∈ (𝓂[K] ^ n : Ideal π’ͺ[K])
    rw [show ((a : π’ͺ[K]) * (b : π’ͺ[K]) - 1) =
        ((a : π’ͺ[K]) - 1) * (b : π’ͺ[K]) + ((b : π’ͺ[K]) - 1) by
      ring]
    exact Ideal.add_mem _ (Ideal.mul_mem_right _ _ ha) hb
  inv_mem' := by
    intro a ha
    change (((a⁻¹ : π’ͺ[K]Λ£) : π’ͺ[K]) - 1) ∈ (𝓂[K] ^ n : Ideal π’ͺ[K])
    rw [show (((a⁻¹ : π’ͺ[K]Λ£) : π’ͺ[K]) - 1) =
        -(((a⁻¹ : π’ͺ[K]Λ£) : π’ͺ[K]) * ((a : π’ͺ[K]) - 1)) by
      calc
        (((a⁻¹ : π’ͺ[K]Λ£) : π’ͺ[K]) - 1)
            = ((a⁻¹ : π’ͺ[K]Λ£) : π’ͺ[K])
              - (((a⁻¹ : π’ͺ[K]Λ£) : π’ͺ[K]) * (a : π’ͺ[K])) := by
                simp
        _ = -(((a⁻¹ : π’ͺ[K]Λ£) : π’ͺ[K]) * ((a : π’ͺ[K]) - 1)) := by
          ring]
    exact (𝓂[K] ^ n : Ideal π’ͺ[K]).neg_mem (Ideal.mul_mem_left _ _ ha)
theorem

mem_principalUnits_iff

L52 β†—
LocalFieldTheory.mem_principalUnits_iff
Documentation

A valuation-ring unit lies in the n-th principal-unit group exactly when it is congruent to one modulo the n-th maximal-ideal power.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
Lean source Β· statement
theorem mem_principalUnits_iff (K : Type u) [Field K] [ValuativeRel K]
    (u : π’ͺ[K]Λ£) (n : Nat) :
    u ∈ principalUnits K n ↔ ((u : π’ͺ[K]) - 1) ∈ (𝓂[K] ^ n : Ideal π’ͺ[K])
theorem

principalUnits_integerRingEquiv_mem

L59 β†—
LocalFieldTheory.principalUnits_integerRingEquiv_mem
Documentation

An automorphism of the valuation integer ring preserves the principal-unit filtration whenever it preserves the corresponding maximal-ideal power.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
Lean source Β· statement
theorem principalUnits_integerRingEquiv_mem (K : Type u) [Field K] [ValuativeRel K]
    (n : Nat) (Οƒπ’ͺ : π’ͺ[K] ≃+* π’ͺ[K])
    (hpow : βˆ€ x : π’ͺ[K],
      x ∈ (𝓂[K] ^ n : Ideal π’ͺ[K]) β†’ Οƒπ’ͺ x ∈ (𝓂[K] ^ n : Ideal π’ͺ[K]))
    (u : π’ͺ[K]Λ£) (hu : u ∈ principalUnits K n) :
    Units.mapEquiv Οƒπ’ͺ.toMulEquiv u ∈ principalUnits K n
theorem

principalUnits_zero

L71 β†—
LocalFieldTheory.principalUnits_zero
Documentation

The zeroth principal-unit group is the full unit group of the valuation ring.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
Lean source Β· statement
theorem principalUnits_zero (K : Type u) [Field K] [ValuativeRel K] :
    principalUnits K 0 = ⊀
theorem

principalUnits_antitone

L77 β†—
LocalFieldTheory.principalUnits_antitone
Documentation

Principal-unit groups decrease as the filtration index increases.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
Lean source Β· statement
theorem principalUnits_antitone (K : Type u) [Field K] [ValuativeRel K]
    {m n : Nat} (h : m ≀ n) :
    principalUnits K n ≀ principalUnits K m
theorem

principalUnits_succ_le

L84 β†—
LocalFieldTheory.principalUnits_succ_le
Documentation

Each successor principal-unit group is contained in the preceding filtration step.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
Lean source Β· statement
theorem principalUnits_succ_le (K : Type u) [Field K] [ValuativeRel K] (n : Nat) :
    principalUnits K (n + 1) ≀ principalUnits K n
theorem

principalUnits_le_one

L89 β†—
LocalFieldTheory.principalUnits_le_one
Documentation

Every positive-index principal unit lies in the first principal-unit group.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
Lean source Β· statement
theorem principalUnits_le_one (K : Type u) [Field K] [ValuativeRel K]
    {n : Nat} (hn : 1 ≀ n) :
    principalUnits K n ≀ principalUnits K 1
def

IntegerUnitsPrincipalQuot

L95 β†—
LocalFieldTheory.IntegerUnitsPrincipalQuot
Documentation

Quotient of integer units by the actual principal-unit filtration.

Source context 4 commands

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

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

integerUnitsPrincipalQuotCommGroup

L101 β†—
LocalFieldTheory.integerUnitsPrincipalQuotCommGroup
Documentation

The quotient of valuation-ring units by an n-th principal-unit subgroup is a commutative group.

Source context 4 commands

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

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

integerUnitsPrincipalQuotConcreteEquiv

L110 β†—
LocalFieldTheory.integerUnitsPrincipalQuotConcreteEquiv
Documentation

Explicit access to the concrete quotient model. Public consumers should use the named constructor and eliminators below instead of unfolding the quotient representation.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
Lean source Β· statement
def integerUnitsPrincipalQuotConcreteEquiv
    (K : Type u) [Field K] [ValuativeRel K] (n : Nat) :
    IntegerUnitsPrincipalQuot K n ≃* (π’ͺ[K]Λ£ β§Έ principalUnits K n)
def

integerUnitsPrincipalQuotMk

L117 β†—
LocalFieldTheory.integerUnitsPrincipalQuotMk
Documentation

The quotient map π’ͺ[K]Λ£ β†’ π’ͺ[K]Λ£/U^n.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
Lean source Β· statement
def integerUnitsPrincipalQuotMk (K : Type u) [Field K] [ValuativeRel K]
    (n : Nat) : π’ͺ[K]Λ£ β†’* IntegerUnitsPrincipalQuot K n
theorem

integerUnitsPrincipalQuotConcreteEquiv_mk

L125 β†—
LocalFieldTheory.integerUnitsPrincipalQuotConcreteEquiv_mk
Documentation

The concrete quotient equivalence sends the class of a valuation-ring unit to its quotient-group class.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
Lean source Β· statement
theorem integerUnitsPrincipalQuotConcreteEquiv_mk
    (K : Type u) [Field K] [ValuativeRel K] (n : Nat) (u : π’ͺ[K]Λ£) :
    integerUnitsPrincipalQuotConcreteEquiv K n
        (integerUnitsPrincipalQuotMk K n u) =
      QuotientGroup.mk u
theorem

integerUnitsPrincipalQuotMk_surjective

L133 β†—
LocalFieldTheory.integerUnitsPrincipalQuotMk_surjective
Documentation

Every principal-unit quotient class has a valuation-ring unit representative.

Source context 4 commands

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

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

integerUnitsPrincipalQuotMk_ker

L139 β†—
LocalFieldTheory.integerUnitsPrincipalQuotMk_ker
Documentation

The kernel of the principal-unit quotient map is the n-th principal-unit subgroup.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
Lean source Β· statement
theorem integerUnitsPrincipalQuotMk_ker
    (K : Type u) [Field K] [ValuativeRel K] (n : Nat) :
    MonoidHom.ker (integerUnitsPrincipalQuotMk K n) = principalUnits K n
theorem

integerUnitsPrincipalQuotMk_eq_one_iff

L147 β†—
LocalFieldTheory.integerUnitsPrincipalQuotMk_eq_one_iff
Documentation

A unit maps to the identity quotient class exactly when it lies in the n-th principal-unit subgroup.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
Lean source Β· statement
theorem integerUnitsPrincipalQuotMk_eq_one_iff
    (K : Type u) [Field K] [ValuativeRel K] (n : Nat) (u : π’ͺ[K]Λ£) :
    integerUnitsPrincipalQuotMk K n u = 1 ↔ u ∈ principalUnits K n
theorem

integerUnitsPrincipalQuotMk_eq_iff_div_mem

L156 β†—
LocalFieldTheory.integerUnitsPrincipalQuotMk_eq_iff_div_mem
Documentation

Two units determine the same quotient class exactly when their quotient lies in the n-th principal-unit subgroup.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
Lean source Β· statement
theorem integerUnitsPrincipalQuotMk_eq_iff_div_mem
    (K : Type u) [Field K] [ValuativeRel K] (n : Nat) (u v : π’ͺ[K]Λ£) :
    integerUnitsPrincipalQuotMk K n u =
        integerUnitsPrincipalQuotMk K n v ↔
      u / v ∈ principalUnits K n
def

integerUnitsPrincipalQuotLift

L166 β†—
LocalFieldTheory.integerUnitsPrincipalQuotLift
Documentation

Descend a homomorphism that kills U^n to the named quotient.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
Lean source Β· statement
def integerUnitsPrincipalQuotLift
    {K : Type u} {M : Type*} [Field K] [ValuativeRel K] [Group M]
    (n : Nat) (f : π’ͺ[K]Λ£ β†’* M) (h : principalUnits K n ≀ f.ker) :
    IntegerUnitsPrincipalQuot K n β†’* M
theorem

integerUnitsPrincipalQuotLift_mk

L176 β†—
LocalFieldTheory.integerUnitsPrincipalQuotLift_mk
Documentation

A homomorphism lifted from the principal-unit quotient agrees with the original map on representatives.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
Lean source Β· statement
theorem integerUnitsPrincipalQuotLift_mk
    {K : Type u} {M : Type*} [Field K] [ValuativeRel K] [Group M]
    (n : Nat) (f : π’ͺ[K]Λ£ β†’* M) (h : principalUnits K n ≀ f.ker)
    (u : π’ͺ[K]Λ£) :
    integerUnitsPrincipalQuotLift n f h
        (integerUnitsPrincipalQuotMk K n u) = f u
theorem

inductionOn

L186 β†—
LocalFieldTheory.IntegerUnitsPrincipalQuot.inductionOn
Documentation

Eliminate a quotient class through the canonical class map on arbitrary representatives.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
Lean source Β· statement
theorem IntegerUnitsPrincipalQuot.inductionOn
    {K : Type u} [Field K] [ValuativeRel K] (n : Nat)
    {motive : IntegerUnitsPrincipalQuot K n β†’ Prop}
    (q : IntegerUnitsPrincipalQuot K n)
    (h : βˆ€ u : π’ͺ[K]Λ£, motive (integerUnitsPrincipalQuotMk K n u)) :
    motive q
lemma

unit_mul_sub_one_eq

L198 β†—
LocalFieldTheory.unit_mul_sub_one_eq
Documentation

Algebra identity used to prove multiplicative closure of principal units.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
Lean source Β· statement
lemma unit_mul_sub_one_eq (K : Type u) [Field K] [ValuativeRel K] (a b : π’ͺ[K]Λ£) :
    ((a * b : π’ͺ[K]Λ£) : π’ͺ[K]) - 1 =
      ((a : π’ͺ[K]) - 1) * ((b : π’ͺ[K]) - 1) +
        ((a : π’ͺ[K]) - 1) + ((b : π’ͺ[K]) - 1)
lemma

maximalIdeal_pow_antitone

L206 β†—
LocalFieldTheory.maximalIdeal_pow_antitone
Documentation

Powers of the maximal ideal decrease as their exponent increases.

Source context 4 commands

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

namespace LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
Lean source Β· statement
lemma maximalIdeal_pow_antitone (K : Type u) [Field K] [ValuativeRel K]
    {m n : Nat} (h : m ≀ n) :
    (𝓂[K] ^ n : Ideal π’ͺ[K]) ≀ (𝓂[K] ^ m : Ideal π’ͺ[K])

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