Module

ResidueQuotient.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PrincipalUnits.ResidueQuotient

4 declarations indexed from sourceView source ↗

Module documentation

The first principal-unit quotient

Identifies valuation-ring units modulo first principal units with residue-field units and records compatibility with valuation-preserving automorphisms.

Imports1

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PrincipalUnits.AutomorphismTransport

Imported by5

theorem

residueUnitHom_ker_eq

L40 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueUnitHom_ker_eq

Documentation

The kernel of the residue map on valuation-ring units is the first principal-unit subgroup.

Source context 11 commands

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

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

Lean source · statement

theorem residueUnitHom_ker_eq :
    (higherPrincipalUnitGroup.residueUnitHom F).ker =
      higherPrincipalUnitGroup F 1

def

unitsModOneEquivResidueFieldUnits

L48 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.unitsModOneEquivResidueFieldUnits

Documentation

The first-isomorphism form of the residue map on valuation-ring units: O_K^* / U_K^1 is the unit group of the residue field.

Source context 11 commands

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

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

Lean source · statement

def unitsModOneEquivResidueFieldUnits :
    F.valuationSubringˣ ⧸ higherPrincipalUnitGroup F 1 ≃* F.residueFieldˣ

theorem

unitsModOneEquivResidueFieldUnits_mk

L64 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.unitsModOneEquivResidueFieldUnits_mk

Documentation

Establishes the identity higherPrincipalUnitGroup.unitsModOneEquivResidueFieldUnits F (QuotientGroup.mk' (higherPrincipalUnitGroup F 1) u) = higherPrincipalUnitGroup.residueUnitHom F u.

Source context 11 commands

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

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

Lean source · statement

theorem unitsModOneEquivResidueFieldUnits_mk
    (u : F.valuationSubringˣ) :
    higherPrincipalUnitGroup.unitsModOneEquivResidueFieldUnits F
        (QuotientGroup.mk' (higherPrincipalUnitGroup F 1) u) =
      higherPrincipalUnitGroup.residueUnitHom F u

theorem

unitsModOneEquivResidueFieldUnits_unitsModPrincipalUnitEquivOfPreserves_one

L73 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.unitsModOneEquivResidueFieldUnits_unitsModPrincipalUnitEquivOfPreserves_one

Documentation

Compatibility of the induced action on O^*/U^1 with the induced action on residue-field units.

Source context 11 commands

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

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

Lean source · statement

theorem unitsModOneEquivResidueFieldUnits_unitsModPrincipalUnitEquivOfPreserves_one
    (e : K ≃+* K)
    (hmem :
      ∀ x : K,
        x ∈ F.valuation.valuationSubring ↔
          e x ∈ F.valuation.valuationSubring)
    (q : F.valuationSubringˣ ⧸ higherPrincipalUnitGroup F 1) :
    higherPrincipalUnitGroup.unitsModOneEquivResidueFieldUnits F
        (higherPrincipalUnitGroup.unitsModPrincipalUnitEquivOfPreserves
          F e hmem 1 q) =
      Units.map
        (valuationSubringResidueFieldEquivOfPreserves F e hmem).toMonoidHom
        (higherPrincipalUnitGroup.unitsModOneEquivResidueFieldUnits F q)

Module documentation

The first principal-unit quotient

Declarations

residueUnitHom_ker_eq

unitsModOneEquivResidueFieldUnits

unitsModOneEquivResidueFieldUnits_mk

unitsModOneEquivResidueFieldUnits_unitsModPrincipalUnitEquivOfPreserves_one