Real points of an affine normalization

Definition

Esgk_IrreduciblePlaneAffineNormalizationRealEvaluation

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

algebraic-geometryreal-algebraic-geometry

This names normalized real curve points and provides their base and comap maps to the underlying coordinate data.

Definition code

-- Extracted dependency interfaces and their necessary proofs.
import Definitions.Def_Esgk_IrreduciblePlaneAffineNormalization
import Definitions.Def_Esgk_IrreduciblePlaneAffineNormalizationDistanceAction
import Definitions.Def_Esgk_IrreduciblePlaneFunctionField
import Definitions.Def_Esgk_SelfCurveDistancePairs
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

 
abbrev RealAffineNormalizationPoint (C : IrreduciblePlanePolynomial ℝ) :=
  C.affineNormalizationRing →ₐ[ℝ] ℝ

namespace RealAffineNormalizationPoint

 
def basePoint {C : IrreduciblePlanePolynomial ℝ}
    (x : C.RealAffineNormalizationPoint) : Point2 :=
  WithLp.toLp 2 (fun i ↦ x (C.affineNormalizationLift (C.coordinateClass i)))


def comap {C : IrreduciblePlanePolynomial ℝ}
    (x : C.RealAffineNormalizationPoint)
    (E : C.affineNormalizationRing ≃ₐ[ℝ] C.affineNormalizationRing) :
    C.RealAffineNormalizationPoint :=
  x.comp E.toAlgHom


end RealAffineNormalizationPoint

end IrreduciblePlanePolynomial

end Esgk

View graph