Nyll.EtaleFundamentalGroups.Inertia.Residue.TrivialRamificationDegree

Module documentation

Ramification degree with trivial residue extension

For a finite local extension of discrete valuation rings, a bijection on residue fields forces the inertia degree to be one. The local Dedekind identity e * f = [L : K] then identifies the ramification index with the degree of the fraction-field extension.

theorem

maximalIdeal_ramificationIdx_eq_finrank_of_residueFieldMap_bijective

L29 ↗

EtaleFundamentalGroups.maximalIdeal_ramificationIdx_eq_finrank_of_residueFieldMap_bijective

Documentation

A finite local extension of DVRs inducing an isomorphism on residue fields has ramification index equal to its generic degree.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uS uK uL

Lean source · statement

theorem maximalIdeal_ramificationIdx_eq_finrank_of_residueFieldMap_bijective
    {R : Type uR} {S : Type uS} {K : Type uK} {L : Type uL}
    [CommRing R] [CommRing S] [IsDomain R] [IsDomain S]
    [IsDiscreteValuationRing R] [IsDiscreteValuationRing S]
    [Algebra R S] [IsLocalHom (algebraMap R S)]
    [Field K] [Field L]
    [Algebra R K] [IsFractionRing R K]
    [Algebra S L] [IsFractionRing S L]
    [Algebra K L] [Algebra R L]
    [IsScalarTower R S L] [IsScalarTower R K L]
    [Module.Finite R S]
    (hres : Function.Bijective
      (IsLocalRing.ResidueField.map (algebraMap R S))) :
    (IsLocalRing.maximalIdeal S).ramificationIdx R =
      Module.finrank K L

Module documentation

Ramification degree with trivial residue extension

Declarations

maximalIdeal_ramificationIdx_eq_finrank_of_residueFieldMap_bijective