NYLL
Module

StandardDVF.lean

Nyll.EtaleFundamentalGroups.LocalGeometry.HeightOne.StandardDVF
6 declarations indexed from sourceView source ↗

Module documentation

The standard discrete valuation field attached to a DVR

A discrete valuation ring inside a chosen fraction field determines the adic rank-one discrete valuation of that field. This file packages that valuation as a DVF, transports a local map of DVRs to an extension of the packaged valuations, and compares the resulting DVF ramification index with the original ideal-theoretic ramification index.

Imports3
Imported by6

Declarations

def

standardDVFOfDVR

L32 ↗
EtaleFundamentalGroups.standardDVFOfDVR
Documentation

The rank-one discrete valuation field canonically attached to a DVR and a chosen fraction field.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe uV uW uK uL
Lean source · full declaration
def standardDVFOfDVR
    (V : Type uV) (K : Type uK)
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K] :
    DVF.{uK, 0} K where
  ValueGroup := WithZero (Multiplicative ℤ)
  valuation := (IsDiscreteValuationRing.maximalIdeal V).valuation K
theorem

valuation_hasExtension_of_local_valuationSubring_map

L42 ↗
EtaleFundamentalGroups.valuation_hasExtension_of_local_valuationSubring_map
Documentation

A local map between valuation subrings which agrees with the ambient field map determines an extension of the two valuations.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe uV uW uK uL
Lean source · statement
theorem valuation_hasExtension_of_local_valuationSubring_map
    {K : Type uK} {L : Type uL} [Field K] [Field L] [Algebra K L]
    (base : DVF.{uK, uV} K) (target : DVF.{uL, uW} L)
    (f : base.valuationSubring →+* target.valuationSubring)
    [IsLocalHom f]
    (hcoe : ∀ z : base.valuationSubring,
      ((f z : target.valuationSubring) : L) =
        algebraMap K L (z : K)) :
    base.valuation.HasExtension target.valuation
theorem

standardDVFOfDVR_hasExtension

L107 ↗
EtaleFundamentalGroups.standardDVFOfDVR_hasExtension
Documentation

A local map of DVRs which induces the prescribed map of fraction fields produces an extension between their standard rank-one discrete valuations.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe uV uW uK uL
Lean source · statement
theorem standardDVFOfDVR_hasExtension
    {V : Type uV} {W : Type uW} {K : Type uK} {L : Type uL}
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [CommRing W] [IsDomain W] [IsDiscreteValuationRing W]
    [Field K] [Algebra V K] [IsFractionRing V K]
    [Field L] [Algebra W L] [IsFractionRing W L]
    [Algebra K L]
    (f : V →+* W) [IsLocalHom f]
    (hcomm : (algebraMap W L).comp f =
      (algebraMap K L).comp (algebraMap V K)) :
    (standardDVFOfDVR V K).valuation.HasExtension
      (standardDVFOfDVR W L).valuation
theorem

map_maximalIdeal_ringEquiv

L152 ↗
EtaleFundamentalGroups.map_maximalIdeal_ringEquiv
Documentation

A ring equivalence carries the maximal ideal of one local ring to the maximal ideal of the other.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe uV uW uK uL
Lean source · statement
theorem map_maximalIdeal_ringEquiv
    {R S : Type*} [CommRing R] [CommRing S]
    [IsLocalRing R] [IsLocalRing S] (e : R ≃+* S) :
    Ideal.map e (IsLocalRing.maximalIdeal R) =
      IsLocalRing.maximalIdeal S
theorem

ramificationIdx'_eq_of_map_eq

L172 ↗
EtaleFundamentalGroups.ramificationIdx'_eq_of_map_eq
Documentation

Ramification indices agree when the two source ideals have the same image in the target ring.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe uV uW uK uL
Lean source · full declaration
theorem ramificationIdx'_eq_of_map_eq
    {R R' S : Type*} [CommRing R] [CommRing R'] [CommRing S]
    (f : R →+* S) (g : R' →+* S)
    (p : Ideal R) (q : Ideal R') (P : Ideal S)
    (h : Ideal.map f p = Ideal.map g q) :
    letI : Algebra R S := f.toAlgebra
    letI : Algebra R' S := g.toAlgebra
    Ideal.ramificationIdx' p P = Ideal.ramificationIdx' q P := by
  unfold Ideal.ramificationIdx'
  change sSup {n | Ideal.map f p ≤ P ^ n} =
    sSup {n | Ideal.map g q ≤ P ^ n}
  rw [h]
theorem

standardDVFOfDVR_ramificationIndex_eq_ramificationIdx

L187 ↗
EtaleFundamentalGroups.standardDVFOfDVR_ramificationIndex_eq_ramificationIdx
Documentation

The ramification index of the standard DVF packages is the ideal-theoretic ramification index of the original local map of DVRs.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe uV uW uK uL
Lean source · full declaration
theorem standardDVFOfDVR_ramificationIndex_eq_ramificationIdx
    {V : Type uV} {W : Type uW} {K : Type uK} {L : Type uL}
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [CommRing W] [IsDomain W] [IsDiscreteValuationRing W]
    [Field K] [Algebra V K] [IsFractionRing V K]
    [Field L] [Algebra W L] [IsFractionRing W L]
    [Algebra K L] [FiniteDimensional K L]
    [Algebra V W] [IsLocalHom (algebraMap V W)]
    (hcomm : (algebraMap W L).comp (algebraMap V W) =
      (algebraMap K L).comp (algebraMap V K)) :
    let base := standardDVFOfDVR V K
    let target := standardDVFOfDVR W L
    letI : base.valuation.HasExtension target.valuation :=
      standardDVFOfDVR_hasExtension (algebraMap V W) hcomm
    ramificationIndex base target =
      (IsLocalRing.maximalIdeal W).ramificationIdx V := by
  dsimp only
  let base := standardDVFOfDVR V K
  let target := standardDVFOfDVR W L
  let hExt : base.valuation.HasExtension target.valuation :=
    standardDVFOfDVR_hasExtension (algebraMap V W) hcomm
  let : base.valuation.HasExtension target.valuation := hExt
  let eV : V ≃+* base.valuationSubring :=
    IsDiscreteValuationRing.equivValuationSubring (A := V) (K := K)
  let eW : W ≃+* target.valuationSubring :=
    IsDiscreteValuationRing.equivValuationSubring (A := W) (K := L)
  let iCan : base.valuationSubring →+* target.valuationSubring :=
    algebraMap base.valuationSubring target.valuationSubring
  let g : V →+* target.valuationSubring := iCan.comp eV.toRingHom
  let : Algebra V target.valuationSubring := g.toAlgebra
  let eWAlg : W ≃ₐ[V] target.valuationSubring :=
    AlgEquiv.ofRingEquiv (f := eW) (by
      intro a
      apply Subtype.ext
      change algebraMap W L (algebraMap V W a) =
        algebraMap K L (algebraMap V K a)
      exact DFunLike.congr_fun hcomm a)
  have htransport :=
    Ideal.ramificationIdx'_map_eq
      (IsLocalRing.maximalIdeal V) (IsLocalRing.maximalIdeal W) eWAlg
  change Ideal.ramificationIdx' (IsLocalRing.maximalIdeal V)
        (Ideal.map eW (IsLocalRing.maximalIdeal W)) =
      Ideal.ramificationIdx' (IsLocalRing.maximalIdeal V)
        (IsLocalRing.maximalIdeal W) at htransport
  have hMaxW : Ideal.map eW (IsLocalRing.maximalIdeal W) =
      target.maximalIdeal :=
    map_maximalIdeal_ringEquiv eW
  rw [hMaxW] at htransport
  have hMaxV : Ideal.map eV (IsLocalRing.maximalIdeal V) =
      base.maximalIdeal :=
    map_maximalIdeal_ringEquiv eV
  have hMap : Ideal.map g (IsLocalRing.maximalIdeal V) =
      Ideal.map iCan base.maximalIdeal := by
    calc
      Ideal.map g (IsLocalRing.maximalIdeal V) =
          Ideal.map (iCan.comp eV.toRingHom)
            (IsLocalRing.maximalIdeal V) := rfl
      _ = Ideal.map iCan
            (Ideal.map eV (IsLocalRing.maximalIdeal V)) := by
            exact (Ideal.map_map eV.toRingHom iCan).symm
      _ = Ideal.map iCan base.maximalIdeal := by rw [hMaxV]
  have hOld :
      Ideal.ramificationIdx' (IsLocalRing.maximalIdeal V)
          (IsLocalRing.maximalIdeal W) =
        ramificationIndex base target := by
    calc
      Ideal.ramificationIdx' (IsLocalRing.maximalIdeal V)
          (IsLocalRing.maximalIdeal W) =
          Ideal.ramificationIdx' (IsLocalRing.maximalIdeal V)
            target.maximalIdeal := htransport.symm
      _ = Ideal.ramificationIdx' base.maximalIdeal target.maximalIdeal :=
        ramificationIdx'_eq_of_map_eq g iCan
          (IsLocalRing.maximalIdeal V) base.maximalIdeal
          target.maximalIdeal hMap
      _ = ramificationIndex base target := rfl
  have hf : Function.Injective (algebraMap V W) := by
    intro a b hab
    apply IsFractionRing.injective V K
    apply (algebraMap K L).injective
    have ha := DFunLike.congr_fun hcomm a
    have hb := DFunLike.congr_fun hcomm b
    change algebraMap W L (algebraMap V W a) =
      algebraMap K L (algebraMap V K a) at ha
    change algebraMap W L (algebraMap V W b) =
      algebraMap K L (algebraMap V K b) at hb
    exact ha.symm.trans ((congrArg (algebraMap W L) hab).trans hb)
  have hMaxVNe : IsLocalRing.maximalIdeal V ≠ ⊥ := by
    simpa [ne_eq, ← IsLocalRing.isField_iff_maximalIdeal_eq] using
      (IsDiscreteValuationRing.not_isField V)
  have hMapMaxNe :
      Ideal.map (algebraMap V W) (IsLocalRing.maximalIdeal V) ≠ ⊥ :=
    (Ideal.map_eq_bot_iff_of_injective hf).not.mpr hMaxVNe
  let : (IsLocalRing.maximalIdeal W).LiesOver
      (IsLocalRing.maximalIdeal V) :=
    ⟨(IsLocalRing.maximalIdeal_comap (algebraMap V W)).symm⟩
  let : (IsLocalRing.maximalIdeal W).IsPrime :=
    (IsLocalRing.maximalIdeal.isMaximal W).isPrime
  let : IsDedekindDomain W := inferInstance
  rw [← hOld]
  exact Ideal.ramificationIdx'_eq_ramificationIdx'
    (IsLocalRing.maximalIdeal V) (IsLocalRing.maximalIdeal W) hMapMaxNe

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