Prove2Me

Multiplicity conditions at both circular points

Definition
Esgk_RadialFiltrationCircularMultiplicity

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

algebraic-geometrygeometry

This defines a lower bound on circular multiplicity by requiring the two local chart polynomials of a chosen homogenization to lie in a specified power of the ideal generated by the chart variables.

Definition code
-- Extracted dependency interfaces and their necessary proofs.
import Definitions.Def_Esgk_PlaneCircularLocalChart
import Definitions.Def_Esgk_PlaneProjectiveHomogenization
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


def HasCircularMultiplicityAtLeast (D m : ℕ) (f : PlanePoly) : Prop :=
  projectiveCircularChartI (planeHomogenization D f) ∈
      MvPolynomial.idealOfVars (Fin 2) ℂ ^ m ∧
    projectiveCircularChartJ (planeHomogenization D f) ∈
      MvPolynomial.idealOfVars (Fin 2) ℂ ^ m


end Esgk

View graph