ModuleIntegerValuationUniformizer.lean
Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.ValuationSubringUnits.IntegerValuationUniformizer
7 declarations indexed from sourceView source ↗ Module documentation
Uniformizers and unit subgroups for induced integer valuations
This file relates the induced integer valuation to normalized uniformizers, valuation-ring units, and scalar extension of field units.
Declarations
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.ofWithZeroValuation_isUniformizer_of_valuation_eq_exp_neg
DocumentationAn element of ℤᵐ⁰-value exp (-1) is a uniformizer for the attached integer-valued multiplicative valuation.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open WithZero
open scoped WithZero
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.ofWithZeroValuation_hasUniformizer_of_exists_valuation_eq_exp_neg
DocumentationA normalized ℤᵐ⁰-valued valuation with an element of value exp (-1) has a uniformizer in the attached integer-valued multiplicative valuation.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open WithZero
open scoped WithZero
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.exists_unit_valuation_eq_exp_neg_of_surjective
DocumentationA surjective ℤᵐ⁰-valued valuation has a field unit of value exp (-1).
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open WithZero
open scoped WithZero
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.ofWithZeroValuation_hasUniformizer_of_surjective
DocumentationA surjective ℤᵐ⁰-valued valuation gives a uniformizer for the attached integer-valued multiplicative valuation.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open WithZero
open scoped WithZero
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.ofWithZeroValuation_val_surjective_of_surjective
DocumentationA surjective ℤᵐ⁰-valued valuation gives a surjective integer-valued valuation on field units.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open WithZero
open scoped WithZero
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.ofWithZeroValuation_zeroSubgroup_eq_unitGroup
DocumentationEstablishes the identity (ofWithZeroValuation v).zeroSubgroup = v.valuationSubring.unitGroup.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open WithZero
open scoped WithZero
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]
LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.baseUnitsMap_zeroSubgroup_ofWithZeroValuation
DocumentationEstablishes the membership statement ∀ u : Kˣ, u ∈ (ofWithZeroValuation vK).zeroSubgroup → baseUnitsMap (K := K) (L := L) u ∈ (ofWithZeroValuation vL).zeroSubgroup.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open WithZero
open scoped WithZero
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]
variable {L : Type u} [Field L] [Algebra K L]