In a local ring with principal maximal ideal, the submodule generated by $du$ does not depend on the generator $u$

Proved

CurveSymmetry.localKaehler_span_congr

by carlok · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

curve-symmetry-leanfunction-fieldskahler-differentials

Let $R$ be a commutative ring and $A$ a commutative local $R$ -algebra with maximal ideal $\mathfrak m$ , such that the module of Kähler differentials $\Omega_{A/R}$ is finitely generated over $A$ ; let $d\colon A\to\Omega_{A/R}$ be the universal derivation. Assume that every element of $A$ is congruent modulo $\mathfrak m$ to the image of an element of $R$ , that is, $R\to A/\mathfrak m$ is surjective. If $u,u'\in A$ both generate $\mathfrak m$ , that is, $\mathfrak m=(u)=(u')$ , then

A\,du=A\,du'\qquad\text{in }\Omega_{A/R}.

At a place of a function field, the order of a differential is measured against $du$ for a uniformizer $u$ ; this statement shows that the submodule generated by $du$ does not depend on that choice. It is applied to the local rings at the places of the double cover (7), toward the genus in Lemma 4.

Preamble

import Definitions.Def_CurveSymmetry_08_Differentials
import Mathlib.RingTheory.Etale.Kaehler
import Mathlib.RingTheory.Kaehler.Basic
import Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
import Mathlib.RingTheory.LocalRing.Module
import Mathlib.RingTheory.Nakayama

open CurveSymmetry
set_option autoImplicit false
variable {R A : Type*} [CommRing R] [CommRing A] [Algebra R A] [IsLocalRing A]
  [Module.Finite A Ω[A⁄R]]

Formal statement

theorem CurveSymmetry.localKaehler_span_congr {u u' : A}
    (hres : ∀ x : A, ∃ r : R, x - algebraMap R A r ∈ IsLocalRing.maximalIdeal A)
    (hu : IsLocalRing.maximalIdeal A = Ideal.span {u})
    (hu' : IsLocalRing.maximalIdeal A = Ideal.span {u'}) :
    Submodule.span A {KaehlerDifferential.D R A u} =
      Submodule.span A {KaehlerDifferential.D R A u'} := by sorry

Source

C. Perassi, Sharp symmetry bounds for real algebraic curves (note): lemma of the formalization, for Lemma 4, pp. 3-4, https://github.com/carlok/curve-symmetry-lean/blob/d99bc17a1c397956c05d7417de50f9beed56580f/sharp_symmetry_bounds.pdf. Lean: https://github.com/carlok/curve-symmetry-lean/blob/d99bc17a1c397956c05d7417de50f9beed56580f/lean/LocalDifferentials.lean (C. Perassi)

View graph

In a local ring with principal maximal ideal, the submodule generated by dududu does not depend on the generator uuu

In a local ring with principal maximal ideal, the submodule generated by $du$ does not depend on the generator $u$