A residue-field section in the adic completion of the retained DVR

Let V be a commutative local E-algebra and let K be its residue field. If K/E is separable, formal etaleness gives a unique coefficient section in every positive quotient V / m^(n+1). Uniqueness makes those sections compatible with the quotient transition maps. This file assembles the compatible family in Mathlib's m-adic completion and proves that the level-one residue map retracts it.

The retained DVR produced by RelativeCoefficientDVRPlace satisfies the separability hypothesis in characteristic zero, so the construction applies to it directly. No equivalence with a power-series ring is asserted.

@[reducible, inline]

abbrev Stafford38.Geometry.CompletedDVRCoefficientSection.ResidueFieldModel (V : Type u) [CommRing V] [IsLocalRing V] : Type u

The residue field of the local ring.

Equations

• Stafford38.Geometry.CompletedDVRCoefficientSection.ResidueFieldModel V = IsLocalRing.ResidueField V

@[reducible, inline]

abbrev Stafford38.Geometry.CompletedDVRCoefficientSection.maximalIdealModel (V : Type u) [CommRing V] [IsLocalRing V] : Ideal V

The maximal ideal defining the adic filtration.

Equations

• Stafford38.Geometry.CompletedDVRCoefficientSection.maximalIdealModel V = IsLocalRing.maximalIdeal V

@[reducible, inline]

abbrev Stafford38.Geometry.CompletedDVRCoefficientSection.AdicJet (V : Type u) [CommRing V] [IsLocalRing V] (n : ℕ) : Type u

The positive n-th nilpotent quotient of the local ring.

Equations

• Stafford38.Geometry.CompletedDVRCoefficientSection.AdicJet V n = (V ⧸ Stafford38.Geometry.CompletedDVRCoefficientSection.maximalIdealModel V ^ (n + 1))

noncomputable def Stafford38.Geometry.CompletedDVRCoefficientSection.adicJetResidue (E V : Type u) [Field E] [CommRing V] [IsLocalRing V] [Algebra E V] (n : ℕ) : AdicJet V n →ₐ[E] ResidueFieldModel V

Reduction of a positive adic jet to the residue field.

Equations

• One or more equations did not get rendered due to their size.

theorem Stafford38.Geometry.CompletedDVRCoefficientSection.adicJetResidue_surjective (E V : Type u) [Field E] [CommRing V] [IsLocalRing V] [Algebra E V] (n : ℕ) : Function.Surjective ⇑(adicJetResidue E V n)

Reduction from every positive adic jet is surjective.

theorem Stafford38.Geometry.CompletedDVRCoefficientSection.adicJetResidue_kernel_isNilpotent (E V : Type u) [Field E] [CommRing V] [IsLocalRing V] [Algebra E V] (n : ℕ) : IsNilpotent (RingHom.ker (adicJetResidue E V n).toRingHom)

The kernel of positive-jet reduction is nilpotent.

noncomputable def Stafford38.Geometry.CompletedDVRCoefficientSection.adicJetCoefficientSection (E V : Type u) [Field E] [CommRing V] [IsLocalRing V] [Algebra E V] (hsep : Algebra.IsSeparable E (ResidueFieldModel V)) (n : ℕ) : ResidueFieldModel V →ₐ[E] AdicJet V n

The unique coefficient section in the positive n-th adic jet.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Stafford38.Geometry.CompletedDVRCoefficientSection.adicJetResidue_comp_adicJetCoefficientSection (E V : Type u) [Field E] [CommRing V] [IsLocalRing V] [Algebra E V] (hsep : Algebra.IsSeparable E (ResidueFieldModel V)) (n : ℕ) : (adicJetResidue E V n).comp (adicJetCoefficientSection E V hsep n) = AlgHom.id E (ResidueFieldModel V)

Each finite-level coefficient map is a section of reduction.

def Stafford38.Geometry.CompletedDVRCoefficientSection.adicJetTransition (E V : Type u) [Field E] [CommRing V] [IsLocalRing V] [Algebra E V] {a b : ℕ} (hab : a ≤ b) : AdicJet V b →ₐ[E] AdicJet V a

The transition map between two positive adic jets.

Equations

• One or more equations did not get rendered due to their size.

theorem Stafford38.Geometry.CompletedDVRCoefficientSection.adicJetResidue_comp_transition (E V : Type u) [Field E] [CommRing V] [IsLocalRing V] [Algebra E V] {a b : ℕ} (hab : a ≤ b) : (adicJetResidue E V a).comp (adicJetTransition E V hab) = adicJetResidue E V b

Reduction commutes with every positive-jet transition.

theorem Stafford38.Geometry.CompletedDVRCoefficientSection.adicJetCoefficientSection_compatible (E V : Type u) [Field E] [CommRing V] [IsLocalRing V] [Algebra E V] (hsep : Algebra.IsSeparable E (ResidueFieldModel V)) {a b : ℕ} (hab : a ≤ b) : (adicJetTransition E V hab).comp (adicJetCoefficientSection E V hsep b) = adicJetCoefficientSection E V hsep a

Uniqueness forces the positive finite-level sections to be compatible.

def Stafford38.Geometry.CompletedDVRCoefficientSection.exactQuotientToCompletionCoordinate (E V : Type u) [Field E] [CommRing V] [IsLocalRing V] [Algebra E V] (n : ℕ) : (V ⧸ maximalIdealModel V ^ n) ≃ₐ[E] V ⧸ maximalIdealModel V ^ n • ⊤

Convert the usual quotient by maximalIdealModel^n to the coordinate quotient used in the definition of AdicCompletion.

Equations

• Stafford38.Geometry.CompletedDVRCoefficientSection.exactQuotientToCompletionCoordinate E V n = AlgEquiv.restrictScalars E (Ideal.quotientEquivAlgOfEq V ⋯).symm

def Stafford38.Geometry.CompletedDVRCoefficientSection.zeroCompletionCoordinateSection (E V : Type u) [Field E] [CommRing V] [IsLocalRing V] [Algebra E V] : ResidueFieldModel V →ₐ[E] V ⧸ maximalIdealModel V ^ 0 • ⊤

The zeroth completion coordinate is the zero quotient, so it has a unique E-algebra map from the residue field.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Stafford38.Geometry.CompletedDVRCoefficientSection.completionCoordinateSection (E V : Type u) [Field E] [CommRing V] [IsLocalRing V] [Algebra E V] (hsep : Algebra.IsSeparable E (ResidueFieldModel V)) (n : ℕ) : ResidueFieldModel V →ₐ[E] V ⧸ maximalIdealModel V ^ n • ⊤

The coefficient section in every coordinate of Mathlib's adic inverse limit. Coordinate zero is trivial; coordinate n+1 is the formally etale section in V / maximalIdealModel^(n+1).

Equations

• One or more equations did not get rendered due to their size.
• Stafford38.Geometry.CompletedDVRCoefficientSection.completionCoordinateSection E V hsep 0 = Stafford38.Geometry.CompletedDVRCoefficientSection.zeroCompletionCoordinateSection E V

theorem Stafford38.Geometry.CompletedDVRCoefficientSection.completionCoordinateSection_compatible (E V : Type u) [Field E] [CommRing V] [IsLocalRing V] [Algebra E V] (hsep : Algebra.IsSeparable E (ResidueFieldModel V)) {a b : ℕ} (hab : a ≤ b) (x : ResidueFieldModel V) : (AdicCompletion.transitionMap (maximalIdealModel V) V hab) ((completionCoordinateSection E V hsep b) x) = (completionCoordinateSection E V hsep a) x

The completion-coordinate sections form a compatible inverse-limit family.

noncomputable def Stafford38.Geometry.CompletedDVRCoefficientSection.completedCoefficientSection (E V : Type u) [Field E] [CommRing V] [IsLocalRing V] [Algebra E V] (hsep : Algebra.IsSeparable E (ResidueFieldModel V)) : ResidueFieldModel V →ₐ[E] AdicCompletion (maximalIdealModel V) V

The compatible finite-level sections assemble to an actual E-algebra coefficient section in the adic completion.

Equations

• One or more equations did not get rendered due to their size.

theorem Stafford38.Geometry.CompletedDVRCoefficientSection.eval_completedCoefficientSection (E V : Type u) [Field E] [CommRing V] [IsLocalRing V] [Algebra E V] (hsep : Algebra.IsSeparable E (ResidueFieldModel V)) (n : ℕ) : (AlgHom.restrictScalars E (AdicCompletion.evalₐ (maximalIdealModel V) (n + 1))).comp (completedCoefficientSection E V hsep) = adicJetCoefficientSection E V hsep n

Evaluation of the completed section at every positive level recovers the finite-level section constructed by formal etaleness.

noncomputable def Stafford38.Geometry.CompletedDVRCoefficientSection.completedResidue (E V : Type u) [Field E] [CommRing V] [IsLocalRing V] [Algebra E V] : AdicCompletion (maximalIdealModel V) V →ₐ[E] ResidueFieldModel V

Residue specialization of the completion is evaluation modulo maximalIdealModel, followed by the ordinary residue map.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Stafford38.Geometry.CompletedDVRCoefficientSection.completedResidue_comp_completedCoefficientSection (E V : Type u) [Field E] [CommRing V] [IsLocalRing V] [Algebra E V] (hsep : Algebra.IsSeparable E (ResidueFieldModel V)) : (completedResidue E V).comp (completedCoefficientSection E V hsep) = AlgHom.id E (ResidueFieldModel V)

The adic-completion coefficient map is an actual section of residue.

@[reducible, inline]

abbrev Stafford38.Geometry.CompletedDVRCoefficientSection.SourceDVR (E : Type u) [Field E] : Type u

The coordinate-zero discrete valuation ring used for retained places.

Equations

• Stafford38.Geometry.CompletedDVRCoefficientSection.SourceDVR E = Stafford38.Geometry.AsymptoticDivisorExistence.CoordinateZeroLocalRing E

noncomputable def Stafford38.Geometry.CompletedDVRCoefficientSection.retainedCompletedCoefficientSection (E : Type u) [Field E] [CharZero E] {L : Type u} [Field L] [Algebra (SourceDVR E) L] {a : SourceDVR E} (D : RetainedDVR.RetainedDVRPlace (SourceDVR E) a) : IsLocalRing.ResidueField ↥D.valuation.toSubring →ₐ[E] AdicCompletion (IsLocalRing.maximalIdeal ↥D.valuation.toSubring) ↥D.valuation.toSubring

The actual residue-field coefficient section in the maximal-ideal adic completion of a retained DVR place.

Equations

• One or more equations did not get rendered due to their size.

theorem Stafford38.Geometry.CompletedDVRCoefficientSection.retainedCompletedCoefficientSection_isSection (E : Type u) [Field E] [CharZero E] {L : Type u} [Field L] [Algebra (SourceDVR E) L] {a : SourceDVR E} (D : RetainedDVR.RetainedDVRPlace (SourceDVR E) a) : (completedResidue E ↥D.valuation.toSubring).comp (retainedCompletedCoefficientSection E D) = AlgHom.id E (IsLocalRing.ResidueField ↥D.valuation.toSubring)

The retained completed coefficient section is split by completed residue specialization.