Module

UniqueRing.lean

Nyll.ValuedFieldTheory.Valuation.UniqueRing

12 declarations indexed from sourceView source ↗

Module documentation

The unique-extension characterization: automorphism invariance from unique extension

The pullback of an extension valuation ring by a ground-field automorphism is again an extension valuation ring. Hence uniqueness forces the chosen ring to be fixed by every automorphism of the extension field. This is the first Galois-theoretic step in the converse direction of the unique-extension characterization.

Imports3

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.ChevalleyExtension
Mathlib.RingTheory.Valuation.RamificationGroup
Mathlib.FieldTheory.Normal.Basic

Imported by5

theorem

algEquiv_smul_valuationSubring_hasExtension

L30 ↗

ValuationTheory.Valuations.algEquiv_smul_valuationSubring_hasExtension

Documentation

Translating an extension valuation ring by a K-automorphism preserves the extension property.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
open scoped Pointwise
namespace Valuations

Lean source · statement

theorem algEquiv_smul_valuationSubring_hasExtension
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (V : ValuationSubring K) (W : ValuationSubring L)
    (hW : V.valuation.HasExtension W.valuation)
    (σ : L ≃ₐ[K] L) :
    V.valuation.HasExtension (σ • W).valuation

theorem

algEquiv_smul_valuationSubring_eq_of_unique_extension

L64 ↗

ValuationTheory.Valuations.algEquiv_smul_valuationSubring_eq_of_unique_extension

Documentation

If the extension valuation ring is unique, every ground-field automorphism stabilizes it.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
open scoped Pointwise
namespace Valuations

Lean source · statement

theorem algEquiv_smul_valuationSubring_eq_of_unique_extension
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (V : ValuationSubring K) (W : ValuationSubring L)
    (hW : V.valuation.HasExtension W.valuation)
    (huniq : ∀ W' : ValuationSubring L,
      V.valuation.HasExtension W'.valuation → W' = W)
    (σ : L ≃ₐ[K] L) :
    σ • W = W

theorem

algEquiv_mem_valuationSubring_iff_of_unique_extension

L76 ↗

ValuationTheory.Valuations.algEquiv_mem_valuationSubring_iff_of_unique_extension

Documentation

The preceding equality in elementwise form.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
open scoped Pointwise
namespace Valuations

Lean source · statement

theorem algEquiv_mem_valuationSubring_iff_of_unique_extension
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (V : ValuationSubring K) (W : ValuationSubring L)
    (hW : V.valuation.HasExtension W.valuation)
    (huniq : ∀ W' : ValuationSubring L,
      V.valuation.HasExtension W'.valuation → W' = W)
    (σ : L ≃ₐ[K] L) (x : L) :
    σ x ∈ W.toSubring ↔ x ∈ W.toSubring

def

valuationSubringEquivOfUniqueExtension

L98 ↗

ValuationTheory.Valuations.valuationSubringEquivOfUniqueExtension

Documentation

A ground-field automorphism restricts to an automorphism of the unique extension valuation ring.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
open scoped Pointwise
namespace Valuations

Lean source · full declaration

def valuationSubringEquivOfUniqueExtension
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (V : ValuationSubring K) (W : ValuationSubring L)
    (hW : V.valuation.HasExtension W.valuation)
    (huniq : ∀ W' : ValuationSubring L,
      V.valuation.HasExtension W'.valuation → W' = W)
    (σ : L ≃ₐ[K] L) : W ≃+* W where
  toFun x := ⟨σ (x : L),
    (algEquiv_mem_valuationSubring_iff_of_unique_extension
      V W hW huniq σ (x : L)).2 x.2⟩
  invFun x := ⟨σ⁻¹ (x : L),
    (algEquiv_mem_valuationSubring_iff_of_unique_extension
      V W hW huniq σ⁻¹ (x : L)).2 x.2⟩
  left_inv x := by ext; simp
  right_inv x := by ext; simp
  map_mul' x y := by ext; simp
  map_add' x y := by ext; simp

theorem

coe_valuationSubringEquivOfUniqueExtension_apply

L118 ↗

ValuationTheory.Valuations.coe_valuationSubringEquivOfUniqueExtension_apply

Documentation

The unique-extension equivalence acts on underlying valuation-ring elements as expected.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
open scoped Pointwise
namespace Valuations

Lean source · statement

theorem coe_valuationSubringEquivOfUniqueExtension_apply
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (V : ValuationSubring K) (W : ValuationSubring L)
    (hW : V.valuation.HasExtension W.valuation)
    (huniq : ∀ W' : ValuationSubring L,
      V.valuation.HasExtension W'.valuation → W' = W)
    (σ : L ≃ₐ[K] L) (x : W) :
    ((valuationSubringEquivOfUniqueExtension V W hW huniq σ x : W) : L) =
      σ (x : L)

def

residueFieldEquivOfUniqueExtension

L131 ↗

ValuationTheory.Valuations.residueFieldEquivOfUniqueExtension

Documentation

The induced automorphism of the residue field of the unique extension valuation ring.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
open scoped Pointwise
namespace Valuations

Lean source · statement

def residueFieldEquivOfUniqueExtension
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (V : ValuationSubring K) (W : ValuationSubring L)
    (hW : V.valuation.HasExtension W.valuation)
    (huniq : ∀ W' : ValuationSubring L,
      V.valuation.HasExtension W'.valuation → W' = W)
    (σ : L ≃ₐ[K] L) :
    IsLocalRing.ResidueField W ≃+* IsLocalRing.ResidueField W

theorem

residueFieldEquivOfUniqueExtension_residue

L144 ↗

ValuationTheory.Valuations.residueFieldEquivOfUniqueExtension_residue

Documentation

Reduction commutes with the automorphism induced on the unique extension's residue field.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
open scoped Pointwise
namespace Valuations

Lean source · statement

theorem residueFieldEquivOfUniqueExtension_residue
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (V : ValuationSubring K) (W : ValuationSubring L)
    (hW : V.valuation.HasExtension W.valuation)
    (huniq : ∀ W' : ValuationSubring L,
      V.valuation.HasExtension W'.valuation → W' = W)
    (σ : L ≃ₐ[K] L) (x : W) :
    residueFieldEquivOfUniqueExtension V W hW huniq σ
        (IsLocalRing.residue W x) =
      IsLocalRing.residue W
        ⟨σ (x : L),
          (algEquiv_mem_valuationSubring_iff_of_unique_extension
            V W hW huniq σ (x : L)).2 x.2⟩

def

valuationSubringMapOfHasExtension

L167 ↗

ValuationTheory.Valuations.valuationSubringMapOfHasExtension

Documentation

The canonical homomorphism from the base valuation ring into an extension valuation ring, without identifying either ring with the valuation subring of its canonical valuation.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
open scoped Pointwise
namespace Valuations

Lean source · statement

def valuationSubringMapOfHasExtension
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (V : ValuationSubring K) (W : ValuationSubring L)
    (hW : V.valuation.HasExtension W.valuation) : V →+* W

theorem

valuationSubringMapOfHasExtension_isLocalHom

L182 ↗

ValuationTheory.Valuations.valuationSubringMapOfHasExtension_isLocalHom

Documentation

The canonical map of valuation rings attached to an extension is local.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
open scoped Pointwise
namespace Valuations

Lean source · statement

theorem valuationSubringMapOfHasExtension_isLocalHom
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (V : ValuationSubring K) (W : ValuationSubring L)
    (hW : V.valuation.HasExtension W.valuation) :
    IsLocalHom (valuationSubringMapOfHasExtension V W hW)

def

residueFieldMapOfHasExtension

L201 ↗

ValuationTheory.Valuations.residueFieldMapOfHasExtension

Documentation

The residue-field homomorphism induced by the canonical local map of valuation rings.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
open scoped Pointwise
namespace Valuations

Lean source · statement

def residueFieldMapOfHasExtension
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (V : ValuationSubring K) (W : ValuationSubring L)
    (hW : V.valuation.HasExtension W.valuation) :
    IsLocalRing.ResidueField V →+* IsLocalRing.ResidueField W

theorem

residueFieldEquivOfUniqueExtension_algebraMap

L213 ↗

ValuationTheory.Valuations.residueFieldEquivOfUniqueExtension_algebraMap

Documentation

The induced residue-field automorphism fixes the embedded residue field of the base valuation ring.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
open scoped Pointwise
namespace Valuations

Lean source · statement

theorem residueFieldEquivOfUniqueExtension_algebraMap
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (V : ValuationSubring K) (W : ValuationSubring L)
    [hW : V.valuation.HasExtension W.valuation]
    (huniq : ∀ W' : ValuationSubring L,
      V.valuation.HasExtension W'.valuation → W' = W)
    (σ : L ≃ₐ[K] L)
    (x : IsLocalRing.ResidueField V) :
    residueFieldEquivOfUniqueExtension V W hW huniq σ
        (residueFieldMapOfHasExtension V W hW x) =
      residueFieldMapOfHasExtension V W hW x

theorem

minpoly_residue_eq_of_minpoly_eq_of_unique_extension

L239 ↗

ValuationTheory.Valuations.minpoly_residue_eq_of_minpoly_eq_of_unique_extension

Documentation

Conjugate integral elements have conjugate reductions over the residue field of the base valuation ring. In particular, their reductions have the same minimal polynomial. This is the residue-field form of the Galois argument used in the converse direction of the unique-extension characterization.

Source context 4 commands

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

namespace ValuationTheory
noncomputable section
open scoped Pointwise
namespace Valuations

Lean source · full declaration

theorem minpoly_residue_eq_of_minpoly_eq_of_unique_extension
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    [Normal K L]
    (V : ValuationSubring K) (W : ValuationSubring L)
    [hW : V.valuation.HasExtension W.valuation]
    (huniq : ∀ W' : ValuationSubring L,
      V.valuation.HasExtension W'.valuation → W' = W)
    {x y : L} (hxy : minpoly K x = minpoly K y)
    (hx : x ∈ W.toSubring) (hy : y ∈ W.toSubring) :
    letI : Algebra (IsLocalRing.ResidueField V)
        (IsLocalRing.ResidueField W) :=
      (residueFieldMapOfHasExtension V W hW).toAlgebra
    minpoly (IsLocalRing.ResidueField V)
        (IsLocalRing.residue W ⟨x, hx⟩) =
      minpoly (IsLocalRing.ResidueField V)
        (IsLocalRing.residue W ⟨y, hy⟩) := by
  let : Algebra (IsLocalRing.ResidueField V)
      (IsLocalRing.ResidueField W) :=
    (residueFieldMapOfHasExtension V W hW).toAlgebra
  obtain ⟨σ, hσ⟩ := (Normal.minpoly_eq_iff_mem_orbit L).1 hxy
  let e : IsLocalRing.ResidueField W ≃ₐ[IsLocalRing.ResidueField V]
      IsLocalRing.ResidueField W :=
    { residueFieldEquivOfUniqueExtension V W hW huniq σ with
      commutes' := fun z =>
        residueFieldEquivOfUniqueExtension_algebraMap V W huniq σ z }
  have hred :
      e (IsLocalRing.residue W ⟨y, hy⟩) =
        IsLocalRing.residue W ⟨x, hx⟩ := by
    change
      residueFieldEquivOfUniqueExtension V W hW huniq σ
          (IsLocalRing.residue W ⟨y, hy⟩) =
        IsLocalRing.residue W ⟨x, hx⟩
    rw [residueFieldEquivOfUniqueExtension_residue]
    congr 1
    exact Subtype.ext hσ
  rw [← hred]
  exact minpoly.algEquiv_eq e _

Module documentation

The unique-extension characterization: automorphism invariance from unique extension

Declarations