NYLL
Module

PurelyInseparable.lean

Nyll.SchemeTheory.FunctionFields.Valuations.PurelyInseparable
13 declarations indexed from sourceView source ↗

Module documentation

Valuation subrings in purely inseparable extensions

Let E / F be a purely inseparable extension of fields. Membership in a valuation subring of E can be tested after raising an element to a positive power. A sufficiently large exponential-characteristic power of every element of E lies in the image of F. It follows that a valuation subring of E is determined by its restriction to F.

This supplies the inseparable part of valuation-extension counting: after restricting from an algebraic extension to its maximal separable subextension, no two valuation subrings become equal.

Imports2
  • Mathlib.FieldTheory.PurelyInseparable.Basic
  • Mathlib.RingTheory.Valuation.ValuationSubring
Imported by2

Declarations

theorem

mem_iff_pow_mem

L42 ↗
FieldArithmetic.Chapter06.PurelyInseparableValuation.mem_iff_pow_mem
Documentation

Membership in a valuation subring can be detected after taking any positive power.

The reverse implication uses only the defining valuation-ring dichotomy. If x⁻¹ belongs to the valuation subring as well as x ^ n, then x = x ^ n * (x⁻¹) ^ (n - 1) belongs to it.

Source context 6 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PurelyInseparableValuation
universe u v
variable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E]
Lean source · statement
theorem mem_iff_pow_mem
    (A : ValuationSubring E) (x : E) {n : ℕ} (hn : 0 < n) :
    x ∈ A ↔ x ^ n ∈ A
def

restriction

L69 ↗
FieldArithmetic.Chapter06.PurelyInseparableValuation.restriction
Documentation

Restrict a valuation subring along the field-extension map.

Source context 6 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PurelyInseparableValuation
universe u v
variable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E]
Lean source · statement
def restriction (A : ValuationSubring E) : ValuationSubring F
theorem

mem_restriction

L73 ↗
FieldArithmetic.Chapter06.PurelyInseparableValuation.mem_restriction
Source context 6 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PurelyInseparableValuation
universe u v
variable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E]
Lean source · statement
theorem mem_restriction (A : ValuationSubring E) (x : F) :
    x ∈ restriction A ↔ algebraMap F E x ∈ A
theorem

restriction_injective

L85 ↗
FieldArithmetic.Chapter06.PurelyInseparableValuation.restriction_injective
Documentation

Restriction of valuation subrings along a purely inseparable field extension is injective.

For x : E, choose n such that x ^ (ringExpChar F) ^ n = algebraMap F E y. Positive-power membership and equality of the two restrictions then decide membership of x.

Source context 6 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PurelyInseparableValuation
universe u v
variable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E]
Lean source · statement
theorem restriction_injective [IsPurelyInseparable F E] :
    Function.Injective
      (restriction : ValuationSubring E → ValuationSubring F)
theorem

eq_of_restriction_eq

L100 ↗
FieldArithmetic.Chapter06.PurelyInseparableValuation.eq_of_restriction_eq
Documentation

Two valuation subrings over the same restriction are equal.

Source context 6 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PurelyInseparableValuation
universe u v
variable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E]
Lean source · statement
theorem eq_of_restriction_eq [IsPurelyInseparable F E]
    {A B : ValuationSubring E}
    (h : restriction (F := F) A = restriction (F := F) B) :
    A = B
def

Extensions

L109 ↗
FieldArithmetic.Chapter06.PurelyInseparableValuation.Extensions
Documentation

Valuation subrings of E extending a fixed valuation subring of F.

Source context 6 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PurelyInseparableValuation
universe u v
variable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E]
Lean source · statement
def Extensions (R : ValuationSubring F)
instance

extensions_subsingleton

L116 ↗
FieldArithmetic.Chapter06.PurelyInseparableValuation.extensions_subsingleton
Documentation

A valuation subring has at most one extension through a purely inseparable field extension.

Source context 6 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PurelyInseparableValuation
universe u v
variable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E]
Lean source · full declaration
instance extensions_subsingleton [IsPurelyInseparable F E]
    (R : ValuationSubring F) :
    Subsingleton (Extensions (E := E) R) where
  allEq A B := by
    apply Subtype.ext
    apply restriction_injective (F := F) (E := E)
    exact A.property.trans B.property.symm
theorem

natCard_extensions_le_one

L128 ↗
FieldArithmetic.Chapter06.PurelyInseparableValuation.natCard_extensions_le_one
Documentation

Consequently, any finite collection of extensions of a fixed valuation subring through a purely inseparable extension has cardinality at most one.

Source context 6 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PurelyInseparableValuation
universe u v
variable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E]
Lean source · statement
theorem natCard_extensions_le_one [IsPurelyInseparable F E]
    (R : ValuationSubring F) [Finite (Extensions (E := E) R)] :
    Nat.card (Extensions (E := E) R) ≤ 1
def

restrictionToSeparableClosure

L137 ↗
FieldArithmetic.Chapter06.PurelyInseparableValuation.restrictionToSeparableClosure
Documentation

Restrict a valuation subring to the separable closure of F inside an algebraic extension E.

Source context 6 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PurelyInseparableValuation
universe u v
variable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E]
Lean source · statement
def restrictionToSeparableClosure [Algebra.IsAlgebraic F E]
    (A : ValuationSubring E) :
    ValuationSubring (separableClosure F E)
theorem

restrictionToSeparableClosure_injective

L149 ↗
FieldArithmetic.Chapter06.PurelyInseparableValuation.restrictionToSeparableClosure_injective
Documentation

In an algebraic extension, valuation subrings inject into the valuation subrings of the maximal separable subextension.

Indeed, E is purely inseparable over separableClosure F E, so the previous restriction theorem applies verbatim.

Source context 6 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PurelyInseparableValuation
universe u v
variable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E]
Lean source · statement
theorem restrictionToSeparableClosure_injective
    [Algebra.IsAlgebraic F E] :
    Function.Injective
      (restrictionToSeparableClosure (F := F) (E := E))
def

extensionRestrictionToSeparableClosure

L162 ↗
FieldArithmetic.Chapter06.PurelyInseparableValuation.extensionRestrictionToSeparableClosure
Documentation

Restrict an extension of R to the maximal separable subextension.

The scalar-tower identity shows that the resulting valuation subring still restricts to R.

Source context 6 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PurelyInseparableValuation
universe u v
variable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E]
Lean source · statement
def extensionRestrictionToSeparableClosure [Algebra.IsAlgebraic F E]
    (R : ValuationSubring F) :
    Extensions (E := E) R →
      Extensions (F := F) (E := separableClosure F E) R
theorem

extensionRestrictionToSeparableClosure_injective

L177 ↗
FieldArithmetic.Chapter06.PurelyInseparableValuation.extensionRestrictionToSeparableClosure_injective
Documentation

Extension counting over an algebraic field extension reduces injectively to extension counting over its maximal separable subextension.

Source context 6 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PurelyInseparableValuation
universe u v
variable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E]
Lean source · statement
theorem extensionRestrictionToSeparableClosure_injective
    [Algebra.IsAlgebraic F E] (R : ValuationSubring F) :
    Function.Injective
      (extensionRestrictionToSeparableClosure (E := E) R)
theorem

natCard_extensions_le_separableClosure

L190 ↗
FieldArithmetic.Chapter06.PurelyInseparableValuation.natCard_extensions_le_separableClosure
Documentation

The corresponding numerical extension count is bounded by the count over the separable closure whenever that target collection is finite.

Source context 6 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PurelyInseparableValuation
universe u v
variable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E]
Lean source · statement
theorem natCard_extensions_le_separableClosure
    [Algebra.IsAlgebraic F E] (R : ValuationSubring F)
    [Finite (Extensions (F := F) (E := separableClosure F E) R)] :
    Nat.card (Extensions (E := E) R) ≤
      Nat.card (Extensions (F := F) (E := separableClosure F E) R)

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