Squared-distance functions on a plane curve field

Definition

Esgk_IrreduciblePlaneAffineIsometryDistanceTransport

by mysticflounder · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometryfunction-fieldsgeometry

This defines the coordinate-ring class and function-field image of squared distance to an arbitrary planar point.

Definition code

-- Extracted dependency interfaces and their necessary proofs.
import Definitions.Def_Esgk_IrreduciblePlaneAffineIsometryTransport
import Definitions.Def_Esgk_IrreduciblePlaneDistanceImageField
import Definitions.Def_Esgk_IrreduciblePlaneFunctionField
import Definitions.Def_Esgk_PlaneAffineIsometryDistancePolynomial
import Definitions.Def_LeanFormalizations_PachDeZeeuw_AlgebraicPrelim
import Mathlib

/-
Copyright (c) 2026 Adam McKenna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam McKenna
-/


noncomputable section

namespace Esgk

open PachDeZeeuw.Algebraic

namespace IrreduciblePlanePolynomial


def squaredDistanceClassAt
    (C : IrreduciblePlanePolynomial ℝ) (a : Point2) : C.CoordinateRing :=
  Ideal.Quotient.mk _ (planeSquaredDistancePolynomial a)


def squaredDistanceFunctionAt
    (C : IrreduciblePlanePolynomial ℝ) (a : Point2) : C.FunctionField :=
  algebraMap C.CoordinateRing C.FunctionField (C.squaredDistanceClassAt a)


end IrreduciblePlanePolynomial

end Esgk

View graph