structure LocalRingAtPoint (k : Type u_1) [Field k] (K : Type u_2) [Field K] [Algebra k K] : Type u_2

An abstract local ring at a point $P$ of a curve $C/k$ with function field $K = k(C)$: the ring of regular functions $\mathcal{O}_P = \{f \in k(C) : f(P) \neq \infty\}$ presented as a valuation subring of $K$ whose valuation is nontrivial and trivial on the constants $k$ (Definition 23.3).

• toValuationSubring : ValuationSubring K
• valuation_nontrivial : self.toValuationSubring.valuation.IsNontrivial
• valuation_trivial_on_k (a : k) : a ≠ 0 → self.toValuationSubring.valuation ((algebraMap k K) a) = 1

instance LocalRingAtPoint.instIsLocalRing {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] (P : LocalRingAtPoint k K) : IsLocalRing ↥P.toValuationSubring

The local ring at a point is a local ring (it has a unique maximal ideal).

theorem LocalRingAtPoint.instIsPrincipalIdealRing {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] (P : LocalRingAtPoint k K) : IsPrincipalIdealRing ↥P.toValuationSubring

The local ring at a point of a smooth curve is a principal ideal domain (part of Definition 23.3).

noncomputable def LocalRingAtPoint.maximalIdeal {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] (P : LocalRingAtPoint k K) : Ideal ↥P.toValuationSubring

The unique maximal ideal $\mathfrak{m}_P = \{f \in \mathcal{O}_P : f(P) = 0\}$ of the local ring at $P$.

def LocalRingAtPoint.IsUniformizerAt {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] (P : LocalRingAtPoint k K) (u : ↥P.toValuationSubring) : Prop

An element $u \in \mathcal{O}_P$ is a uniformizer at $P$ if it generates the maximal ideal $\mathfrak{m}_P = (u)$ (Definition 23.3).

def LocalRingAtPoint.IsRegularAt {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] (P : LocalRingAtPoint k K) (g : K) : Prop

A rational function $g \in K$ is regular at $P$ if it lies in the local ring $\mathcal{O}_P$.

@[simp]

theorem LocalRingAtPoint.isRegularAt_iff {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] (P : LocalRingAtPoint k K) (g : K) : P.IsRegularAt g ↔ g ∈ P.toValuationSubring

Regularity at $P$ unfolds to membership in the local ring.

theorem LocalRingAtPoint.algebraMap_mem {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] (P : LocalRingAtPoint k K) (a : k) : (algebraMap k K) a ∈ P.toValuationSubring

Constants from $k$ are regular at every point: the image of $k$ lies in $\mathcal{O}_P$.

def IsUniformizer {R : Type u_1} [CommRing R] [IsLocalRing R] (u : R) : Prop

An element $u$ of a local ring is a uniformizer if it generates the maximal ideal.