Module

Core.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PrincipalUnits.Core

69 declarations indexed from sourceView source ↗

Module documentation

Develops quotients of valuation-ring units by higher principal units and compares their first layer with residue-field units.

Successive principal-unit quotients

Imports7

Imported by8

theorem

unitsModOne_mk_eq_iff_residueUnitHom_eq

L47 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.unitsModOne_mk_eq_iff_residueUnitHom_eq

Documentation

Characterizes QuotientGroup.mk' (higherPrincipalUnitGroup F 1) u = QuotientGroup.mk' (higherPrincipalUnitGroup F 1) v by the equivalent condition higherPrincipalUnitGroup.residueUnitHom F u = higherPrincipalUnitGroup.residueUnitHom F v.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem unitsModOne_mk_eq_iff_residueUnitHom_eq
    (u v : F.valuationSubringˣ) :
    QuotientGroup.mk' (higherPrincipalUnitGroup F 1) u =
        QuotientGroup.mk' (higherPrincipalUnitGroup F 1) v ↔
      higherPrincipalUnitGroup.residueUnitHom F u =
        higherPrincipalUnitGroup.residueUnitHom F v

theorem

unitsModOne_mk_eq_iff_residue_eq

L71 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.unitsModOne_mk_eq_iff_residue_eq

Documentation

Characterizes QuotientGroup.mk' (higherPrincipalUnitGroup F 1) u = QuotientGroup.mk' (higherPrincipalUnitGroup F 1) v by the equivalent condition F.residueMap (u : F.valuationSubring) = F.residueMap (v : F.valuationSubring).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem unitsModOne_mk_eq_iff_residue_eq
    (u v : F.valuationSubringˣ) :
    QuotientGroup.mk' (higherPrincipalUnitGroup F 1) u =
        QuotientGroup.mk' (higherPrincipalUnitGroup F 1) v ↔
      F.residueMap (u : F.valuationSubring) =
        F.residueMap (v : F.valuationSubring)

def

quotientMaximalIdealPowRingEquivOfPreserves

L82 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.quotientMaximalIdealPowRingEquivOfPreserves

Documentation

A valuation-ring-preserving field automorphism induces a ring automorphism on every quotient O/m^n.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

def quotientMaximalIdealPowRingEquivOfPreserves
    (e : K ≃+* K)
    (hmem :
      ∀ x : K,
        x ∈ F.valuation.valuationSubring ↔
          e x ∈ F.valuation.valuationSubring)
    (n : ℕ) :
    F.valuationSubring ⧸ F.maximalIdeal ^ n ≃+*
      F.valuationSubring ⧸ F.maximalIdeal ^ n

theorem

quotientMaximalIdealPowRingEquivOfPreserves_mk

L111 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.quotientMaximalIdealPowRingEquivOfPreserves_mk

Documentation

Establishes the identity quotientMaximalIdealPowRingEquivOfPreserves F e hmem n (Ideal.Quotient.mk (F.maximalIdeal ^ n) x) = Ideal.Quotient.mk (F.maximalIdeal ^ n) (valuationSubringRingEquivOfPreserves F e hmem x).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem quotientMaximalIdealPowRingEquivOfPreserves_mk
    (e : K ≃+* K)
    (hmem :
      ∀ x : K,
        x ∈ F.valuation.valuationSubring ↔
          e x ∈ F.valuation.valuationSubring)
    (n : ℕ) (x : F.valuationSubring) :
    quotientMaximalIdealPowRingEquivOfPreserves F e hmem n
        (Ideal.Quotient.mk (F.maximalIdeal ^ n) x) =
      Ideal.Quotient.mk (F.maximalIdeal ^ n)
        (valuationSubringRingEquivOfPreserves F e hmem x)

def

quotientUnitHom

L139 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.quotientUnitHom

Documentation

Reduction of valuation-ring units modulo the n-th power of the maximal ideal.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

def quotientUnitHom (n : ℕ) :
    F.valuationSubringˣ →*
      (F.valuationSubring ⧸ F.maximalIdeal ^ n)ˣ

theorem

quotientUnitHom_apply

L150 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.quotientUnitHom_apply

Documentation

The defining evaluation formula for quotientUnitHom is ((higherPrincipalUnitGroup.quotientUnitHom F n u : (F.valuationSubring ⧸ F.maximalIdeal ^ n)ˣ) : F.valuationSubring ⧸ F.maximalIdeal ^ n) = Ideal.Quotient.mk (F.maximalIdeal ^ n) (u : F.valuationSubring).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem quotientUnitHom_apply (n : ℕ) (u : F.valuationSubringˣ) :
    ((higherPrincipalUnitGroup.quotientUnitHom F n u :
        (F.valuationSubring ⧸ F.maximalIdeal ^ n)ˣ) :
      F.valuationSubring ⧸ F.maximalIdeal ^ n) =
      Ideal.Quotient.mk (F.maximalIdeal ^ n) (u : F.valuationSubring)

theorem

quotientUnitHom_valuationSubringUnitEquivOfPreserves

L159 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.quotientUnitHom_valuationSubringUnitEquivOfPreserves

Documentation

Compatibility between the induced action on O^*, the induced action on O/m^n, and reduction of units modulo m^n.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem quotientUnitHom_valuationSubringUnitEquivOfPreserves
    (e : K ≃+* K)
    (hmem :
      ∀ x : K,
        x ∈ F.valuation.valuationSubring ↔
          e x ∈ F.valuation.valuationSubring)
    (n : ℕ) (u : F.valuationSubringˣ) :
    Units.map
        (quotientMaximalIdealPowRingEquivOfPreserves F e hmem n).toMonoidHom
        (higherPrincipalUnitGroup.quotientUnitHom F n u) =
      higherPrincipalUnitGroup.quotientUnitHom F n
        (valuationSubringUnitEquivOfPreserves F e hmem u)

theorem

quotientUnitHom_ker_eq

L177 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.quotientUnitHom_ker_eq

Documentation

The kernel of unit reduction modulo m^n is exactly the concrete principal-unit subgroup U^n.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem quotientUnitHom_ker_eq (n : ℕ) :
    (higherPrincipalUnitGroup.quotientUnitHom F n).ker =
      higherPrincipalUnitGroup F n

def

unitsModHigherPrincipalUnitGroupEquivRange

L211 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.unitsModHigherPrincipalUnitGroupEquivRange

Documentation

First-isomorphism form of unit reduction modulo m^n: O^*/U^n is the range of the unit group of O/m^n.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

def unitsModHigherPrincipalUnitGroupEquivRange (n : ℕ) :
    F.valuationSubringˣ ⧸ higherPrincipalUnitGroup F n ≃*
      (higherPrincipalUnitGroup.quotientUnitHom F n).range

theorem

quotientUnitHom_surjective_of_pos

L221 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.quotientUnitHom_surjective_of_pos

Documentation

For n ≥ 1, every unit modulo m^n is the reduction of a valuation-ring unit.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem quotientUnitHom_surjective_of_pos {n : ℕ} (hn : 1 ≤ n) :
    Function.Surjective (higherPrincipalUnitGroup.quotientUnitHom F n)

def

unitsModHigherPrincipalUnitGroupEquivQuotientUnits

L271 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.unitsModHigherPrincipalUnitGroupEquivQuotientUnits

Documentation

The unit-quotient coordinate theorem, first unit-quotient form: O^*/U^n ≃ (O/m^n)^* for n ≥ 1.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

def unitsModHigherPrincipalUnitGroupEquivQuotientUnits
    (n : ℕ) (hn : 1 ≤ n) :
    F.valuationSubringˣ ⧸ higherPrincipalUnitGroup F n ≃*
      (F.valuationSubring ⧸ F.maximalIdeal ^ n)ˣ

theorem

maximalIdeal_fg

L283 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.maximalIdeal_fg

Documentation

The maximal ideal of a complete DVF valuation ring is finitely generated: it is generated by any uniformizer.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem maximalIdeal_fg :
    F.maximalIdeal.FG

theorem

finite_quotient_maximalIdeal_pow_of_finite_residue

L291 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.finite_quotient_maximalIdeal_pow_of_finite_residue

Documentation

If the residue field is finite, then every quotient by a power of the maximal ideal is finite.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem finite_quotient_maximalIdeal_pow_of_finite_residue
    [Finite F.residueField] (n : ℕ) :
    Finite (F.valuationSubring ⧸ F.maximalIdeal ^ n)

theorem

finite_unitsModHigherPrincipalUnitGroup_of_finite_residue

L301 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.finite_unitsModHigherPrincipalUnitGroup_of_finite_residue

Documentation

Finite-residue complete DVFs have finite unit quotients O^*/U^n.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem finite_unitsModHigherPrincipalUnitGroup_of_finite_residue
    [Finite F.residueField] (n : ℕ) :
    Finite (F.valuationSubringˣ ⧸ higherPrincipalUnitGroup F n)

instance

quotientMaximalIdealPowFinite

L313 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.quotientMaximalIdealPowFinite

Documentation

The type in Finite (F.valuationSubring ⧸ F.maximalIdeal ^ n) is finite.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

instance quotientMaximalIdealPowFinite
    [Finite F.residueField] (n : ℕ) :
    Finite (F.valuationSubring ⧸ F.maximalIdeal ^ n)

instance

unitsModHigherPrincipalUnitGroupFinite

L319 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.unitsModHigherPrincipalUnitGroupFinite

Documentation

The type in Finite (F.valuationSubringˣ ⧸ higherPrincipalUnitGroup F n) is finite.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

instance unitsModHigherPrincipalUnitGroupFinite
    [Finite F.residueField] (n : ℕ) :
    Finite (F.valuationSubringˣ ⧸ higherPrincipalUnitGroup F n)

theorem

card_unitsModHigherPrincipalUnitGroup_eq_quotientUnits

L328 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.card_unitsModHigherPrincipalUnitGroup_eq_quotientUnits

Documentation

Cardinality form of O^*/U^n ≃ (O/m^n)^* for n ≥ 1 over a finite residue field. The finite instances are derived from the residue field before either natural cardinal is formed.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem card_unitsModHigherPrincipalUnitGroup_eq_quotientUnits
    [Finite F.residueField] (n : ℕ) (hn : 1 ≤ n) :
    Nat.card (F.valuationSubringˣ ⧸ higherPrincipalUnitGroup F n) =
      Nat.card ((F.valuationSubring ⧸ F.maximalIdeal ^ n)ˣ)

theorem

finite_principalUnitSubquotient_of_finite_residue

L339 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.finite_principalUnitSubquotient_of_finite_residue

Documentation

Every concrete principal-unit subquotient is finite when the residue field is finite. It is identified with the range of the inclusion into the finite full unit quotient.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem finite_principalUnitSubquotient_of_finite_residue
    [Finite F.residueField] (m n : ℕ) :
    Finite (higherPrincipalUnitGroup F m ⧸
      (higherPrincipalUnitGroup F n).subgroupOf
        (higherPrincipalUnitGroup F m))

instance

principalUnitSubquotientFinite

L374 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSubquotientFinite

Documentation

The type in Finite (higherPrincipalUnitGroup F m ⧸ (higherPrincipalUnitGroup F n).subgroupOf (higherPrincipalUnitGroup F m)) is finite.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

instance principalUnitSubquotientFinite
    [Finite F.residueField] (m n : ℕ) :
    Finite (higherPrincipalUnitGroup F m ⧸
      (higherPrincipalUnitGroup F n).subgroupOf
        (higherPrincipalUnitGroup F m))

def

toPrincipalUnitFiltration

L383 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.toPrincipalUnitFiltration

Documentation

The concrete principal-unit filtration as the abstract filtration API.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · full declaration

def toPrincipalUnitFiltration :
    AntitoneSubgroupFiltration F.valuationSubringˣ where
  subgroup := higherPrincipalUnitGroup F
  antitone := fun h => higherPrincipalUnitGroup.antitone F h

theorem

toPrincipalUnitFiltration_subgroup

L392 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.toPrincipalUnitFiltration_subgroup

Documentation

Establishes the identity (higherPrincipalUnitGroup.toPrincipalUnitFiltration F).subgroup n = higherPrincipalUnitGroup F n.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem toPrincipalUnitFiltration_subgroup (n : ℕ) :
    (higherPrincipalUnitGroup.toPrincipalUnitFiltration F).subgroup n =
      higherPrincipalUnitGroup F n

instance

toPrincipalUnitFiltrationPrincipalUnitSubquotientFinite

L401 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.toPrincipalUnitFiltrationPrincipalUnitSubquotientFinite

Documentation

The type in Finite ((higherPrincipalUnitGroup.toPrincipalUnitFiltration F).principalUnitSubquotient m n) is finite.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

instance toPrincipalUnitFiltrationPrincipalUnitSubquotientFinite
    [Finite F.residueField] (m n : ℕ) :
    Finite
      ((higherPrincipalUnitGroup.toPrincipalUnitFiltration F).principalUnitSubquotient
        m n)

def

principalUnitSuccQuot

L417 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuot

Documentation

The adjacent quotient U^n/U^(n+1) for the concrete complete-DVF principal-unit filtration.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

def principalUnitSuccQuot (n : ℕ) : Type u

instance

principalUnitSuccQuotCommGroup

L425 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotCommGroup

Documentation

Equips the target with its canonical CommGroup structure, namely CommGroup (higherPrincipalUnitGroup.principalUnitSuccQuot F n).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

instance principalUnitSuccQuotCommGroup (n : ℕ) :
    CommGroup (higherPrincipalUnitGroup.principalUnitSuccQuot F n)

def

principalUnitSuccQuotConcreteEquiv

L435 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotConcreteEquiv

Documentation

Explicit access to the concrete quotient used to implement principalUnitSuccQuot.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

def principalUnitSuccQuotConcreteEquiv (n : ℕ) :
    higherPrincipalUnitGroup.principalUnitSuccQuot F n ≃*
      (higherPrincipalUnitGroup F n ⧸
        (higherPrincipalUnitGroup F (n + 1)).subgroupOf
          (higherPrincipalUnitGroup F n))

def

principalUnitSuccQuotMk

L450 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotMk

Documentation

The quotient map U^n → U^n/U^(n+1).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

def principalUnitSuccQuotMk (n : ℕ) :
    higherPrincipalUnitGroup F n →*
      higherPrincipalUnitGroup.principalUnitSuccQuot F n

theorem

principalUnitSuccQuotConcreteEquiv_mk

L464 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotConcreteEquiv_mk

Documentation

Establishes the identity higherPrincipalUnitGroup.principalUnitSuccQuotConcreteEquiv F n (higherPrincipalUnitGroup.principalUnitSuccQuotMk F n u) = QuotientGroup.mk u.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem principalUnitSuccQuotConcreteEquiv_mk (n : ℕ)
    (u : higherPrincipalUnitGroup F n) :
    higherPrincipalUnitGroup.principalUnitSuccQuotConcreteEquiv F n
        (higherPrincipalUnitGroup.principalUnitSuccQuotMk F n u) =
      QuotientGroup.mk u

theorem

principalUnitSuccQuotMk_surjective

L475 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotMk_surjective

Documentation

The specified map is surjective: Function.Surjective (higherPrincipalUnitGroup.principalUnitSuccQuotMk F n).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem principalUnitSuccQuotMk_surjective (n : ℕ) :
    Function.Surjective (higherPrincipalUnitGroup.principalUnitSuccQuotMk F n)

theorem

inductionOn

L482 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuot.inductionOn

Documentation

Eliminate an adjacent principal-unit quotient through its canonical representatives.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem principalUnitSuccQuot.inductionOn
    (n : ℕ)
    {motive : higherPrincipalUnitGroup.principalUnitSuccQuot F n → Prop}
    (q : higherPrincipalUnitGroup.principalUnitSuccQuot F n)
    (h : ∀ u : higherPrincipalUnitGroup F n,
      motive (higherPrincipalUnitGroup.principalUnitSuccQuotMk F n u)) :
    motive q

def

principalUnitSuccQuotLift

L499 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotLift

Documentation

Descend a homomorphism from U^n that kills U^(n+1).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

def principalUnitSuccQuotLift
    {H : Type*} [Group H] (n : ℕ)
    (f : higherPrincipalUnitGroup F n →* H)
    (h : (higherPrincipalUnitGroup F (n + 1)).subgroupOf
      (higherPrincipalUnitGroup F n) ≤ f.ker) :
    higherPrincipalUnitGroup.principalUnitSuccQuot F n →* H

theorem

principalUnitSuccQuotLift_mk

L517 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotLift_mk

Documentation

Establishes the identity higherPrincipalUnitGroup.principalUnitSuccQuotLift F n f h (higherPrincipalUnitGroup.principalUnitSuccQuotMk F n u) = f u.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem principalUnitSuccQuotLift_mk
    {H : Type*} [Group H] (n : ℕ)
    (f : higherPrincipalUnitGroup F n →* H)
    (h : (higherPrincipalUnitGroup F (n + 1)).subgroupOf
      (higherPrincipalUnitGroup F n) ≤ f.ker)
    (u : higherPrincipalUnitGroup F n) :
    higherPrincipalUnitGroup.principalUnitSuccQuotLift F n f h
        (higherPrincipalUnitGroup.principalUnitSuccQuotMk F n u) = f u

instance

principalUnitSuccQuotFinite

L528 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotFinite

Documentation

The type in Finite (higherPrincipalUnitGroup.principalUnitSuccQuot F n) is finite.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

instance principalUnitSuccQuotFinite
    [Finite F.residueField] (n : ℕ) :
    Finite (higherPrincipalUnitGroup.principalUnitSuccQuot F n)

def

principalUnitSuccQuotEquivGradedPiece

L539 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotEquivGradedPiece

Documentation

The concrete complete-DVF adjacent quotient agrees with the generic graded-piece wrapper through explicit public equivalences.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

def principalUnitSuccQuotEquivGradedPiece (n : ℕ) :
    higherPrincipalUnitGroup.principalUnitSuccQuot F n ≃*
      (higherPrincipalUnitGroup.toPrincipalUnitFiltration F).principalUnitGradedPiece n

theorem

principalUnitSuccQuotEquivGradedPiece_mk

L553 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotEquivGradedPiece_mk

Documentation

Establishes the identity higherPrincipalUnitGroup.principalUnitSuccQuotEquivGradedPiece F n (higherPrincipalUnitGroup.principalUnitSuccQuotMk F n u) = (higherPrincipalUnitGroup.toPrincipalUnitFiltration F).principalUnitGradedPieceMk n u.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem principalUnitSuccQuotEquivGradedPiece_mk
    (n : ℕ) (u : higherPrincipalUnitGroup F n) :
    higherPrincipalUnitGroup.principalUnitSuccQuotEquivGradedPiece F n
        (higherPrincipalUnitGroup.principalUnitSuccQuotMk F n u) =
      (higherPrincipalUnitGroup.toPrincipalUnitFiltration F).principalUnitGradedPieceMk
        n u

theorem

principalUnitSuccQuotMk_eq_one_iff

L565 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotMk_eq_one_iff

Documentation

Characterizes higherPrincipalUnitGroup.principalUnitSuccQuotMk F n u = 1 by the equivalent condition u ∈ (higherPrincipalUnitGroup F (n + 1)).subgroupOf (higherPrincipalUnitGroup F n).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem principalUnitSuccQuotMk_eq_one_iff (n : ℕ)
    (u : higherPrincipalUnitGroup F n) :
    higherPrincipalUnitGroup.principalUnitSuccQuotMk F n u = 1 ↔
      u ∈ (higherPrincipalUnitGroup F (n + 1)).subgroupOf
        (higherPrincipalUnitGroup F n)

theorem

principalUnitSuccQuotMk_eq_iff_div_mem

L581 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotMk_eq_iff_div_mem

Documentation

Characterizes higherPrincipalUnitGroup.principalUnitSuccQuotMk F n u = higherPrincipalUnitGroup.principalUnitSuccQuotMk F n v by the equivalent condition u / v ∈ (higherPrincipalUnitGroup F (n + 1)).subgroupOf (higherPrincipalUnitGroup F n).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem principalUnitSuccQuotMk_eq_iff_div_mem (n : ℕ)
    (u v : higherPrincipalUnitGroup F n) :
    higherPrincipalUnitGroup.principalUnitSuccQuotMk F n u =
        higherPrincipalUnitGroup.principalUnitSuccQuotMk F n v ↔
      u / v ∈ (higherPrincipalUnitGroup F (n + 1)).subgroupOf
        (higherPrincipalUnitGroup F n)

theorem

mem_succ_subgroupOf_iff

L601 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.mem_succ_subgroupOf_iff

Documentation

Characterizes u ∈ (higherPrincipalUnitGroup F (n + 1)).subgroupOf (higherPrincipalUnitGroup F n) by the equivalent condition ((u : F.valuationSubringˣ) : F.valuationSubring) - 1 ∈ F.maximalIdeal ^ (n + 1).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem mem_succ_subgroupOf_iff (n : ℕ)
    (u : higherPrincipalUnitGroup F n) :
    u ∈ (higherPrincipalUnitGroup F (n + 1)).subgroupOf
        (higherPrincipalUnitGroup F n) ↔
      ((u : F.valuationSubringˣ) : F.valuationSubring) - 1 ∈
        F.maximalIdeal ^ (n + 1)

theorem

isUnit_one_add_of_mem_maximalIdeal_pow

L610 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.isUnit_one_add_of_mem_maximalIdeal_pow

Documentation

If a ∈ m^n with n ≥ 1, then 1 + a is a unit of the valuation ring.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem isUnit_one_add_of_mem_maximalIdeal_pow {n : ℕ} (hn : 1 ≤ n)
    (a : F.valuationSubring) (ha : a ∈ F.maximalIdeal ^ n) : IsUnit (1 + a)

def

principalUnitOneAddOfMemPow

L624 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitOneAddOfMemPow

Documentation

The unit 1 + a attached to an element a ∈ m^n, for n ≥ 1.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

def principalUnitOneAddOfMemPow {n : ℕ} (hn : 1 ≤ n)
    (a : F.valuationSubring) (ha : a ∈ F.maximalIdeal ^ n) : F.valuationSubringˣ

theorem

principalUnitOneAddOfMemPow_val

L632 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitOneAddOfMemPow_val

Documentation

Establishes the identity ((higherPrincipalUnitGroup.principalUnitOneAddOfMemPow F hn a ha : F.valuationSubringˣ) : F.valuationSubring) = 1 + a.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem principalUnitOneAddOfMemPow_val {n : ℕ} (hn : 1 ≤ n)
    (a : F.valuationSubring) (ha : a ∈ F.maximalIdeal ^ n) :
    ((higherPrincipalUnitGroup.principalUnitOneAddOfMemPow F hn a ha :
        F.valuationSubringˣ) : F.valuationSubring) =
      1 + a

def

principalUnitOneAddOfMemPowSubgroup

L641 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitOneAddOfMemPowSubgroup

Documentation

The unit 1 + a, viewed as an element of U^n.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

def principalUnitOneAddOfMemPowSubgroup {n : ℕ} (hn : 1 ≤ n)
    (a : F.valuationSubring) (ha : a ∈ F.maximalIdeal ^ n) :
    higherPrincipalUnitGroup F n

theorem

principalUnitOneAddOfMemPowSubgroup_val

L654 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitOneAddOfMemPowSubgroup_val

Documentation

Establishes the identity ((higherPrincipalUnitGroup.principalUnitOneAddOfMemPowSubgroup F hn a ha : higherPrincipalUnitGroup F n) : F.valuationSubringˣ) = higherPrincipalUnitGroup.principalUnitOneAddOfMemPow F hn a ha.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem principalUnitOneAddOfMemPowSubgroup_val {n : ℕ} (hn : 1 ≤ n)
    (a : F.valuationSubring) (ha : a ∈ F.maximalIdeal ^ n) :
    ((higherPrincipalUnitGroup.principalUnitOneAddOfMemPowSubgroup F hn a ha :
        higherPrincipalUnitGroup F n) : F.valuationSubringˣ) =
      higherPrincipalUnitGroup.principalUnitOneAddOfMemPow F hn a ha

def

principalUnitSuccQuotOfIdealPow

L663 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotOfIdealPow

Documentation

The concrete map m^n → U^n/U^(n+1) sending a to the class of 1 + a.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

def principalUnitSuccQuotOfIdealPow (n : ℕ) (hn : 1 ≤ n) :
    ((F.maximalIdeal ^ n : Ideal F.valuationSubring) : Type u) →
      higherPrincipalUnitGroup.principalUnitSuccQuot F n

theorem

principalUnitSuccQuotOfIdealPow_apply

L676 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotOfIdealPow_apply

Documentation

The defining evaluation formula for principalUnitSuccQuotOfIdealPow is higherPrincipalUnitGroup.principalUnitSuccQuotOfIdealPow F n hn a = higherPrincipalUnitGroup.principalUnitSuccQuotMk F n (higherPrincipalUnitGroup.principalUnitOneAddOfMemPowSubgroup F hn a.1 a.2).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem principalUnitSuccQuotOfIdealPow_apply (n : ℕ) (hn : 1 ≤ n)
    (a : ((F.maximalIdeal ^ n : Ideal F.valuationSubring) : Type u)) :
    higherPrincipalUnitGroup.principalUnitSuccQuotOfIdealPow F n hn a =
      higherPrincipalUnitGroup.principalUnitSuccQuotMk F n
        (higherPrincipalUnitGroup.principalUnitOneAddOfMemPowSubgroup F hn a.1 a.2)

theorem

principalUnitSuccQuotOfIdealPow_eq_one_of_mem_succ

L684 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotOfIdealPow_eq_one_of_mem_succ

Documentation

Elements of m^(n+1) map to the trivial class in U^n/U^(n+1).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem principalUnitSuccQuotOfIdealPow_eq_one_of_mem_succ
    (n : ℕ) (hn : 1 ≤ n)
    (a : ((F.maximalIdeal ^ n : Ideal F.valuationSubring) : Type u))
    (ha : (a : F.valuationSubring) ∈ F.maximalIdeal ^ (n + 1)) :
    higherPrincipalUnitGroup.principalUnitSuccQuotOfIdealPow F n hn a = 1

theorem

principalUnitSuccQuotOfIdealPow_eq_of_sub_mem_succ

L695 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotOfIdealPow_eq_of_sub_mem_succ

Documentation

The map a ↦ [1 + a] is insensitive to changing a modulo m^(n+1).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem principalUnitSuccQuotOfIdealPow_eq_of_sub_mem_succ
    (n : ℕ) (hn : 1 ≤ n)
    (a b : ((F.maximalIdeal ^ n : Ideal F.valuationSubring) : Type u))
    (hab : ((a : F.valuationSubring) - (b : F.valuationSubring)) ∈
      F.maximalIdeal ^ (n + 1)) :
    higherPrincipalUnitGroup.principalUnitSuccQuotOfIdealPow F n hn a =
      higherPrincipalUnitGroup.principalUnitSuccQuotOfIdealPow F n hn b

theorem

principalUnitSuccQuotOfIdealPow_eq_one_iff

L754 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotOfIdealPow_eq_one_iff

Documentation

The class [1+a] is trivial exactly when a ∈ m^(n+1).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem principalUnitSuccQuotOfIdealPow_eq_one_iff
    (n : ℕ) (hn : 1 ≤ n)
    (a : ((F.maximalIdeal ^ n : Ideal F.valuationSubring) : Type u)) :
    higherPrincipalUnitGroup.principalUnitSuccQuotOfIdealPow F n hn a = 1 ↔
      (a : F.valuationSubring) ∈ F.maximalIdeal ^ (n + 1)

theorem

maximalIdealPow_mul_mem_succ

L772 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.maximalIdealPow_mul_mem_succ

Documentation

Products of two elements of m^n, for n ≥ 1, lie in m^(n+1).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem maximalIdealPow_mul_mem_succ {n : ℕ} (hn : 1 ≤ n)
    (a b : ((F.maximalIdeal ^ n : Ideal F.valuationSubring) : Type u)) :
    ((a : F.valuationSubring) * (b : F.valuationSubring)) ∈
      F.maximalIdeal ^ (n + 1)

theorem

principalUnitSuccQuotOfIdealPow_add

L786 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotOfIdealPow_add

Documentation

The map a ↦ [1+a] is additive after passing to the successive principal-unit quotient.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem principalUnitSuccQuotOfIdealPow_add
    (n : ℕ) (hn : 1 ≤ n)
    (a b : ((F.maximalIdeal ^ n : Ideal F.valuationSubring) : Type u)) :
    higherPrincipalUnitGroup.principalUnitSuccQuotOfIdealPow F n hn (a + b) =
      higherPrincipalUnitGroup.principalUnitSuccQuotOfIdealPow F n hn a *
        higherPrincipalUnitGroup.principalUnitSuccQuotOfIdealPow F n hn b

def

principalUnitSuccQuotOfMaximalIdealPowSuccQuot

L872 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuot

Documentation

The descent of a ↦ [1+a] to m^n/m^(n+1).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

def principalUnitSuccQuotOfMaximalIdealPowSuccQuot
    (n : ℕ) (hn : 1 ≤ n) :
    MaximalIdealPowSuccQuot F.toDVF n →
      higherPrincipalUnitGroup.principalUnitSuccQuot F n

theorem

principalUnitSuccQuotOfMaximalIdealPowSuccQuot_mk

L888 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuot_mk

Documentation

Establishes the identity higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuot F n hn (maximalIdealPowSuccQuotMk F.toDVF n a) = higherPrincipalUnitGroup.principalUnitSuccQuotOfIdealPow F n hn a.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem principalUnitSuccQuotOfMaximalIdealPowSuccQuot_mk
    (n : ℕ) (hn : 1 ≤ n)
    (a : ((F.maximalIdeal ^ n : Ideal F.valuationSubring) : Type u)) :
    higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuot F n hn
        (maximalIdealPowSuccQuotMk F.toDVF n a) =
      higherPrincipalUnitGroup.principalUnitSuccQuotOfIdealPow F n hn a

theorem

principalUnitSuccQuotOfMaximalIdealPowSuccQuot_map_zero

L900 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuot_map_zero

Documentation

principalUnitSuccQuotOfMaximalIdealPowSuccQuot has the zero-value formula higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuot F n hn 0 = 1.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem principalUnitSuccQuotOfMaximalIdealPowSuccQuot_map_zero
    (n : ℕ) (hn : 1 ≤ n) :
    higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuot F n hn 0 = 1

theorem

principalUnitSuccQuotOfMaximalIdealPowSuccQuot_map_add

L918 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuot_map_add

Documentation

principalUnitSuccQuotOfMaximalIdealPowSuccQuot satisfies the addition formula higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuot F n hn (x + y) = higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuot F n hn x * higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuot F n hn y.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem principalUnitSuccQuotOfMaximalIdealPowSuccQuot_map_add
    (n : ℕ) (hn : 1 ≤ n)
    (x y : MaximalIdealPowSuccQuot F.toDVF n) :
    higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuot F n hn (x + y) =
      higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuot F n hn x *
        higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuot F n hn y

def

principalUnitSuccQuotOfMaximalIdealPowSuccQuotAdd

L975 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuotAdd

Documentation

Additive form of the descended map m^n/m^(n+1) → U^n/U^(n+1).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · full declaration

def principalUnitSuccQuotOfMaximalIdealPowSuccQuotAdd
    (n : ℕ) (hn : 1 ≤ n) :
    MaximalIdealPowSuccQuot F.toDVF n →+
      Additive (higherPrincipalUnitGroup.principalUnitSuccQuot F n) where
  toFun x := Additive.ofMul
    (higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuot F n hn x)
  map_zero' := by
    change Additive.ofMul
        (higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuot F n hn 0) = 0
    simp
  map_add' x y := by
    change Additive.ofMul
        (higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuot F n hn (x + y)) =
      Additive.ofMul
        (higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuot F n hn x *
          higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuot F n hn y)
    rw [higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuot_map_add]

theorem

principalUnitSuccQuotOfMaximalIdealPowSuccQuotAdd_apply

L999 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuotAdd_apply

Documentation

The defining evaluation formula for principalUnitSuccQuotOfMaximalIdealPowSuccQuotAdd is higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuotAdd F n hn x = Additive.ofMul (higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuot F n hn x).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem principalUnitSuccQuotOfMaximalIdealPowSuccQuotAdd_apply
    (n : ℕ) (hn : 1 ≤ n) (x : MaximalIdealPowSuccQuot F.toDVF n) :
    higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuotAdd F n hn x =
      Additive.ofMul
        (higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuot F n hn x)

theorem

principalUnitSuccQuotOfMaximalIdealPowSuccQuot_eq_one_iff

L1010 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuot_eq_one_iff

Documentation

Characterizes higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuot F n hn x = 1 by the equivalent condition x = 0.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem principalUnitSuccQuotOfMaximalIdealPowSuccQuot_eq_one_iff
    (n : ℕ) (hn : 1 ≤ n) (x : MaximalIdealPowSuccQuot F.toDVF n) :
    higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuot F n hn x = 1 ↔
      x = 0

theorem

principalUnitSuccQuotOfMaximalIdealPowSuccQuot_surjective

L1035 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuot_surjective

Documentation

The specified map is surjective: Function.Surjective (higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuot F n hn).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem principalUnitSuccQuotOfMaximalIdealPowSuccQuot_surjective
    (n : ℕ) (hn : 1 ≤ n) :
    Function.Surjective
      (higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuot F n hn)

theorem

principalUnitSuccQuotOfMaximalIdealPowSuccQuotAdd_surjective

L1062 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuotAdd_surjective

Documentation

The specified map is surjective: Function.Surjective (higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuotAdd F n hn).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem principalUnitSuccQuotOfMaximalIdealPowSuccQuotAdd_surjective
    (n : ℕ) (hn : 1 ≤ n) :
    Function.Surjective
      (higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuotAdd F n hn)

theorem

principalUnitSuccQuotOfMaximalIdealPowSuccQuotAdd_injective

L1079 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuotAdd_injective

Documentation

The specified map is injective: Function.Injective (higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuotAdd F n hn).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem principalUnitSuccQuotOfMaximalIdealPowSuccQuotAdd_injective
    (n : ℕ) (hn : 1 ≤ n) :
    Function.Injective
      (higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuotAdd F n hn)

def

maximalIdealPowSuccQuotAddEquivPrincipalUnitSuccQuot

L1106 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.maximalIdealPowSuccQuotAddEquivPrincipalUnitSuccQuot

Documentation

The additive isomorphism m^n/m^(n+1) ≃ U^n/U^(n+1) induced by a ↦ 1+a.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

def maximalIdealPowSuccQuotAddEquivPrincipalUnitSuccQuot
    (n : ℕ) (hn : 1 ≤ n) :
    MaximalIdealPowSuccQuot F.toDVF n ≃+
      Additive (higherPrincipalUnitGroup.principalUnitSuccQuot F n)

theorem

maximalIdealPowSuccQuotAddEquivPrincipalUnitSuccQuot_apply

L1122 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.maximalIdealPowSuccQuotAddEquivPrincipalUnitSuccQuot_apply

Documentation

The defining evaluation formula for maximalIdealPowSuccQuotAddEquivPrincipalUnitSuccQuot is higherPrincipalUnitGroup.maximalIdealPowSuccQuotAddEquivPrincipalUnitSuccQuot F n hn x = higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuotAdd F n hn x.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem maximalIdealPowSuccQuotAddEquivPrincipalUnitSuccQuot_apply
    (n : ℕ) (hn : 1 ≤ n) (x : MaximalIdealPowSuccQuot F.toDVF n) :
    higherPrincipalUnitGroup.maximalIdealPowSuccQuotAddEquivPrincipalUnitSuccQuot
        F n hn x =
      higherPrincipalUnitGroup.principalUnitSuccQuotOfMaximalIdealPowSuccQuotAdd F n hn x

def

principalUnitSuccQuotAddEquivResidueOfUniformizer

L1131 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotAddEquivResidueOfUniformizer

Documentation

The unit-quotient coordinate theorem for a complete DVF with a specified uniformizer: U^n/U^(n+1) is additively the residue field.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

def principalUnitSuccQuotAddEquivResidueOfUniformizer
    {pi : F.valuationSubring} (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n) :
    Additive (higherPrincipalUnitGroup.principalUnitSuccQuot F n) ≃+ F.residueField

theorem

card_principalUnitSuccQuot_eq_residue_of_uniformizer

L1141 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.card_principalUnitSuccQuot_eq_residue_of_uniformizer

Documentation

Cardinality form of the associated-graded identification U^n/U^(n+1) ≃ k for n ≥ 1.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem card_principalUnitSuccQuot_eq_residue_of_uniformizer
    [Finite F.residueField]
    {pi : F.valuationSubring} (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n) :
    Nat.card (higherPrincipalUnitGroup.principalUnitSuccQuot F n) =
      Nat.card F.residueField

theorem

card_principalUnitSubquotient_one_eq_residue_pow_of_uniformizer

L1162 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.card_principalUnitSubquotient_one_eq_residue_pow_of_uniformizer

Documentation

Cardinality of the finite principal-unit range U^1/U^n, obtained by iterating the adjacent quotients U^i/U^(i+1) ≃ k.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem card_principalUnitSubquotient_one_eq_residue_pow_of_uniformizer
    [Finite F.residueField]
    {pi : F.valuationSubring} (hpi : F.valuation.IsUniformizer (pi : K))
    {n : ℕ} (hn : 1 ≤ n) :
    Nat.card (higherPrincipalUnitGroup F 1 ⧸
        (higherPrincipalUnitGroup F n).subgroupOf
          (higherPrincipalUnitGroup F 1)) =
      Nat.card F.residueField ^ (n - 1)

theorem

principalUnitSuccQuotAddEquivResidueOfUniformizer_symm_residue

L1211 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotAddEquivResidueOfUniformizer_symm_residue

Documentation

Under the inverse of U^n/U^(n+1) ≃ k, the residue of r is represented by the principal unit 1 + r * pi^n.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem principalUnitSuccQuotAddEquivResidueOfUniformizer_symm_residue
    {pi : F.valuationSubring} (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n) (r : F.valuationSubring) :
    (higherPrincipalUnitGroup.principalUnitSuccQuotAddEquivResidueOfUniformizer
        F hpi n hn).symm (F.residueMap r) =
      Additive.ofMul
        (higherPrincipalUnitGroup.principalUnitSuccQuotOfIdealPow F n hn
          (maximalIdealPowMulUniformizerPowMap F.toDVF hpi n r))

theorem

principalUnitSuccQuotAddEquivResidueOfUniformizer_coord

L1236 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitSuccQuotAddEquivResidueOfUniformizer_coord

Documentation

The equivalence U^n/U^(n+1) ≃ k sends the coordinate class [1 + r * pi^n] to the residue of r.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem principalUnitSuccQuotAddEquivResidueOfUniformizer_coord
    {pi : F.valuationSubring} (hpi : F.valuation.IsUniformizer (pi : K))
    (n : ℕ) (hn : 1 ≤ n) (r : F.valuationSubring) :
    higherPrincipalUnitGroup.principalUnitSuccQuotAddEquivResidueOfUniformizer
        F hpi n hn
        (Additive.ofMul
          (higherPrincipalUnitGroup.principalUnitSuccQuotOfIdealPow F n hn
            (maximalIdealPowMulUniformizerPowMap F.toDVF hpi n r))) =
      F.residueMap r

theorem

unitsModPrincipalUnitEquivOfPreserves_mem_principalUnitClassInQuotient_iff

L1264 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.unitsModPrincipalUnitEquivOfPreserves_mem_principalUnitClassInQuotient_iff

Documentation

The induced action on O^*/U^n preserves the image of U^m in that quotient. This is the finite-stage principal-unit class compatibility needed before applying prime-to-p quotient invisibility.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem unitsModPrincipalUnitEquivOfPreserves_mem_principalUnitClassInQuotient_iff
    (e : K ≃+* K)
    (hmem :
      ∀ x : K,
        x ∈ F.valuation.valuationSubring ↔
          e x ∈ F.valuation.valuationSubring)
    {m n : ℕ} (hmn : m ≤ n)
    (q : F.valuationSubringˣ ⧸ higherPrincipalUnitGroup F n) :
    unitsModPrincipalUnitEquivOfPreserves F e hmem n q ∈
        (higherPrincipalUnitGroup.toPrincipalUnitFiltration F).principalUnitSubgroupClassInQuotient
          m n ↔
      q ∈
        (higherPrincipalUnitGroup.toPrincipalUnitFiltration F).principalUnitSubgroupClassInQuotient
          m n

theorem

unitsModPrincipalUnitEquivOfPreserves_div_mem_principalUnitClass_one

L1306 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.unitsModPrincipalUnitEquivOfPreserves_div_mem_principalUnitClass_one

Documentation

If the induced residue-field automorphism is pointwise trivial, then the displacement of the induced action on O^*/U^n lies in the image of U^1/U^n.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem unitsModPrincipalUnitEquivOfPreserves_div_mem_principalUnitClass_one
    (e : K ≃+* K)
    (hmem :
      ∀ x : K,
        x ∈ F.valuation.valuationSubring ↔
          e x ∈ F.valuation.valuationSubring)
    (hres :
      ∀ x : F.residueField,
        valuationSubringResidueFieldEquivOfPreserves F e hmem x = x)
    (n : ℕ)
    (q : F.valuationSubringˣ ⧸ higherPrincipalUnitGroup F n) :
    unitsModPrincipalUnitEquivOfPreserves F e hmem n q / q ∈
      (higherPrincipalUnitGroup.toPrincipalUnitFiltration F).principalUnitSubgroupClassInQuotient
        1 n

theorem

finite_principalUnitSubgroupClassInQuotient_of_finite_residue

L1341 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.finite_principalUnitSubgroupClassInQuotient_of_finite_residue

Documentation

Therefore every adjacent concrete principal-unit class U^i/U^(i+1) is finite when the residue field is finite.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
open ValuationTheory.DiscreteValuationField.DVF
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)

Lean source · statement

theorem finite_principalUnitSubgroupClassInQuotient_of_finite_residue
    [Finite F.residueField] (i : ℕ) :
    Finite
      ((higherPrincipalUnitGroup.toPrincipalUnitFiltration F).principalUnitSubgroupClassInQuotient
        i (i + 1))

Module documentation

Successive principal-unit quotients

Declarations