Dehomogenizing a circular chart polynomial
DefinitionEsgk_DistanceNewtonITangentHomogeneousFormalgebracomplex-analysispolynomials
This defines the ring homomorphism that evaluates the homogenizing variable at one and the affine chart variable at the polynomial variable.
Definition code
-- Extracted dependency interfaces and their necessary proofs.
import Definitions.Def_Esgk_PlaneCircularLocalChart
import Mathlib
import Mathlib.RingTheory.MvPolynomial.Homogeneous
/-
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 scoped BigOperators
variable {n : ℕ}
def circularChartDehomogenization : CircularChartPoly →+* Polynomial ℂ :=
MvPolynomial.eval₂Hom (Polynomial.C : ℂ →+* Polynomial ℂ) ![Polynomial.X, 1]
end Esgk