NYLL
Module

HenselianSeparableTensorField.lean

Nyll.ValuedFieldTheory.Valuation.Completion.HenselianSeparableTensorField
1 declaration indexed from sourceView source ↗

Module documentation

Separable algebraic extensions after Henselian completion

Each tensor element comes from a finite subextension. Inverting a nonzero lift there and mapping the inverse back proves the field property without assuming a comparison map is injective.

Imports4
Imported by2

Declarations

theorem

completionTensor_isField_of_isSeparable

L28 ↗
ValuationTheory.DiscreteValuationField.HenselianDVF.completionTensor_isField_of_isSeparable
Documentation

Completing a Henselian DVF preserves the field property of scalar extension by any separable algebraic extension, including a separable closure.

Source context 3 commands

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

namespace ValuationTheory.DiscreteValuationField.HenselianDVF
open scoped TensorProduct
variable {K : Type*} [Field K]
Lean source · statement
theorem completionTensor_isField_of_isSeparable (base : HenselianDVF K)
    (L : Type*) [Field L] [Algebra K L] [Algebra.IsSeparable K L] :
    IsField (base.valuation.Completion ⊗[K] L)

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