NYLL
Module

FiniteLevelValuationRestriction.lean

Nyll.ValuedFieldTheory.Ramification.GaloisValuation.AbsoluteGalois.FiniteLevelValuationRestriction
17 declarations indexed from sourceView source ↗

Module documentation

Finite-level valuation restriction for absolute Galois arguments

This file isolates the valuation-restriction and separable-power lemmas used to pass from absolute Galois questions to finite intermediate fields.

Imports38
Imported by2

Declarations

theorem

mem_iff_pow_mem

L74 ↗
RamificationTheory.ValuationSubring.mem_iff_pow_mem
Documentation

Membership in a valuation subring is detected by any positive natural power.

This is useful in absolute arguments: after moving an element into a finite separable level only after taking a positive power, valuation-subring membership can be pulled back to the original element.

Source context 7 commands

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

namespace RamificationTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.HenselianDVF
noncomputable section
universe u v w z
namespace ValuationSubring
variable {K : Type u} [Field K] (A : ValuationSubring K)
Lean source · statement
theorem mem_iff_pow_mem (x : K) {n : ℕ} (hn : 0 < n) :
    x ∈ A ↔ x ^ n ∈ A
theorem

mem_of_pow_mem

L101 ↗
RamificationTheory.ValuationSubring.mem_of_pow_mem
Documentation

States the theorem mem_of_pow_mem.

Source context 7 commands

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

namespace RamificationTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.HenselianDVF
noncomputable section
universe u v w z
namespace ValuationSubring
variable {K : Type u} [Field K] (A : ValuationSubring K)
Lean source · statement
theorem mem_of_pow_mem (x : K) {n : ℕ} (hn : 0 < n) (hx : x ^ n ∈ A) :
    x ∈ A
theorem

pow_mem_iff_mem

L106 ↗
RamificationTheory.ValuationSubring.pow_mem_iff_mem
Documentation

States the theorem pow_mem_iff_mem.

Source context 7 commands

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

namespace RamificationTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.HenselianDVF
noncomputable section
universe u v w z
namespace ValuationSubring
variable {K : Type u} [Field K] (A : ValuationSubring K)
Lean source · statement
theorem pow_mem_iff_mem (x : K) {n : ℕ} (hn : 0 < n) :
    x ^ n ∈ A ↔ x ∈ A
def

restrictIntermediateField

L115 ↗
RamificationTheory.ValuationSubring.restrictIntermediateField
Documentation

Restrict a valuation subring of an ambient field to an intermediate field.

Source context 9 commands

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

namespace RamificationTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.HenselianDVF
noncomputable section
universe u v w z
namespace ValuationSubring
variable {K : Type u} [Field K] (A : ValuationSubring K)
section RestrictIntermediateField
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
Lean source · statement
def restrictIntermediateField
    (A : ValuationSubring Ω) (E : IntermediateField K Ω) :
    ValuationSubring E
theorem

restrictIntermediateField_eq_comap

L121 ↗
RamificationTheory.ValuationSubring.restrictIntermediateField_eq_comap
Documentation

States the theorem restrictIntermediateField_eq_comap.

Source context 9 commands

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

namespace RamificationTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.HenselianDVF
noncomputable section
universe u v w z
namespace ValuationSubring
variable {K : Type u} [Field K] (A : ValuationSubring K)
section RestrictIntermediateField
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
Lean source · statement
theorem restrictIntermediateField_eq_comap
    (A : ValuationSubring Ω) (E : IntermediateField K Ω) :
    (restrictIntermediateField A E) = A.comap (algebraMap E Ω)
theorem

mem_restrictIntermediateField_iff

L127 ↗
RamificationTheory.ValuationSubring.mem_restrictIntermediateField_iff
Documentation

States the theorem mem_restrictIntermediateField_iff.

Source context 9 commands

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

namespace RamificationTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.HenselianDVF
noncomputable section
universe u v w z
namespace ValuationSubring
variable {K : Type u} [Field K] (A : ValuationSubring K)
section RestrictIntermediateField
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
Lean source · statement
theorem mem_restrictIntermediateField_iff
    (A : ValuationSubring Ω) (E : IntermediateField K Ω) (x : E) :
    x ∈ (restrictIntermediateField A E) ↔ (x : Ω) ∈ A
theorem

restrictIntermediateField_hasExtension

L133 ↗
RamificationTheory.ValuationSubring.restrictIntermediateField_hasExtension
Documentation

States the theorem restrictIntermediateField_hasExtension.

Source context 9 commands

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

namespace RamificationTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.HenselianDVF
noncomputable section
universe u v w z
namespace ValuationSubring
variable {K : Type u} [Field K] (A : ValuationSubring K)
section RestrictIntermediateField
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
Lean source · statement
theorem restrictIntermediateField_hasExtension
    {Γ : Type w} [LinearOrderedCommGroupWithZero Γ]
    (v : Valuation K Γ) (A : ValuationSubring Ω)
    [_root_.Valuation.HasExtension v A.valuation]
    (E : IntermediateField K Ω) :
    _root_.Valuation.HasExtension v ((restrictIntermediateField A E)).valuation
theorem

mem_inv_smul_iff_apply_mem

L154 ↗
RamificationTheory.ValuationSubring.mem_inv_smul_iff_apply_mem
Documentation

Membership in the inverse translate is the same as membership after applying the automorphism.

Source context 10 commands

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

namespace RamificationTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.HenselianDVF
noncomputable section
universe u v w z
namespace ValuationSubring
variable {K : Type u} [Field K] (A : ValuationSubring K)
section RestrictIntermediateField
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
open scoped Pointwise
Lean source · statement
theorem mem_inv_smul_iff_apply_mem
    (A : ValuationSubring Ω) (σ : Ω ≃ₐ[K] Ω) (z : Ω) :
    z ∈ σ⁻¹ • A ↔ σ z ∈ A
theorem

mem_smul_valuationSubring_iff

L163 ↗
RamificationTheory.ValuationSubring.mem_smul_valuationSubring_iff
Documentation

Membership in an automorphic translate is membership after applying the inverse automorphism.

Source context 10 commands

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

namespace RamificationTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.HenselianDVF
noncomputable section
universe u v w z
namespace ValuationSubring
variable {K : Type u} [Field K] (A : ValuationSubring K)
section RestrictIntermediateField
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
open scoped Pointwise
Lean source · statement
theorem mem_smul_valuationSubring_iff
    (A : ValuationSubring Ω) (σ : Ω ≃ₐ[K] Ω) (z : Ω) :
    z ∈ σ • A ↔ σ⁻¹ z ∈ A
theorem

smul_hasExtension

L172 ↗
RamificationTheory.ValuationSubring.smul_hasExtension
Documentation

A K-algebra automorphic translate of an extension valuation subring is again an extension of the base valuation.

Source context 10 commands

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

namespace RamificationTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.HenselianDVF
noncomputable section
universe u v w z
namespace ValuationSubring
variable {K : Type u} [Field K] (A : ValuationSubring K)
section RestrictIntermediateField
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
open scoped Pointwise
Lean source · statement
theorem smul_hasExtension
    {Γ : Type w} [LinearOrderedCommGroupWithZero Γ]
    (v : Valuation K Γ) (A : ValuationSubring Ω)
    [_root_.Valuation.HasExtension v A.valuation]
    (σ : Ω ≃ₐ[K] Ω) :
    _root_.Valuation.HasExtension v (σ • A).valuation
theorem

restrictIntermediateField_smul_hasExtension

L194 ↗
RamificationTheory.ValuationSubring.restrictIntermediateField_smul_hasExtension
Documentation

Restricting an automorphic translate to an intermediate field preserves the extension property over the base valuation.

Source context 10 commands

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

namespace RamificationTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.HenselianDVF
noncomputable section
universe u v w z
namespace ValuationSubring
variable {K : Type u} [Field K] (A : ValuationSubring K)
section RestrictIntermediateField
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
open scoped Pointwise
Lean source · statement
theorem restrictIntermediateField_smul_hasExtension
    {Γ : Type w} [LinearOrderedCommGroupWithZero Γ]
    (v : Valuation K Γ) (A : ValuationSubring Ω)
    [_root_.Valuation.HasExtension v A.valuation]
    (σ : Ω ≃ₐ[K] Ω) (E : IntermediateField K Ω) :
    _root_.Valuation.HasExtension v ((restrictIntermediateField (σ • A) E)).valuation
theorem

restrictIntermediateField_inv_smul_hasExtension

L207 ↗
RamificationTheory.ValuationSubring.restrictIntermediateField_inv_smul_hasExtension
Documentation

The inverse translate used in absolute Galois stabilization also restricts to an extension of the base valuation.

Source context 10 commands

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

namespace RamificationTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.HenselianDVF
noncomputable section
universe u v w z
namespace ValuationSubring
variable {K : Type u} [Field K] (A : ValuationSubring K)
section RestrictIntermediateField
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
open scoped Pointwise
Lean source · statement
theorem restrictIntermediateField_inv_smul_hasExtension
    {Γ : Type w} [LinearOrderedCommGroupWithZero Γ]
    (v : Valuation K Γ) (A : ValuationSubring Ω)
    [_root_.Valuation.HasExtension v A.valuation]
    (σ : Ω ≃ₐ[K] Ω) (E : IntermediateField K Ω) :
    _root_.Valuation.HasExtension v ((restrictIntermediateField (σ⁻¹ • A) E)).valuation
theorem

restrictIntermediateField_eq_inv_smul_restrictIntermediateField_of_unique

L217 ↗
RamificationTheory.ValuationSubring.restrictIntermediateField_eq_inv_smul_restrictIntermediateField_of_unique
Documentation

Under finite-level uniqueness, the restriction of A is equal to the restriction of its inverse automorphic translate.

Source context 10 commands

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

namespace RamificationTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.HenselianDVF
noncomputable section
universe u v w z
namespace ValuationSubring
variable {K : Type u} [Field K] (A : ValuationSubring K)
section RestrictIntermediateField
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
open scoped Pointwise
Lean source · statement
theorem restrictIntermediateField_eq_inv_smul_restrictIntermediateField_of_unique
    {Γ : Type w} [LinearOrderedCommGroupWithZero Γ]
    (v : Valuation K Γ) (A : ValuationSubring Ω)
    [_root_.Valuation.HasExtension v A.valuation]
    (E : IntermediateField K Ω)
    (huniq :
      ∀ (B : ValuationSubring E)
        [_root_.Valuation.HasExtension v B.valuation],
          (restrictIntermediateField A E) = B)
    (σ : Ω ≃ₐ[K] Ω) :
    (restrictIntermediateField A E) = (restrictIntermediateField (σ⁻¹ • A) E)
theorem

mem_algEquiv_apply_iff_of_restrictIntermediateField_unique

L236 ↗
RamificationTheory.ValuationSubring.mem_algEquiv_apply_iff_of_restrictIntermediateField_unique
Documentation

If the restricted valuation on a finite level is the unique extension of the base valuation, then every ambient K-automorphism preserves membership in the ambient valuation subring on that level.

Source context 10 commands

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

namespace RamificationTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.HenselianDVF
noncomputable section
universe u v w z
namespace ValuationSubring
variable {K : Type u} [Field K] (A : ValuationSubring K)
section RestrictIntermediateField
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
open scoped Pointwise
Lean source · statement
theorem mem_algEquiv_apply_iff_of_restrictIntermediateField_unique
    {Γ : Type w} [LinearOrderedCommGroupWithZero Γ]
    (v : Valuation K Γ) (A : ValuationSubring Ω)
    [_root_.Valuation.HasExtension v A.valuation]
    (E : IntermediateField K Ω)
    (huniq :
      ∀ (B : ValuationSubring E)
        [_root_.Valuation.HasExtension v B.valuation],
          (restrictIntermediateField A E) = B)
    (σ : Ω ≃ₐ[K] Ω) (x : E) :
    ((x : Ω) ∈ A) ↔ σ (x : Ω) ∈ A
theorem

mem_algEquiv_apply_iff_of_restrictIntermediateField_henselianUnique

L273 ↗
RamificationTheory.ValuationSubring.mem_algEquiv_apply_iff_of_restrictIntermediateField_henselianUnique
Documentation

A Henselian-DVF unique-extension package on the finite level supplies the membership preservation core needed for the absolute power route.

Source context 10 commands

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

namespace RamificationTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.HenselianDVF
noncomputable section
universe u v w z
namespace ValuationSubring
variable {K : Type u} [Field K] (A : ValuationSubring K)
section RestrictIntermediateField
variable {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
open scoped Pointwise
Lean source · statement
theorem mem_algEquiv_apply_iff_of_restrictIntermediateField_henselianUnique
    (base : ValuationTheory.DiscreteValuationField.HenselianDVF.{u, w} K)
    (A : ValuationSubring Ω)
    [_root_.Valuation.HasExtension base.valuation A.valuation]
    (E : IntermediateField K Ω)
    (target : ValuationTheory.DiscreteValuationField.HenselianDVF.{v, z} E)
    (hA : target.valuation.valuationSubring = (restrictIntermediateField A E))
    (huniq :
      HasUniqueValuationExtension.{u, w, v, z, v}
        base target)
    (σ : Ω ≃ₐ[K] Ω) (x : E) :
    ((x : Ω) ∈ A) ↔ σ (x : Ω) ∈ A
theorem

exists_finite_separable_intermediate_pow_mem

L308 ↗
RamificationTheory.exists_finite_separable_intermediate_pow_mem
Documentation

A power of an algebraic element lies in a finite separable intermediate field.

This packages the standard reduction through the separable closure: an algebraic extension is purely inseparable over its separable closure, so a positive power of the element lands in the separable closure, and adjoining that power gives the finite separable level.

Source context 5 commands

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

namespace RamificationTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.HenselianDVF
noncomputable section
universe u v w z
Lean source · statement
theorem exists_finite_separable_intermediate_pow_mem
    {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
    [Algebra.IsAlgebraic K Ω] (z : Ω) :
    ∃ n : ℕ, ∃ E : IntermediateField K Ω,
      0 < n ∧ FiniteDimensional K E ∧ Algebra.IsSeparable K E ∧ z ^ n ∈ E
theorem

exists_pow_isSeparable_of_isAlgebraic

L332 ↗
RamificationTheory.exists_pow_isSeparable_of_isAlgebraic
Documentation

A positive power of any algebraic element is separable over the base.

Source context 5 commands

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

namespace RamificationTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.HenselianDVF
noncomputable section
universe u v w z
Lean source · statement
theorem exists_pow_isSeparable_of_isAlgebraic
    {K : Type u} {Ω : Type v} [Field K] [Field Ω] [Algebra K Ω]
    [Algebra.IsAlgebraic K Ω] (z : Ω) :
    ∃ n : ℕ, 0 < n ∧ IsSeparable K (z ^ n)

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