A sample lifted to the regular curve locus
DefinitionEsgk_PlaneCurveSafeSamplealgebraic-geometrygeometry
This removes singular and radial-critical points from a finite sample and lifts the remaining points that lie on the curve to its regular-locus subtype.
Definition code
-- Extracted dependency interfaces and their necessary proofs.
import Definitions.Def_Esgk_PlaneCurveExceptionalSample
import Definitions.Def_Esgk_PlaneCurveRegularChart
import Definitions.Def_LeanFormalizations_PachDeZeeuw_AlgebraicPrelim
import Definitions.Def_LeanFormalizations_PachDeZeeuw_CurveInterface
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
open Set MvPolynomial
open scoped Classical
open PachDeZeeuw.Algebraic hiding Point2
namespace Esgk
def planeCurveSafeSample (G : PlanePoly) (o : Point2) (S : Finset Point2) :
Finset (planeCurveRegularLocus G) :=
(S \ planeCurveExceptionalSample G o S).preimage Subtype.val Subtype.val_injective.injOn
end Esgk