Module

DVRLocalExtension.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.FiniteExtension.DVRLocalExtension

3 declarations indexed from sourceView source ↗

Module documentation

Valuation extension from a local map into a discrete valuation ring

A local map of valuation rings with the given fraction-field map determines an extension of valuations. Applied to an actual local DVR over the base valuation ring, this supplies the extension property of its normalized valuation.

Imports4

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.Basic
Mathlib.RingTheory.Valuation.Extension
Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing
Mathlib.RingTheory.LocalRing.RingHom.Basic

Imported by3

theorem

hasExtension_of_local_valuationSubring_map

L26 ↗

ValuationTheory.DiscreteValuationField.hasExtension_of_local_valuationSubring_map

Documentation

A local map of valuation subrings over the field inclusion determines the extension property, without completeness or discreteness assumptions.

Source context 2 commands

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

namespace ValuationTheory.DiscreteValuationField
variable {K L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem hasExtension_of_local_valuationSubring_map
    {ΓK ΓL : Type*} [LinearOrderedCommGroupWithZero ΓK]
    [LinearOrderedCommGroupWithZero ΓL]
    (vK : _root_.Valuation K ΓK) (vL : _root_.Valuation L ΓL)
    (f : vK.valuationSubring →+* vL.valuationSubring) [IsLocalHom f]
    (hcoe : ∀ z : vK.valuationSubring,
      (f z : L) = algebraMap K L (z : K)) :
    vK.HasExtension vL

theorem

dvr_equivValuationSubring_coe

L63 ↗

ValuationTheory.DiscreteValuationField.dvr_equivValuationSubring_coe

Documentation

Evaluation of the DVR-to-valuation-subring equivalence is the fraction map.

Source context 2 commands

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

namespace ValuationTheory.DiscreteValuationField
variable {K L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem dvr_equivValuationSubring_coe
    (A : Type*) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [Algebra A L] [IsFractionRing A L] (x : A) :
    (IsDiscreteValuationRing.equivValuationSubring (A := A) (K := L) x : L) =
      algebraMap A L x

theorem

hasExtension_dvr_valuation_of_isLocalHom

L72 ↗

ValuationTheory.DiscreteValuationField.hasExtension_dvr_valuation_of_isLocalHom

Documentation

A local DVR over the base valuation ring, with compatible fraction map, supplies an actual extension of the base discrete valuation.

Source context 2 commands

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

namespace ValuationTheory.DiscreteValuationField
variable {K L : Type*} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem hasExtension_dvr_valuation_of_isLocalHom (base : DVF K)
    (A : Type*) [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [Algebra A L] [IsFractionRing A L] [Algebra base.valuationSubring A]
    [IsScalarTower base.valuationSubring A L]
    [IsLocalHom (algebraMap base.valuationSubring A)] :
    base.valuation.HasExtension ((IsDiscreteValuationRing.maximalIdeal A).valuation L)

Module documentation

Valuation extension from a local map into a discrete valuation ring

Declarations

hasExtension_of_local_valuationSubring_map

dvr_equivValuationSubring_coe

hasExtension_dvr_valuation_of_isLocalHom