noncomputable def Lec5BezoutPascal.dehomogenize₀ (k : Type u_1) [Field k] : MvPolynomial (Fin 3) k →ₐ[k] MvPolynomial (Fin 2) k

Dehomogenization with respect to the 0th coordinate: substitutes x₀ = 1 in a homogeneous polynomial in three variables to land in the affine chart k[x₁, x₂].

noncomputable def Lec5BezoutPascal.affinePoint₀ (k : Type u_1) [Field k] (p : P2 k) (h₀ : Projectivization.rep p 0 ≠ 0) : Fin 2 → k

The affine coordinates of a projective point p in the 0th affine chart x₀ ≠ 0, obtained by dividing by the 0th homogeneous coordinate.

def Lec5BezoutPascal.PlaneCurve.IsSingularAt (k : Type u_1) [Field k] (X : PlaneCurve k) (p : P2 k) (h₀ : Projectivization.rep p 0 ≠ 0) (hf : (dehomogenize₀ k) X.poly ≠ 0) : Prop

A plane curve X is singular at a projective point p (with p in the chart x₀ ≠ 0) if the multiplicity of its dehomogenization at the corresponding affine point is at least two.

noncomputable def Lec5BezoutPascal.projIntersectionMultiplicity (k : Type u_1) [Field k] (X Y : PlaneCurve k) (p : P2 k) (h₀ : Projectivization.rep p 0 ≠ 0) [Module.Finite k (CurveQuotient k ((dehomogenize₀ k) X.poly) ((dehomogenize₀ k) Y.poly))] : ℕ

Projective intersection multiplicity of two plane curves at a point p (in the x₀ ≠ 0 chart), defined as the affine intersection multiplicity of their dehomogenizations.

theorem Lec5BezoutPascal.intersectionMultiplicity_ge_two_of_mult_ge_two (k : Type u_2) [Field k] [IsAlgClosed k] (f g : MvPolynomial (Fin 2) k) (p : Fin 2 → k) [Module.Finite k (CurveQuotient k f g)] (hf : f ≠ 0) (hfp : (MvPolynomial.eval p) f = 0) (hgp : (MvPolynomial.eval p) g = 0) (hmult : hypersurfaceMultiplicity k f p hf ≥ 2) : intersectionMultiplicity k f g p ≥ 2

If f has multiplicity ≥ 2 at the common zero p, then the intersection multiplicity of f and g at p is at least two.

theorem Lec5BezoutPascal.intersectionMultiplicity_ge_two_of_mult_ge_two_right (k : Type u_2) [Field k] [IsAlgClosed k] (f g : MvPolynomial (Fin 2) k) (p : Fin 2 → k) [Module.Finite k (CurveQuotient k f g)] (hg : g ≠ 0) (hfp : (MvPolynomial.eval p) f = 0) (hgp : (MvPolynomial.eval p) g = 0) (hmult : hypersurfaceMultiplicity k g p hg ≥ 2) : intersectionMultiplicity k f g p ≥ 2

Symmetric version: if g has multiplicity ≥ 2 at the common zero p, then the intersection multiplicity of f and g at p is at least two.

theorem Lec5BezoutPascal.projIntersectionMultiplicity_gt_one_of_singular_X (k : Type u_1) [Field k] [IsAlgClosed k] (X Y : PlaneCurve k) (p : P2 k) (h₀ : Projectivization.rep p 0 ≠ 0) (hf : (dehomogenize₀ k) X.poly ≠ 0) (hg : (dehomogenize₀ k) Y.poly ≠ 0) [Module.Finite k (CurveQuotient k ((dehomogenize₀ k) X.poly) ((dehomogenize₀ k) Y.poly))] (hp_on_X : (MvPolynomial.eval (affinePoint₀ k p h₀)) ((dehomogenize₀ k) X.poly) = 0) (hp_on_Y : (MvPolynomial.eval (affinePoint₀ k p h₀)) ((dehomogenize₀ k) Y.poly) = 0) (hsing : PlaneCurve.IsSingularAt k X p h₀ hf) : projIntersectionMultiplicity k X Y p h₀ > 1

Projective version: if X is singular at the common point p, the intersection multiplicity of X and Y at p exceeds one.

theorem Lec5BezoutPascal.projIntersectionMultiplicity_gt_one_of_singular_Y (k : Type u_1) [Field k] [IsAlgClosed k] (X Y : PlaneCurve k) (p : P2 k) (h₀ : Projectivization.rep p 0 ≠ 0) (hf : (dehomogenize₀ k) X.poly ≠ 0) (hg : (dehomogenize₀ k) Y.poly ≠ 0) [Module.Finite k (CurveQuotient k ((dehomogenize₀ k) X.poly) ((dehomogenize₀ k) Y.poly))] (hp_on_X : (MvPolynomial.eval (affinePoint₀ k p h₀)) ((dehomogenize₀ k) X.poly) = 0) (hp_on_Y : (MvPolynomial.eval (affinePoint₀ k p h₀)) ((dehomogenize₀ k) Y.poly) = 0) (hsing : PlaneCurve.IsSingularAt k Y p h₀ hg) : projIntersectionMultiplicity k X Y p h₀ > 1

Projective version: if Y is singular at the common point p, the intersection multiplicity of X and Y at p exceeds one.

theorem Lec5BezoutPascal.corollary20_intersection_mult_gt_one_of_singular (k : Type u_1) [Field k] [IsAlgClosed k] (X Y : PlaneCurve k) (p : P2 k) (h₀ : Projectivization.rep p 0 ≠ 0) (hf : (dehomogenize₀ k) X.poly ≠ 0) (hg : (dehomogenize₀ k) Y.poly ≠ 0) [Module.Finite k (CurveQuotient k ((dehomogenize₀ k) X.poly) ((dehomogenize₀ k) Y.poly))] (hp_on_X : (MvPolynomial.eval (affinePoint₀ k p h₀)) ((dehomogenize₀ k) X.poly) = 0) (hp_on_Y : (MvPolynomial.eval (affinePoint₀ k p h₀)) ((dehomogenize₀ k) Y.poly) = 0) (hsing : PlaneCurve.IsSingularAt k X p h₀ hf ∨ PlaneCurve.IsSingularAt k Y p h₀ hg) : projIntersectionMultiplicity k X Y p h₀ > 1

Corollary 20 (Lec 5): for two plane curves through a common point p, the intersection multiplicity at p exceeds one iff at least one curve is singular there.