NYLL
Module

MixedCharCompleteExtension.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.MixedCharCompleteExtension
1 declaration indexed from sourceView source ↗

Module documentation

Complete extension valuations with the base residue characteristic

A finite separable extension receives an integer-valued complete discrete valuation. The induced embedding of residue fields preserves characteristic.

Imports4
Imported by3

Declarations

theorem

exists_complete_valuation_of_finite_separable_of_residueChar

L23 ↗
ValuationTheory.DiscreteValuationField.ValuedExtension.exists_complete_valuation_of_finite_separable_of_residueChar
Documentation

A finite separable extension has a complete integer-valued valuation extending the given valuation and with the same residue characteristic.

Source context 1 command

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

namespace ValuationTheory.DiscreteValuationField.ValuedExtension
Lean source · statement
theorem exists_complete_valuation_of_finite_separable_of_residueChar
    {F E : Type*} [Field F] [Field E] [Algebra F E]
    [FiniteDimensional F E] [Algebra.IsSeparable F E]
    (vF : _root_.Valuation F (WithZero (Multiplicative ℤ)))
    [Valuation.IsCompleteDiscrete vF] (n : ℕ)
    [hres : CharP (IsLocalRing.ResidueField vF.valuationSubring) n] :
    ∃ vE : _root_.Valuation E (WithZero (Multiplicative ℤ)),
      Valuation.IsCompleteDiscrete vE ∧ vF.HasExtension vE ∧
        CharP (IsLocalRing.ResidueField vE.valuationSubring) n

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