Module

ValuedExtensionUnitMap.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.ValuationSubringUnits.ValuedExtensionUnitMap

4 declarations indexed from sourceView source ↗

Module documentation

Valuation-subring units in complete-DVF extensions

This file proves compatibility of valuation-ring units with scalar extension and relates the value of an embedded base uniformizer to the ramification index.

Imports3

Imported by6

theorem

baseUnitsMap_mem_target_unitGroup_of_mem_base_unitGroup

L39 ↗

LocalFieldTheory.DiscreteValuationField.ValuedExtension.baseUnitsMap_mem_target_unitGroup_of_mem_base_unitGroup

Documentation

Embedded base field units of valuation one remain valuation-one units in the target field.

Source context 10 commands

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

noncomputable section
universe u v x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type u} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{u, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem baseUnitsMap_mem_target_unitGroup_of_mem_base_unitGroup
    {a : Kˣ}
    (ha : a ∈ base.valuation.valuationSubring.unitGroup) :
    baseUnitsMap (K := K) (L := L) a ∈
      target.valuation.valuationSubring.unitGroup

theorem

baseUnitGroup_map_le_target_unitGroup

L51 ↗

LocalFieldTheory.DiscreteValuationField.ValuedExtension.baseUnitGroup_map_le_target_unitGroup

Documentation

Subgroup form: the embedded base valuation-one unit group maps into the target valuation-one unit group.

Source context 10 commands

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

noncomputable section
universe u v x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type u} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{u, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem baseUnitGroup_map_le_target_unitGroup
    :
    (base.valuation.valuationSubring.unitGroup).map
        (baseUnitsMap (K := K) (L := L)) ≤
      target.valuation.valuationSubring.unitGroup

theorem

baseUnitsMap_valuationSubringUnitsToFieldUnits

L61 ↗

LocalFieldTheory.DiscreteValuationField.ValuedExtension.baseUnitsMap_valuationSubringUnitsToFieldUnits

Documentation

Compatibility between the valuation-ring unit map and the field-unit map.

Source context 10 commands

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

noncomputable section
universe u v x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type u} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{u, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem baseUnitsMap_valuationSubringUnitsToFieldUnits
    (a : base.valuationSubringˣ) :
    baseUnitsMap (K := K) (L := L)
        ((CompleteDVF.valuationSubringUnitsToFieldUnits base) a) =
      (CompleteDVF.valuationSubringUnitsToFieldUnits target)
        (Units.map (integerMap base.toDVF target.toDVF).toMonoidHom a)

theorem

base_uniformizer_image_val_eq_ramificationIndex

L77 ↗

LocalFieldTheory.DiscreteValuationField.ValuedExtension.base_uniformizer_image_val_eq_ramificationIndex

Documentation

The ramification-ideal unit-multiple source gives the value of the embedded base uniformizer.

This is the source-producing bridge from exists_unit_mul_target_uniformizer_pow_eq_base_uniformizer_image to the hϖmap input used by ValuationScaling.lean.

Source context 10 commands

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

noncomputable section
universe u v x
namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace ValuedExtension
open ValuationTheory.DiscreteValuationField.ValuedExtension
variable {K : Type u} {L : Type u} [Field K] [Field L]
variable [Algebra K L]
variable (base : CompleteDVF.{u, v} K) (target : CompleteDVF.{u, x} L)
variable [base.valuation.HasExtension target.valuation]

Lean source · statement

theorem base_uniformizer_image_val_eq_ramificationIndex
    (vL : MultiplicativeIntegerValuation Lˣ)
    (hunit :
      ∀ u : target.valuationSubringˣ,
        (CompleteDVF.valuationSubringUnitsToFieldUnits target) u ∈ vL.zeroSubgroup)
    {ϖ : base.valuationSubring} {π : target.valuationSubring}
    (hϖ : base.valuation.IsUniformizer (ϖ : K))
    (hπ : target.valuation.IsUniformizer (π : L))
    (hπval : vL.val (Units.mk0 (π : L) hπ.ne_zero) = 1) :
    vL.val
        (baseUnitsMap (K := K) (L := L)
          (Units.mk0 (ϖ : K) hϖ.ne_zero)) =
      (ramificationIndex base.toDVF target.toDVF : ℤ)

Module documentation

Valuation-subring units in complete-DVF extensions

Declarations

baseUnitsMap_mem_target_unitGroup_of_mem_base_unitGroup

baseUnitGroup_map_le_target_unitGroup

baseUnitsMap_valuationSubringUnitsToFieldUnits

base_uniformizer_image_val_eq_ramificationIndex