The residue partition and local multiplicities of a homogeneous plane curve supply a global single-prime determinant divisor. The residue points and their multiplicities are the case n = 0 of the hypersurface construction in ProjectiveHypersurfaceResidueDeterminant.

@[reducible, inline]

abbrev CCDN.ProjectivePlaneResidue (f : MvPolynomial (Fin 3) ℤ) (p : ℕ) [Fact (Nat.Prime p)] : Set (ProjectiveResidueSpace (0 + 2) p)

The residue points of a projective plane curve: the case n = 0 of ProjectiveHypersurfaceResidue.

Equations

• CCDN.ProjectivePlaneResidue f p = CCDN.ProjectiveHypersurfaceResidue f p

@[reducible, inline]

noncomputable abbrev CCDN.projectivePlaneResidueMultiplicity {p d : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin 3) ℤ) (hf : f.IsHomogeneous d) (hf0 : (MvPolynomial.map (Int.castRingHom (ZMod p))) f ≠ 0) (r : ↑(ProjectivePlaneResidue f p)) : ℕ

The local multiplicity at a residue point of a projective plane curve.

Equations

• CCDN.projectivePlaneResidueMultiplicity f hf hf0 r = CCDN.projectiveHypersurfaceResidueMultiplicity f hf hf0 r

theorem CCDN.projectivePlaneResidueMultiplicity_spec {p d : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin 3) ℤ) (hf : f.IsHomogeneous d) (hf0 : (MvPolynomial.map (Int.castRingHom (ZMod p))) f ≠ 0) (r : ↑(ProjectivePlaneResidue f p)) : 0 < projectivePlaneResidueMultiplicity f hf hf0 r ∧ projectivePlaneResidueMultiplicity f hf hf0 r ≤ d ∧ (MvPolynomial.map (Int.castRingHom (ZMod p))) ((originShift (projectiveResidueChartLift ↑r)) (projectivePlaneChart (projectiveResiduePivot ↑r) f)) ∈ MvPolynomial.idealOfVars (Fin 2) (ZMod p) ^ projectivePlaneResidueMultiplicity f hf hf0 r ∧ (MvPolynomial.homogeneousComponent (projectivePlaneResidueMultiplicity f hf hf0 r)) ((MvPolynomial.map (Int.castRingHom (ZMod p))) ((originShift (projectiveResidueChartLift ↑r)) (projectivePlaneChart (projectiveResiduePivot ↑r) f))) ≠ 0

The multiplicity of the reduction f mod p of a plane curve at a residue point r is between 1 and the degree d; in the chart of r, translated so that r is the origin, the reduced equation lies in that power of the ideal of the origin and has a nonzero homogeneous component of that degree.

@[reducible, inline]

noncomputable abbrev CCDN.projectivePlaneTotalMultiplicity {p d : ℕ} [Fact (Nat.Prime p)] (f : MvPolynomial (Fin 3) ℤ) (hf : f.IsHomogeneous d) (hf0 : (MvPolynomial.map (Int.castRingHom (ZMod p))) f ≠ 0) : ℕ

The total residue multiplicity of a projective plane curve modulo p.

Equations

• CCDN.projectivePlaneTotalMultiplicity f hf hf0 = CCDN.projectiveHypersurfaceTotalMultiplicity f hf hf0

theorem CCDN.projective_reduction_minorGcd {s N p d M : ℕ} [Fact (Nat.Prime p)] (hs : 0 < s) (f : MvPolynomial (Fin 3) ℤ) (hf : f.IsHomogeneous d) (hf0 : (MvPolynomial.map (Int.castRingHom (ZMod p))) f ≠ 0) (F : Fin N → MvPolynomial (Fin 3) ℤ) (hF : ∀ (j : Fin N), (F j).IsHomogeneous M) (z : Fin s → IntPoint 3) (hprim : ∀ (i : Fin s), Finset.univ.gcd (z i) = 1) (hz : ∀ (i : Fin s), (MvPolynomial.eval (z i)) f = 0) : 0 < projectivePlaneTotalMultiplicity f hf hf0 ∧ ∃ (e : ℕ), s ^ 2 ≤ 2 * projectivePlaneTotalMultiplicity f hf hf0 * (e + s) ∧ ↑s ^ 2 / (2 * ↑(projectivePlaneTotalMultiplicity f hf hf0)) - ↑s ≤ ↑e ∧ ↑p ^ e ∣ Int.Matrix.minorGcd (Matrix.of fun (i : Fin s) (j : Fin N) => (MvPolynomial.eval (z i)) (F j))

Primitive integer zeros determine the residue partition, unit chart coordinates and positive local multiplicities. The divisor's leading quadratic constant uses their total multiplicity.