import OAI.AlgebraicGeometry.AbhyankarSathaye.Quotient
import OAI.AlgebraicGeometry.AbhyankarSathaye.Reconstruction
import Mathlib.Algebra.Polynomial.AlgebraMap
import Mathlib.Data.Fin.VecNotation
import Mathlib.Tactic.FinCases
namespace OAI
/-!
# Lifting a cusp relation
If `x² + y³ = h * s` and `α * h + β * y = 1`, the quotient defined by
`U³ + h * V = x`, `-U² + h * W = y`, and `S h U V W = s` is a polynomial
algebra in one variable. This includes the zero ring and rings with zero divisors.
-/
noncomputable section
namespace AbhyankarSathaye.Lifting
open MvPolynomial
variable {B : Type*} [CommRing B]
def relX (h x : B) : MvPolynomial (Fin 3) B := X 0^3+C h*X 1-C x
def relY (h y : B) : MvPolynomial (Fin 3) B := -X 0^2+C h*X 2-C y
def relS (h s : B) : MvPolynomial (Fin 3) B := S (C h) (X 0) (X 1) (X 2)-C s
def ideal (h x y s : B) : Ideal (MvPolynomial (Fin 3) B) :=
Ideal.span {relX h x, relY h y, relS h s}
abbrev Q (h x y s : B) := MvPolynomial (Fin 3) B ⧸ ideal h x y s
def qmap (h x y s : B) : MvPolynomial (Fin 3) B →ₐ[B] Q h x y s :=
Ideal.Quotient.mkₐ B (ideal h x y s)
def qvar (h x y s : B) (i : Fin 3) : Q h x y s := qmap h x y s (X i)
theorem quotient_relations (h x y s : B) :
let c := algebraMap B (Q h x y s)
let U := qvar h x y s 0
let V := qvar h x y s 1
let W := qvar h x y s 2
U^3+c h*V = c x ∧ -U^2+c h*W = c y ∧ S (c h) U V W = c s := by
dsimp only
have hx : qmap h x y s (relX h x) = 0 :=
quotient_triple_first (relX h x) (relY h y) (relS h s)
have hy : qmap h x y s (relY h y) = 0 :=
quotient_triple_second (relX h x) (relY h y) (relS h s)
have hs : qmap h x y s (relS h s) = 0 :=
quotient_triple_third (relX h x) (relY h y) (relS h s)
refine ⟨?_, ?_, ?_⟩
· apply sub_eq_zero.mp
simpa [relX, qvar] using hx
· apply sub_eq_zero.mp
simpa [relY, qvar] using hy
· apply sub_eq_zero.mp
simpa [relS, qvar] using hs
def polyU (h x β : B) : Polynomial B := inverseU (Polynomial.C h) (Polynomial.C x)
(Polynomial.C β) Polynomial.X
def polyG (x y α : B) : Polynomial B := inverseG (Polynomial.C x) (Polynomial.C y)
(Polynomial.C α) Polynomial.X
def polyW (h x y s α β : B) : Polynomial B :=
inverseW (Polynomial.C h) (Polynomial.C y) (Polynomial.C s) (Polynomial.C α)
(Polynomial.C β) (polyU h x β) (polyG x y α)
def polyV (h x y s α β : B) : Polynomial B :=
inverseV (polyU h x β) (polyG x y α) (polyW h x y s α β)
def values (h x y s α β : B) : Fin 3 → Polynomial B :=
![polyU h x β, polyV h x y s α β, polyW h x y s α β]
theorem values_relations (h x y s α β : B)
(hc : x^2+y^3 = h*s) (hb : α*h+β*y = 1) :
(aeval (values h x y s α β)) (relX h x) = 0 ∧
(aeval (values h x y s α β)) (relY h y) = 0 ∧
(aeval (values h x y s α β)) (relS h s) = 0 := by
have hc' : (Polynomial.C x)^2+(Polynomial.C y)^3 = Polynomial.C h*Polynomial.C s := by
simpa using congrArg (Polynomial.C : B →+* Polynomial B) hc
have hb' : Polynomial.C α*Polynomial.C h+Polynomial.C β*Polynomial.C y = 1 := by
simpa using congrArg (Polynomial.C : B →+* Polynomial B) hb
have hr := inverse_relations (Polynomial.C h) (Polynomial.C x) (Polynomial.C y)
(Polynomial.C s) (Polynomial.C α) (Polynomial.C β) Polynomial.X hc' hb'
dsimp only at hr
refine ⟨?_, ?_, ?_⟩
· simpa [relX, values, polyU, polyV, polyG, polyW, Polynomial.algebraMap_eq]
using sub_eq_zero.mpr hr.1
· simpa [relY, values, polyU, polyV, polyG, polyW, Polynomial.algebraMap_eq]
using sub_eq_zero.mpr hr.2.1
· simpa [relS, values, polyU, polyV, polyG, polyW, Polynomial.algebraMap_eq]
using sub_eq_zero.mpr hr.2.2
def forward (h x y s α β : B) (hc : x^2+y^3 = h*s) (hb : α*h+β*y = 1) :
Q h x y s →ₐ[B] Polynomial B :=
lift_triple (relX h x) (relY h y) (relS h s) (aeval (values h x y s α β))
(values_relations h x y s α β hc hb).1
(values_relations h x y s α β hc hb).2.1
(values_relations h x y s α β hc hb).2.2
@[simp] theorem forward_qvar (h x y s α β : B) (hc hb) (i : Fin 3) :
forward h x y s α β hc hb (qvar h x y s i) = values h x y s α β i := by
change aeval (values h x y s α β) (X i) = values h x y s α β i
exact aeval_X _ _
def backward (h x y s α β : B) : Polynomial B →ₐ[B] Q h x y s :=
Polynomial.aeval (parameter (algebraMap B _ α) (algebraMap B _ β)
(qvar h x y s 0) (qvar h x y s 1) (qvar h x y s 2))
theorem forward_backward (h x y s α β : B) (hc hb) :
(forward h x y s α β hc hb).comp (backward h x y s α β) = AlgHom.id B _ := by
apply Polynomial.algHom_ext
have hb' : Polynomial.C α*Polynomial.C h+Polynomial.C β*Polynomial.C y = 1 := by
simpa using congrArg (Polynomial.C : B →+* Polynomial B) hb
simpa [backward, values, polyU, polyV, polyW, polyG, Polynomial.algebraMap_eq]
using inverse_parameter (Polynomial.C h) (Polynomial.C x) (Polynomial.C y)
(Polynomial.C s) (Polynomial.C α) (Polynomial.C β) Polynomial.X hb'
theorem backward_forward (h x y s α β : B) (hc hb) :
(backward h x y s α β).comp (forward h x y s α β hc hb) = AlgHom.id B _ := by
apply Ideal.Quotient.algHom_ext
apply MvPolynomial.algHom_ext
intro i
have hb' : algebraMap B (Q h x y s) α*algebraMap B _ h+
algebraMap B _ β*algebraMap B _ y = 1 := by
simpa using congrArg (algebraMap B (Q h x y s)) hb
obtain ⟨hx, hy, hs⟩ := quotient_relations h x y s
have hr := original_reconstruction (algebraMap B (Q h x y s) h)
(algebraMap B _ x) (algebraMap B _ y) (algebraMap B _ s)
(algebraMap B _ α) (algebraMap B _ β)
(qvar h x y s 0) (qvar h x y s 1) (qvar h x y s 2) hb' hx hy hs
dsimp only at hr
change backward h x y s α β (forward h x y s α β hc hb (qvar h x y s i)) =
qvar h x y s i
rw [forward_qvar]
fin_cases i
· simpa [values, polyU, backward] using hr.1
· simpa [values, polyU, polyV, polyG, polyW, backward] using hr.2.1
· simpa [values, polyU, polyV, polyG, polyW, backward] using hr.2.2
def equivalence (h x y s α β : B) (hc : x^2+y^3 = h*s) (hb : α*h+β*y = 1) :
Q h x y s ≃ₐ[B] Polynomial B :=
AlgEquiv.ofAlgHom (forward h x y s α β hc hb) (backward h x y s α β)
(forward_backward h x y s α β hc hb) (backward_forward h x y s α β hc hb)
end AbhyankarSathaye.Lifting
end
end OAI
SHA-256 1572068ef8754f570b77049940b69f9c6fe4450390f818394c40f5a9af1dd323