NYLL
Module

StandardDVFResidue.lean

Nyll.EtaleFundamentalGroups.LocalGeometry.HeightOne.StandardDVFResidue
1 declaration indexed from sourceView source ↗

Module documentation

Residue characteristic of the standard DVR valuation

The standard discrete valuation attached to a DVR uses a valuation subring canonically equivalent to the original DVR. This file descends that ring equivalence to the closed-point quotients. In particular, characteristic zero of the original DVR residue ring supplies characteristic zero of the DVF residue field required by the higher-radical factor construction.

Imports2
Imported by3

Declarations

theorem

charZero_standardDVFOfDVR_residueField

L30 ↗
EtaleFundamentalGroups.charZero_standardDVFOfDVR_residueField
Documentation

Characteristic zero of a DVR's closed-point quotient is preserved by the standard DVF package attached to a chosen fraction field.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open ValuationTheory.DiscreteValuationField
universe uV uK
Lean source · statement
theorem charZero_standardDVFOfDVR_residueField
    {V : Type uV} {K : Type uK}
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Algebra V K] [IsFractionRing V K]
    (hCharZero : CharZero (V ⧸ IsLocalRing.maximalIdeal V)) :
    CharZero (standardDVFOfDVR V K).residueField

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