NYLL
Module

DegreeSandwich.lean

Nyll.EtaleFundamentalGroups.Kummer.SelectedRoot.Exact.DegreeSandwich
4 declarations indexed from sourceView source ↗

Module documentation

The degree sandwich for an exact ramification-index root

Let Omega / K be a finite extension of discretely valued fields with ramification index e, and let Froot be the fraction field of the integral root ring V[X] / (X ^ e - varpi). The latter has degree exactly e over K. If a common overfield P is the fraction field of a uniquely chosen finite etale factor over the strictly Henselian root ring, then strict Henselianity identifies P with Froot. The inclusions

e <= [Omega : K] <= [P : K] = [Froot : K] = e

therefore force the literal right algebra map Omega -> P to be bijective.

The exponent in this file is definitionally ramificationIndex base target. In particular, specializing after an earlier root extension still requires a separate source theorem identifying that new local ramification index; no such comparison is accepted as an input here.

Imports3
Imported by4

Declarations

theorem

pureRadicalFractionField_finrank_eq_exponent

L49 ↗
EtaleFundamentalGroups.Kummer.pureRadicalFractionField_finrank_eq_exponent
Documentation

The fraction field of the integral root ring V[X] / (X ^ N - varpi) has degree exactly N over Frac(V).

Both the finite-dimensionality and the degree computation use the canonical generic-fibre equivalence, so the statement preserves the specified fraction-field and scalar-tower maps.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe uK uV uOmega uW uFroot uD uP
Lean source · statement
theorem pureRadicalFractionField_finrank_eq_exponent
    {V : Type uK} {K : Type uK} {F : Type uFroot}
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Field F]
    [Algebra V K] [IsFractionRing V K]
    [Algebra K F]
    {N : ℕ} (hN : 0 < N) (varpi : V) (hvarpi : Prime varpi)
    [Algebra (AdjoinRoot (X ^ N - C varpi)) F]
    [IsFractionRing (AdjoinRoot (X ^ N - C varpi)) F]
    [Algebra V F]
    [IsScalarTower V (AdjoinRoot (X ^ N - C varpi)) F]
    [IsScalarTower V K F] :
    Module.finrank K F = N
theorem

finiteDimensional_of_finite_valuationSubrings_degreeSandwich

L88 ↗
EtaleFundamentalGroups.Kummer.finiteDimensional_of_finite_valuationSubrings_degreeSandwich
Documentation

Finiteness of the valuation-subring extension supplies finiteness of its canonical generic fibre.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe uK uV uOmega uW uFroot uD uP
Lean source · statement
theorem finiteDimensional_of_finite_valuationSubrings_degreeSandwich
    {K : Type uK} {Omega : Type uOmega}
    [Field K] [Field Omega] [Algebra K Omega]
    (base : DVF.{uK, uV} K) (target : DVF.{uOmega, uW} Omega)
    [base.valuation.HasExtension target.valuation]
    [Module.Finite base.valuationSubring target.valuationSubring] :
    FiniteDimensional K Omega
theorem

ramificationIndex_le_finrank_of_moduleFinite

L106 ↗
EtaleFundamentalGroups.Kummer.ramificationIndex_le_finrank_of_moduleFinite
Documentation

The ideal-theoretic ramification index of a finite extension of DVRs is bounded by the degree of its canonical generic fibre.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe uK uV uOmega uW uFroot uD uP
Lean source · statement
theorem ramificationIndex_le_finrank_of_moduleFinite
    {K : Type uK} {Omega : Type uOmega}
    [Field K] [Field Omega] [Algebra K Omega]
    (base : DVF.{uK, uV} K) (target : DVF.{uOmega, uW} Omega)
    [base.valuation.HasExtension target.valuation]
    [Module.Finite base.valuationSubring target.valuationSubring] :
    ramificationIndex base target ≤ Module.finrank K Omega
theorem

selectedExactRamificationRoot_rightAlgebraMap_bijective_of_strictHenselianChosenFactor

L138 ↗
EtaleFundamentalGroups.Kummer.selectedExactRamificationRoot_rightAlgebraMap_bijective_of_strictHenselianChosenFactor
Documentation

Exact-degree selected-root sandwich.

The finite etale factor D, its chosen prime q, and uniqueness over the closed point are precisely the data produced by the local-purity chosen-factor stage. Strict Henselian splitting is used internally to identify its fraction field P with the radical fraction field Froot; neither that field equivalence nor any degree equality is an input.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe uK uV uOmega uW uFroot uD uP
Lean source · statement
theorem
    selectedExactRamificationRoot_rightAlgebraMap_bijective_of_strictHenselianChosenFactor
    {K : Type uK} {Omega : Type uOmega} {Froot : Type uFroot}
    {D : Type uD} {P : Type uP}
    [Field K] [Field Omega] [Field Froot]
    [CommRing D] [Field P]
    [Algebra K Omega]
    (base : DVF.{uK, uV} K) (target : DVF.{uOmega, uW} Omega)
    [base.valuation.HasExtension target.valuation]
    [Module.Finite base.valuationSubring target.valuationSubring]
    (varpi : base.valuationSubring)
    (hvarpi : base.valuation.IsUniformizer (varpi : K))
    [Algebra K Froot]
    [Algebra
      (AdjoinRoot
        (X ^ ramificationIndex base target - C varpi)) Froot]
    [IsFractionRing
      (AdjoinRoot
        (X ^ ramificationIndex base target - C varpi)) Froot]
    [Algebra base.valuationSubring Froot]
    [IsScalarTower base.valuationSubring
      (AdjoinRoot
        (X ^ ramificationIndex base target - C varpi)) Froot]
    [IsScalarTower base.valuationSubring K Froot]
    [HenselianLocalRing
      (AdjoinRoot
        (X ^ ramificationIndex base target - C varpi))]
    [IsSepClosed
      (IsLocalRing.ResidueField
        (AdjoinRoot
          (X ^ ramificationIndex base target - C varpi)))]
    [Algebra
      (AdjoinRoot
        (X ^ ramificationIndex base target - C varpi)) D]
    [Module.Finite
      (AdjoinRoot
        (X ^ ramificationIndex base target - C varpi)) D]
    [Algebra.Etale
      (AdjoinRoot
        (X ^ ramificationIndex base target - C varpi)) D]
    (q : Ideal D) [q.IsPrime]
    [q.LiesOver
      (IsLocalRing.maximalIdeal
        (AdjoinRoot
          (X ^ ramificationIndex base target - C varpi)))]
    (hunique : ∀ Q : Ideal D, Q.IsPrime →
      Q.LiesOver
        (IsLocalRing.maximalIdeal
          (AdjoinRoot
            (X ^ ramificationIndex base target - C varpi))) →
      Q = q)
    [Algebra D P] [IsFractionRing D P]
    [Algebra
      (AdjoinRoot
        (X ^ ramificationIndex base target - C varpi)) P]
    [IsScalarTower
      (AdjoinRoot
        (X ^ ramificationIndex base target - C varpi)) D P]
    [Algebra Froot P]
    [IsScalarTower
      (AdjoinRoot
        (X ^ ramificationIndex base target - C varpi)) Froot P]
    [Algebra K P] [Algebra Omega P]
    [IsScalarTower K Froot P] [IsScalarTower K Omega P] :
    Function.Bijective (algebraMap Omega P)

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