Module

FiniteResidueValuationComparison.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.FiniteResidueValuationComparison

1 declaration indexed from sourceView source ↗

Module documentation

Finite-separable comparison of restricted valuation rings

The valuation on an algebraic ambient field can be restricted to a finite intermediate field. Over a complete discrete valuation field this restriction is the unique extension valuation ring, so it agrees with any other extension valuation ring on the finite field. This is the valuation-ring comparison used in the finite local reciprocity construction before comparing residue degrees.

Imports2

Imported by3

theorem

restrictIntermediateField_eq_of_finite_separable

L37 ↗

LocalClassFieldTheory.ValuationSubring.restrictIntermediateField_eq_of_finite_separable

Documentation

Over a complete discrete valuation field, restricting an ambient extension valuation ring to a finite separable intermediate field gives the same valuation ring as any independently constructed extension valuation on that intermediate field.

Source context 5 commands

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

namespace LocalClassFieldTheory
open ValuationTheory RamificationTheory
noncomputable section
universe u v w
open DiscreteValuationField

Lean source · statement

theorem ValuationSubring.restrictIntermediateField_eq_of_finite_separable
    {K : Type u} {Omega : Type v} [Field K] [Field Omega] [Algebra K Omega]
    (base : CompleteDVF K)
    (A : ValuationSubring Omega) [base.valuation.HasExtension A.valuation]
    (E : IntermediateField K Omega) [FiniteDimensional K E]
    [Algebra.IsSeparable K E]
    (C : ValuationSubring E) [base.valuation.HasExtension C.valuation] :
    A.restrictIntermediateField E = C

Module documentation

Finite-separable comparison of restricted valuation rings

Declarations

restrictIntermediateField_eq_of_finite_separable