NYLL
Module

ValuationSubringUnitMap.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.ValuationSubringUnits.ValuationSubringUnitMap
3 declarations indexed from sourceView source ↗

Module documentation

Valuation-subring units inside field units

This file defines the canonical homomorphism from units of a complete-DVF valuation ring to units of its fraction field.

Imports1
Imported by10

Declarations

def

valuationSubringUnitsToFieldUnits

L31 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.valuationSubringUnitsToFieldUnits
Documentation

The inclusion O_K^* -> K^* for the chosen valuation ring of a complete DVF.

Source context 6 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
def valuationSubringUnitsToFieldUnits
    (F : CompleteDVF.{u, v} K) : F.valuationSubringˣ →* Kˣ
theorem

coe_valuationSubringUnitsToFieldUnits_apply

L40 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.coe_valuationSubringUnitsToFieldUnits_apply
Documentation

The defining evaluation formula for coe_valuationSubringUnitsToFieldUnits is (((CompleteDVF.valuationSubringUnitsToFieldUnits F) a : Kˣ) : K) = (a : F.valuationSubring).

Source context 6 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem coe_valuationSubringUnitsToFieldUnits_apply
    (F : CompleteDVF.{u, v} K) (a : F.valuationSubringˣ) :
    (((LocalFieldTheory.DiscreteValuationField.CompleteDVF.valuationSubringUnitsToFieldUnits F)
      a : Kˣ) : K) =
      (a : F.valuationSubring)
theorem

valuationSubringUnitsToFieldUnits_mem_unitGroup

L55 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.valuationSubringUnitsToFieldUnits_mem_unitGroup
Documentation

Establishes the membership statement (CompleteDVF.valuationSubringUnitsToFieldUnits F) a ∈ F.valuation.valuationSubring.unitGroup.

Source context 6 commands

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

noncomputable section
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
Lean source · statement
theorem valuationSubringUnitsToFieldUnits_mem_unitGroup
    (F : CompleteDVF.{u, v} K) (a : F.valuationSubringˣ) :
    (LocalFieldTheory.DiscreteValuationField.CompleteDVF.valuationSubringUnitsToFieldUnits F) a ∈
      F.valuation.valuationSubring.unitGroup

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