NYLL
Module

SubfieldMixedCharacteristic.lean

Nyll.Yamaguchi26AbfaithfulGalois.FieldExamples.SubfieldMixedCharacteristic
3 declarations indexed from sourceView source ↗

Module documentation

Mixed-characteristic valuations on extensions and subfields

The existence of a mixed-characteristic discrete valuation is preserved under essentially finite-type field extensions and restriction along field embeddings.

Imports5
Imported by2

Declarations

theorem

mixedChar_DVF_of_discreteValuationSubring

L25 ↗
Yamaguchi26AbfaithfulGalois.mixedChar_DVF_of_discreteValuationSubring
Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ValuationTheory.DiscreteValuationField
universe u v w
Lean source · statement
theorem mixedChar_DVF_of_discreteValuationSubring
    {E : Type u} [Field E] (p : ℕ) [Fact p.Prime]
    (W : ValuationSubring E) [IsDiscreteValuationRing W] (hp : (p : E) ∈ W.nonunits) :
    ∃ D : DVF.{u, 0} E, CharP D.residueField p
theorem

exists_mixedChar_DVF_of_essFiniteType

L48 ↗
Yamaguchi26AbfaithfulGalois.exists_mixedChar_DVF_of_essFiniteType
Documentation

Finite generation preserves the existence of a mixed-characteristic DVR.

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ValuationTheory.DiscreteValuationField
universe u v w
Lean source · statement
theorem exists_mixedChar_DVF_of_essFiniteType
    (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E]
    [CharZero F] [Algebra.EssFiniteType F E]
    (base : DVF.{u, w} F) (p : ℕ) [Fact p.Prime] [CharP base.residueField p] :
    ∃ D : DVF.{v, 0} E, CharP D.residueField p
theorem

exists_mixedChar_DVF_of_embedding

L78 ↗
Yamaguchi26AbfaithfulGalois.exists_mixedChar_DVF_of_embedding
Documentation

Restricting a mixed-characteristic discrete valuation along any field embedding remains nontrivial, since the prime has positive valuation.

Source context 3 commands

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

namespace Yamaguchi26AbfaithfulGalois
open ValuationTheory.DiscreteValuationField
universe u v w
Lean source · statement
theorem exists_mixedChar_DVF_of_embedding
    {K : Type u} {E : Type v} [Field K] [Field E] [CharZero E]
    (f : K →+* E) (base : DVF.{v, w} E) (p : ℕ) [Fact p.Prime]
    [CharP base.residueField p] : ∃ D : DVF.{u, 0} K, CharP D.residueField p

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