NYLL
Module

DVRNormalizationComparison.lean

Nyll.EtaleFundamentalGroups.Kummer.SelectedRoot.Exact.DVRNormalizationComparison
1 declaration indexed from sourceView source ↗

Module documentation

DVR normalization comparison at the exact ramification-index root

For the exact ramification-index root, the degree sandwich identifies the input DVR extension field Omega with the strict-stage chosen component field P. Mapping integral closures along that sourced field equivalence identifies the input DVR normalization with the normalization of the original DVR inside P. Since the root ring is integral over the DVR, the integral-base comparison then identifies this normalization with the chosen root factor D.

This is only a height-one DVR coordinate comparison. An Away localization of the displayed DVR is merely its generic fibre, so this theorem deliberately does not claim the height-two boundary Away statement needed by the final chosen-factor terminal. That statement must first be lifted through the height-two finite-etale descent/purity stage.

The integral-closure inputs have concrete producers in the existing chain:

  • exists_etaleChosenLocalFactor_finiteGenericFiberComponent_algEquiv

identifies the actual Tag local factor with a prime localization of the normalization of the selected component. After the standard fraction-ring and integrally-closed localization instances, IsIntegralClosure.of_isIntegrallyClosed supplies its IsIntegralClosure T V Omega instance.

  • higherRadicalUnitFactorData_exists_strictHenselian_localizationAlgEquiv

produces the retained exact-root local factor. Its domain and finite-etale data are supplied by higherRadicalUnitFactorData_isDomain, higherRadicalUnitFactorData_radical_finite, and factor.radical_etale; taking its fraction ring and applying IsIntegralClosure.of_isIntegrallyClosed supplies IsIntegralClosure D B P.

  • lowerUnitFactorHigherBaseChangeFixedComponentRingEquiv and

lowerUnitFactorHigherBaseChangeFixedComponentRingEquiv_root retain that same lower factor and its root coordinate in the later fixed component.

Thus neither integral-closure class is a theorem-shaped comparison assumption. No field equivalence, degree equality, or comparison equality is an input.

Imports2
Imported by1

Declarations

def

selectedExactRamificationRoot_DVRNormalizations_algEquiv

L66 ↗
EtaleFundamentalGroups.Kummer.selectedExactRamificationRoot_DVRNormalizations_algEquiv
Documentation

Compare the two DVR normalizations at the strict exact-root stage.

The returned equivalence is over the literal valuation subring of base. The field equivalence Omega ≃ P is built internally from the exact-root degree sandwich. This theorem is a local coordinate junction, not the height-two boundary-Away terminal.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe uK uV uOmega uW uFroot uT uD uP
Lean source · statement
def
    selectedExactRamificationRoot_DVRNormalizations_algEquiv
    {K : Type uK} {Omega : Type uOmega} {Froot : Type uFroot}
    {T : Type uT} {D : Type uD} {P : Type uP}
    [Field K] [Field Omega] [Field Froot]
    [CommRing T] [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 base.valuationSubring T]
    [Algebra T Omega]
    [IsScalarTower base.valuationSubring T Omega]
    [IsIntegralClosure T base.valuationSubring Omega]
    [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]
    [Algebra base.valuationSubring D]
    [IsScalarTower base.valuationSubring
      (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]
    [IsIntegralClosure D
      (AdjoinRoot
        (X ^ ramificationIndex base target - C varpi)) 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]
    [Algebra base.valuationSubring P]
    [IsScalarTower base.valuationSubring
      (AdjoinRoot
        (X ^ ramificationIndex base target - C varpi)) P]
    [IsScalarTower base.valuationSubring D P]
    [IsScalarTower base.valuationSubring Omega P] :
    T ≃ₐ[base.valuationSubring] D

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