Definitions/Def_WeierstrassCurve_ProjModel_GroupLawVocabulary.lean

import Definitions.Def_WeierstrassCurve_ProjModel
import Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic ↗
import Mathlib.RingTheory.MvPolynomial.Homogeneous ↗
import Mathlib.Algebra.MvPolynomial.Rename ↗
import Mathlib.RingTheory.Ideal.Span ↗
import Mathlib.RingTheory.Polynomial.Basic ↗
import Mathlib.RingTheory.Localization.FractionRing ↗
import Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal ↗
import Mathlib.RingTheory.Ideal.Quotient.Operations ↗
import Mathlib.RingTheory.TensorProduct.Basic ↗
import Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization ↗
import Mathlib.RingTheory.FiniteType ↗
import Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper ↗
import Mathlib.AlgebraicGeometry.Cover.Open ↗
import Mathlib.AlgebraicGeometry.Gluing ↗
import Mathlib.AlgebraicGeometry.Pullbacks ↗
import Mathlib.RingTheory.MvPolynomial.Ideal ↗
import Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor ↗
import Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point ↗
import Mathlib.Algebra.Module.Torsion.Basic ↗
import Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point ↗
import Definitions.Def_WeierstrassCurve_ProjModel_AddFormulas

set_option Elab.async false

section MEGA_KwLRSymOnCurveScaled_lean
set_option autoImplicit false
set_option linter.unusedSimpArgs false
set_option maxHeartbeats 6400000

noncomputable section

open MvPolynomial WeierstrassCurve

namespace WeierstrassProjModel

attribute [local instance] MvPolynomial.gradedAlgebra

universe u

variable {R : Type u} [CommRing R] (W : WeierstrassCurve R)

local notation "P₆" => MvPolynomial (Fin 3 ⊕ Fin 3) R
local notation "WP₁" => kw_lrAdd_WP₁ W
local notation "WP₂" => kw_lrAdd_WP₂ W

section Abstract

variable {S : Type u} [CommRing S] [Algebra R S]

theorem kw_lrSymOC_aeval_scale (l x y z : S) :
    aeval ![l*x, l*y, l*z] W.toProjective.polynomial
      = l^3 * aeval ![x, y, z] W.toProjective.polynomial := by
  simp only [WeierstrassCurve.Projective.polynomial, WeierstrassCurve.toProjective,
    map_add, map_sub, map_mul, map_pow, aeval_X, aeval_C,
    Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_two,
    Matrix.head_cons, Matrix.tail_cons]
  ring

theorem kw_lrSymOC_aeval_diff (x x' y y' z z' : S) :
    aeval ![x, y, z] W.toProjective.polynomial
        - aeval ![x', y', z'] W.toProjective.polynomial
      = (x - x') * (- (x^2 + x*x' + x'^2) - algebraMap R S W.a₂ * (x+x') * z
          + algebraMap R S W.a₁ * y * z - algebraMap R S W.a₄ * z^2)
        + (y - y') * ((y+y') * z + algebraMap R S W.a₁ * x' * z
          + algebraMap R S W.a₃ * z^2)
        + (z - z') * (y'^2 + algebraMap R S W.a₁ * x' * y'
          + algebraMap R S W.a₃ * y' * (z+z') - algebraMap R S W.a₂ * x'^2
          - algebraMap R S W.a₄ * x' * (z+z')
          - algebraMap R S W.a₆ * (z^2 + z*z' + z'^2)) := by
  simp only [WeierstrassCurve.Projective.polynomial, WeierstrassCurve.toProjective,
    map_add, map_sub, map_mul, map_pow, aeval_X, aeval_C,
    Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_two,
    Matrix.head_cons, Matrix.tail_cons]
  ring

end Abstract

theorem kw_lrSymOC_scaled_mem_span_of (l m : P₆)
    (hX : l * kw_lrSym_X W - m * kw_lrAdd_X W ∈ Ideal.span {WP₁, WP₂})
    (hY : l * kw_lrSym_Y W - m * kw_lrAdd_Y W ∈ Ideal.span {WP₁, WP₂})
    (hZ : l * kw_lrSym_Z W - m * kw_lrAdd_Z W ∈ Ideal.span {WP₁, WP₂}) :
    l^3 * aeval ![kw_lrSym_X W, kw_lrSym_Y W, kw_lrSym_Z W]
          W.toProjective.polynomial
      ∈ Ideal.span {WP₁, WP₂} := by
  have hdiff : l^3 * aeval ![kw_lrSym_X W, kw_lrSym_Y W, kw_lrSym_Z W]
        W.toProjective.polynomial
      - m^3 * aeval ![kw_lrAdd_X W, kw_lrAdd_Y W, kw_lrAdd_Z W]
        W.toProjective.polynomial ∈ Ideal.span {WP₁, WP₂} := by
    rw [← kw_lrSymOC_aeval_scale W l, ← kw_lrSymOC_aeval_scale W m,
        kw_lrSymOC_aeval_diff W
          (l * kw_lrSym_X W) (m * kw_lrAdd_X W)
          (l * kw_lrSym_Y W) (m * kw_lrAdd_Y W)
          (l * kw_lrSym_Z W) (m * kw_lrAdd_Z W)]
    exact add_mem (add_mem (Ideal.mul_mem_right _ _ hX) (Ideal.mul_mem_right _ _ hY))
      (Ideal.mul_mem_right _ _ hZ)
  have hAdd : m^3 * aeval ![kw_lrAdd_X W, kw_lrAdd_Y W, kw_lrAdd_Z W]
        W.toProjective.polynomial ∈ Ideal.span {WP₁, WP₂} :=
    Ideal.mul_mem_left _ _ (kw_lrAdd_onCurve_mem_span W)
  have := add_mem hdiff hAdd
  simpa using this

theorem kw_lrSymOC_scaled_mem_span_Z :
    (kw_lrAdd_Z W)^3 * aeval ![kw_lrSym_X W, kw_lrSym_Y W, kw_lrSym_Z W]
          W.toProjective.polynomial
      ∈ Ideal.span {WP₁, WP₂} := by
  refine kw_lrSymOC_scaled_mem_span_of W (kw_lrAdd_Z W) (kw_lrSym_Z W) ?_ ?_ ?_
  · have := kw_lrSym_minor_XZ_mem_span W
    rwa [show kw_lrSym_X W * kw_lrAdd_Z W - kw_lrSym_Z W * kw_lrAdd_X W
        = kw_lrAdd_Z W * kw_lrSym_X W - kw_lrSym_Z W * kw_lrAdd_X W from by ring] at this
  · have := kw_lrSym_minor_YZ_mem_span W
    rwa [show kw_lrSym_Y W * kw_lrAdd_Z W - kw_lrSym_Z W * kw_lrAdd_Y W
        = kw_lrAdd_Z W * kw_lrSym_Y W - kw_lrSym_Z W * kw_lrAdd_Y W from by ring] at this
  · rw [mul_comm, sub_self]; exact Ideal.zero_mem _

end WeierstrassProjModel

end

end MEGA_KwLRSymOnCurveScaled_lean

section MEGA_KwLRSymOnCurve_lean
set_option autoImplicit false
set_option maxHeartbeats 6400000
set_option linter.unusedSimpArgs false

noncomputable section

open MvPolynomial WeierstrassCurve ProjWeierstrassCubicPrime

namespace WeierstrassProjModel

universe u v

variable {R : Type u} [CommRing R] (W : WeierstrassCurve R)

section Map

variable {S : Type v} [CommRing S] (f : R →+* S)

theorem kw_lrSymOC_map_WP₁ :
    MvPolynomial.map f (kw_lrAdd_WP₁ W) = kw_lrAdd_WP₁ (W.map f) := by
  simp only [kw_lrAdd_WP₁, MvPolynomial.map_rename,
    WeierstrassCurve.Projective.map_polynomial, WeierstrassCurve.Projective.map,
    WeierstrassCurve.toProjective]

theorem kw_lrSymOC_map_WP₂ :
    MvPolynomial.map f (kw_lrAdd_WP₂ W) = kw_lrAdd_WP₂ (W.map f) := by
  simp only [kw_lrAdd_WP₂, MvPolynomial.map_rename,
    WeierstrassCurve.Projective.map_polynomial, WeierstrassCurve.Projective.map,
    WeierstrassCurve.toProjective]

theorem kw_lrSymOC_map_lrSym_X :
    MvPolynomial.map f (kw_lrSym_X W) = kw_lrSym_X (W.map f) := by
  simp only [kw_lrSym_X, map_add, map_mul, map_neg, map_pow, MvPolynomial.map_C,
    MvPolynomial.map_X, map_ofNat, map_one, WeierstrassCurve.map_a₁, WeierstrassCurve.map_a₂,
    WeierstrassCurve.map_a₃, WeierstrassCurve.map_a₄, WeierstrassCurve.map_a₆, map_sub]

theorem kw_lrSymOC_map_lrSym_Y :
    MvPolynomial.map f (kw_lrSym_Y W) = kw_lrSym_Y (W.map f) := by
  simp only [kw_lrSym_Y, map_add, map_mul, map_neg, map_pow, MvPolynomial.map_C,
    MvPolynomial.map_X, map_ofNat, map_one, WeierstrassCurve.map_a₁, WeierstrassCurve.map_a₂,
    WeierstrassCurve.map_a₃, WeierstrassCurve.map_a₄, WeierstrassCurve.map_a₆, map_sub]

theorem kw_lrSymOC_map_lrSym_Z :
    MvPolynomial.map f (kw_lrSym_Z W) = kw_lrSym_Z (W.map f) := by
  simp only [kw_lrSym_Z, map_add, map_mul, map_neg, map_pow, MvPolynomial.map_C,
    MvPolynomial.map_X, map_ofNat, map_one, WeierstrassCurve.map_a₁, WeierstrassCurve.map_a₂,
    WeierstrassCurve.map_a₃, WeierstrassCurve.map_a₄, WeierstrassCurve.map_a₆, map_sub]

theorem kw_lrSymOC_map_W_lrSym :
    MvPolynomial.map f
        (aeval ![kw_lrSym_X W, kw_lrSym_Y W, kw_lrSym_Z W] W.toProjective.polynomial)
      = aeval ![kw_lrSym_X (W.map f), kw_lrSym_Y (W.map f), kw_lrSym_Z (W.map f)]
          (W.map f).toProjective.polynomial := by
  simp only [WeierstrassCurve.Projective.polynomial, WeierstrassCurve.toProjective,
    map_add, map_sub, map_mul, map_pow, aeval_X, aeval_C,
    Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_two,
    Matrix.head_cons, Matrix.tail_cons, MvPolynomial.map_C, MvPolynomial.algebraMap_eq,
    WeierstrassCurve.map_a₁, WeierstrassCurve.map_a₂, WeierstrassCurve.map_a₃,
    WeierstrassCurve.map_a₄, WeierstrassCurve.map_a₆,
    kw_lrSymOC_map_lrSym_X, kw_lrSymOC_map_lrSym_Y, kw_lrSymOC_map_lrSym_Z]

end Map

local notation "R₀" => MvPolynomial (Fin 5) ℤ

abbrev kw_lrSymOC_W₀ : WeierstrassCurve R₀ := ⟨X 0, X 1, X 2, X 3, X 4⟩

local notation "W₀" => kw_lrSymOC_W₀
local notation "P₆₀" => MvPolynomial (Fin 3 ⊕ Fin 3) R₀
local notation "WP₁₀" => kw_lrAdd_WP₁ W₀
local notation "WP₂₀" => kw_lrAdd_WP₂ W₀

theorem kw_lrSymOC_W₀_map :
    WeierstrassCurve.map kw_lrSymOC_W₀
        (MvPolynomial.eval₂Hom (Int.castRingHom R) ![W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]) = W := by
  ext <;> simp only [WeierstrassCurve.map, kw_lrSymOC_W₀, MvPolynomial.eval₂Hom_X'] <;> rfl

section EngineHelpers

variable {F : Type*} [CommRing F]

theorem kw_lrSymOC_finSuccEquiv_map {S : Type*} [CommRing S] (f : F →+* S)
    (p : MvPolynomial (Fin 3) F) :
    finSuccEquiv S 2 (MvPolynomial.map f p)
      = Polynomial.map (MvPolynomial.map f) (finSuccEquiv F 2 p) := by
  induction p using MvPolynomial.induction_on with
  | C a => simp [finSuccEquiv_apply, MvPolynomial.eval₂_C]
  | add p q hp hq => simp [hp, hq, map_add, Polynomial.map_add]
  | mul_X p i hp =>
    simp only [map_mul, MvPolynomial.map_X, hp, Polynomial.map_mul]
    congr 1
    refine Fin.cases ?_ (fun j => ?_) i
    · simp [finSuccEquiv_apply]
    · simp [finSuccEquiv_apply]

theorem kw_lrSymOC_wCubic_map (V : WeierstrassCurve.Projective F)
    {S : Type*} [CommRing S] (f : F →+* S) :
    (wCubic (V.map f)).toPoly
      = Polynomial.map (MvPolynomial.map f) (wCubic V).toPoly := by
  simp only [wCubic, Cubic.toPoly, WeierstrassCurve.Projective.map, WeierstrassCurve.map,
    Polynomial.map_add, Polynomial.map_mul, Polynomial.map_sub, Polynomial.map_pow,
    Polynomial.map_C, Polynomial.map_X, Polynomial.map_one, MvPolynomial.map_C,
    MvPolynomial.map_X, map_mul, map_sub, map_one, map_pow]

end EngineHelpers

section Engine

variable {F : Type*} [CommRing F] [IsDomain F] (V : WeierstrassCurve.Projective F)

theorem kw_lrSymOC_isDomain_quot_span_poly :
    IsDomain (MvPolynomial (Fin 3) F ⧸ Ideal.span {V.polynomial}) := by
  have hθ : Function.Injective (algebraMap F (FractionRing F)) :=
    IsFractionRing.injective F (FractionRing F)
  have hθ'' : Function.Injective
      (MvPolynomial.map (σ := Fin 2) (algebraMap F (FractionRing F))) :=
    MvPolynomial.map_injective _ hθ

  have hD : IsDomain (MvPolynomial (Fin 3) (FractionRing F)
      ⧸ Ideal.span {(V.map (algebraMap F (FractionRing F))).polynomial}) :=
    isDomain_quotient_span_polynomial (V.map (algebraMap F (FractionRing F)))

  have hcomap : (Ideal.span {(V.map (algebraMap F (FractionRing F))).polynomial}).comap
      (MvPolynomial.map (algebraMap F (FractionRing F)) :
        MvPolynomial (Fin 3) F →+* MvPolynomial (Fin 3) (FractionRing F))
      ≤ Ideal.span {V.polynomial} := by
    intro p hp
    simp only [Ideal.mem_comap, Ideal.mem_span_singleton] at hp ⊢

    have hp' : finSuccEquiv (FractionRing F) 2 (V.map (algebraMap F (FractionRing F))).polynomial
        ∣ finSuccEquiv (FractionRing F) 2 (MvPolynomial.map (algebraMap F (FractionRing F)) p) :=
      map_dvd (finSuccEquiv (FractionRing F) 2) hp
    rw [kw_lrSymOC_finSuccEquiv_map (algebraMap F (FractionRing F)) p,
        finSuccEquiv_polynomial (V.map (algebraMap F (FractionRing F))),
        kw_lrSymOC_wCubic_map V (algebraMap F (FractionRing F))] at hp'
    have hdvd : (wCubic V).toPoly ∣ finSuccEquiv F 2 p :=
      (Polynomial.map_dvd_map _ hθ'' (wCubic_toPoly_monic V)).mp (neg_dvd.mp hp')

    have hdvd' : finSuccEquiv F 2 V.polynomial ∣ finSuccEquiv F 2 p := by
      rw [finSuccEquiv_polynomial V]; exact hdvd.neg_left
    have := map_dvd (finSuccEquiv F 2).symm hdvd'
    simpa only [AlgEquiv.symm_apply_apply] using this

  have hH : Ideal.span {V.polynomial}
      ≤ (Ideal.span {(V.map (algebraMap F (FractionRing F))).polynomial}).comap
        (MvPolynomial.map (algebraMap F (FractionRing F))) := by
    rw [Ideal.span_le, Set.singleton_subset_iff, SetLike.mem_coe, Ideal.mem_comap,
      WeierstrassCurve.Projective.map_polynomial]
    exact Ideal.subset_span (Set.mem_singleton _)
  exact (Ideal.quotientMap_injective' hcomap :
    Function.Injective (Ideal.quotientMap _ _ hH)).isDomain _

end Engine

abbrev kw_lrSymOC_ℬ₀ :=
  MvPolynomial (Fin 3) R₀ ⧸ Ideal.span {kw_lrSymOC_W₀.toProjective.polynomial}

local notation "ℬ₀" => kw_lrSymOC_ℬ₀

instance kw_lrSymOC_isDomain_ℬ₀ : IsDomain ℬ₀ :=
  kw_lrSymOC_isDomain_quot_span_poly kw_lrSymOC_W₀.toProjective

theorem kw_lrSymOC_isDomain_quotSpanPair :
    IsDomain (P₆₀ ⧸ Ideal.span {WP₁₀, WP₂₀}) := by
  classical
  let A := MvPolynomial (Fin 3) R₀
  let π : A →+* ℬ₀ := Ideal.Quotient.mk _
  let πC : R₀ →+* ℬ₀ := π.comp C
  let Wℬ : WeierstrassCurve ℬ₀ := kw_lrSymOC_W₀.map πC

  haveI hD : IsDomain
      (MvPolynomial (Fin 3) ℬ₀ ⧸ Ideal.span {Wℬ.toProjective.polynomial}) :=
    kw_lrSymOC_isDomain_quot_span_poly Wℬ.toProjective

  let e : P₆₀ ≃+* MvPolynomial (Fin 3) A :=
    (sumAlgEquiv R₀ (Fin 3) (Fin 3) : P₆₀ ≃ₐ[R₀] _).toRingEquiv
  let mπ : MvPolynomial (Fin 3) A →+* MvPolynomial (Fin 3) ℬ₀ := MvPolynomial.map π
  let ψ : P₆₀ →+* (MvPolynomial (Fin 3) ℬ₀ ⧸ Ideal.span {Wℬ.toProjective.polynomial}) :=
    (Ideal.Quotient.mk _).comp (mπ.comp (e : P₆₀ →+* _))
  have hsurj : Function.Surjective ψ :=
    (Ideal.Quotient.mk_surjective).comp
      ((MvPolynomial.map_surjective π Ideal.Quotient.mk_surjective).comp e.surjective)

  have heWP₁ : e WP₁₀
      = MvPolynomial.map (C : R₀ →+* A) kw_lrSymOC_W₀.toProjective.polynomial := by
    have h := DFunLike.congr_fun (sumAlgEquiv_comp_rename_inl R₀ (Fin 3) (Fin 3))
      kw_lrSymOC_W₀.toProjective.polynomial
    simpa [kw_lrAdd_WP₁, e] using h
  have heWP₂ : e WP₂₀ = C kw_lrSymOC_W₀.toProjective.polynomial := by
    have h := DFunLike.congr_fun (sumAlgEquiv_comp_rename_inr R₀ (Fin 3) (Fin 3))
      kw_lrSymOC_W₀.toProjective.polynomial
    simpa [kw_lrAdd_WP₂, e] using h

  have hker : RingHom.ker ψ = Ideal.span {WP₁₀, WP₂₀} := by

    have hkermπ : RingHom.ker mπ
        = Ideal.span {(C kw_lrSymOC_W₀.toProjective.polynomial :
            MvPolynomial (Fin 3) A)} := by
      rw [MvPolynomial.ker_map, Ideal.mk_ker, Ideal.map_span, Set.image_singleton]
    have hmap : mπ (e WP₁₀) = Wℬ.toProjective.polynomial := by
      rw [heWP₁]
      show (MvPolynomial.map π) ((MvPolynomial.map C) _) = _
      rw [MvPolynomial.map_map, ← WeierstrassCurve.Projective.map_polynomial]
    have hcomap :
        (Ideal.span {Wℬ.toProjective.polynomial}).comap mπ
          = Ideal.span {e WP₁₀, e WP₂₀} := by
      have hmapspan :
          (Ideal.span {e WP₁₀}).map mπ = Ideal.span {Wℬ.toProjective.polynomial} := by
        rw [Ideal.map_span, Set.image_singleton, hmap]
      rw [← hmapspan, Ideal.comap_map_of_surjective mπ
          (MvPolynomial.map_surjective π Ideal.Quotient.mk_surjective),
        ← RingHom.ker_eq_comap_bot, hkermπ, ← heWP₂, ← Ideal.span_union,
        Set.union_singleton, Set.pair_comm]

    have h₁ : RingHom.ker ψ
        = ((Ideal.span {Wℬ.toProjective.polynomial}).comap mπ).comap
            (e : P₆₀ →+* _) := by
      ext x; simp only [RingHom.mem_ker, Ideal.mem_comap]
      exact Ideal.Quotient.eq_zero_iff_mem
    rw [h₁, hcomap, Ideal.comap_coe, ← Ideal.map_symm, Ideal.map_span, Set.image_pair,
      RingEquiv.symm_apply_apply, RingEquiv.symm_apply_apply]

  have heq : P₆₀ ⧸ Ideal.span {WP₁₀, WP₂₀}
      ≃+* (MvPolynomial (Fin 3) ℬ₀ ⧸ Ideal.span {Wℬ.toProjective.polynomial}) :=
    (Ideal.quotEquivOfEq hker.symm).trans (RingHom.quotientKerEquivOfSurjective hsurj)
  exact heq.injective.isDomain _

theorem kw_lrSymOC_lrAddZ_notMem_span :
    kw_lrAdd_Z W₀ ∉ Ideal.span {WP₁₀, WP₂₀} := by

  let ev₀ : R₀ →+* ℤ := MvPolynomial.eval (0 : Fin 5 → ℤ)
  let ev : P₆₀ →+* ℤ :=
    MvPolynomial.eval₂Hom ev₀ (Sum.elim ![0, 0, 1] ![1, 1, 1])

  have hevXl : ∀ i, ev (X (Sum.inl i)) = ![(0:ℤ), 0, 1] i := fun i => by
    simp [ev, Sum.elim_inl]
  have hevXr : ∀ i, ev (X (Sum.inr i)) = ![(1:ℤ), 1, 1] i := fun i => by
    simp [ev, Sum.elim_inr]
  have hevCX : ∀ j : Fin 5, ev (C (X j)) = 0 := fun j => by
    simp [ev, ev₀]
  have hevC : ∀ n : ℤ, ev (C ((n : R₀))) = n := fun n => by
    simp [ev, ev₀]
  intro hmem
  have hWP₁ : ev WP₁₀ = 0 := by
    show ev (rename Sum.inl kw_lrSymOC_W₀.toProjective.polynomial) = 0
    simp only [WeierstrassCurve.Projective.polynomial, WeierstrassCurve.toProjective,
      kw_lrSymOC_W₀, map_add, map_sub, map_mul, map_pow, rename_C, rename_X]
    simp only [hevXl, hevCX, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_two,
      Matrix.head_cons, Matrix.tail_cons]
    ring
  have hWP₂ : ev WP₂₀ = 0 := by
    show ev (rename Sum.inr kw_lrSymOC_W₀.toProjective.polynomial) = 0
    simp only [WeierstrassCurve.Projective.polynomial, WeierstrassCurve.toProjective,
      kw_lrSymOC_W₀, map_add, map_sub, map_mul, map_pow, rename_C, rename_X]
    simp only [hevXr, hevCX, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_two,
      Matrix.head_cons, Matrix.tail_cons]
    ring
  have hZ : ev (kw_lrAdd_Z W₀) = 1 := by
    simp only [kw_lrAdd_Z, kw_lrAdd_starZ, kw_lrAdd_c₁₂, kw_lrAdd_c₂₁,
      kw_lrSymOC_W₀, map_add, map_sub, map_mul, map_neg, map_pow,
      hevXl, hevXr, hevCX, C_mul, hevC,
      Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_two,
      Matrix.head_cons, Matrix.tail_cons]
    ring
  have hker : Ideal.span {WP₁₀, WP₂₀} ≤ RingHom.ker ev := by
    rw [Ideal.span_le]
    intro x hx
    rcases (Set.mem_insert_iff.mp hx) with rfl | hx'
    · exact hWP₁
    · rw [Set.mem_singleton_iff.mp hx']; exact hWP₂
  have habs : ev (kw_lrAdd_Z W₀) = 0 := hker hmem
  rw [hZ] at habs
  exact one_ne_zero habs

theorem kw_lrSymOC_univ_mem_span :
    aeval ![kw_lrSym_X W₀, kw_lrSym_Y W₀, kw_lrSym_Z W₀]
        kw_lrSymOC_W₀.toProjective.polynomial
      ∈ Ideal.span {WP₁₀, WP₂₀} := by
  haveI := kw_lrSymOC_isDomain_quotSpanPair
  rw [← Ideal.Quotient.eq_zero_iff_mem]
  have hscaled := kw_lrSymOC_scaled_mem_span_Z W₀
  rw [← Ideal.Quotient.eq_zero_iff_mem, map_mul, map_pow] at hscaled
  have hZne : (Ideal.Quotient.mk (Ideal.span {WP₁₀, WP₂₀})) (kw_lrAdd_Z W₀) ≠ 0 := by
    rw [Ne, Ideal.Quotient.eq_zero_iff_mem]
    exact kw_lrSymOC_lrAddZ_notMem_span
  exact (mul_eq_zero.mp hscaled).resolve_left (pow_ne_zero 3 hZne)

theorem kw_lrSym_onCurve_mem_span :
    aeval ![kw_lrSym_X W, kw_lrSym_Y W, kw_lrSym_Z W]
        W.toProjective.polynomial
      ∈ Ideal.span {kw_lrAdd_WP₁ W, kw_lrAdd_WP₂ W} := by
  let φ : R₀ →+* R := MvPolynomial.eval₂Hom (Int.castRingHom R) ![W.a₁, W.a₂, W.a₃, W.a₄, W.a₆]
  have hW : kw_lrSymOC_W₀.map φ = W := kw_lrSymOC_W₀_map W

  have hmem := Ideal.mem_map_of_mem
    (MvPolynomial.map φ : P₆₀ →+* MvPolynomial (Fin 3 ⊕ Fin 3) R)
    kw_lrSymOC_univ_mem_span
  rw [Ideal.map_span, Set.image_pair, kw_lrSymOC_map_WP₁, kw_lrSymOC_map_WP₂,
    hW] at hmem
  have hrw := kw_lrSymOC_map_W_lrSym kw_lrSymOC_W₀ φ
  rw [hW] at hrw
  rw [← hrw]
  exact hmem

end WeierstrassProjModel

end

end MEGA_KwLRSymOnCurve_lean

section MEGA_KwLRAddQuotientGradedHom_lean
set_option autoImplicit false
set_option linter.unusedSimpArgs false

noncomputable section

open MvPolynomial WeierstrassCurve HomogeneousIdealQuotientGrading ProjWeierstrassCubicPrime
open scoped TensorProduct

namespace WeierstrassProjModel

attribute [local instance] MvPolynomial.gradedAlgebra

universe u

variable {R : Type u} [CommRing R] (W : WeierstrassCurve R)

local notation "P₆" => MvPolynomial (Fin 3 ⊕ Fin 3) R
local notation "WP₁" => kw_lrAdd_WP₁ W
local notation "WP₂" => kw_lrAdd_WP₂ W
local notation "ℬ" => ProjModelRingCR W.toProjective

def kw_lrAdd_vec : Fin 3 → P₆ := ![kw_lrAdd_X W, kw_lrAdd_Y W, kw_lrAdd_Z W]

theorem kw_lrAdd_vec_isHomogeneous (k : Fin 3) : (kw_lrAdd_vec W k).IsHomogeneous 4 := by
  fin_cases k
  · exact kw_lrAdd_X_isHomogeneous W
  · exact kw_lrAdd_Y_isHomogeneous W
  · exact kw_lrAdd_Z_isHomogeneous W

theorem kw_lrComul_WP₁_isHomogeneous : (WP₁).IsHomogeneous 3 :=
  (isHomogeneous_polynomial W.toProjective).rename_isHomogeneous

theorem kw_lrComul_WP₂_isHomogeneous : (WP₂).IsHomogeneous 3 :=
  (isHomogeneous_polynomial W.toProjective).rename_isHomogeneous

theorem kw_lrComul_biSpan_isHomogeneous :
    (Ideal.span {WP₁, WP₂}).IsHomogeneous (homogeneousSubmodule (Fin 3 ⊕ Fin 3) R) := by
  refine Ideal.homogeneous_span _ _ ?_
  rintro p (rfl | hp)
  · exact ⟨3, (mem_homogeneousSubmodule _ _).mpr (kw_lrComul_WP₁_isHomogeneous W)⟩
  · rw [Set.mem_singleton_iff] at hp; subst hp
    exact ⟨3, (mem_homogeneousSubmodule _ _).mpr (kw_lrComul_WP₂_isHomogeneous W)⟩

def kw_lrComul_biIdeal : HomogeneousIdeal (homogeneousSubmodule (Fin 3 ⊕ Fin 3) R) :=
  ⟨Ideal.span {WP₁, WP₂}, kw_lrComul_biSpan_isHomogeneous W⟩

abbrev KwLRBiRing : Type u := P₆ ⧸ (kw_lrComul_biIdeal W).toIdeal

local notation "ℬ²" => KwLRBiRing W

abbrev kw_lrComul_biGrading : ℕ → Submodule R (ℬ²) :=
  quotGradingSubmodule (homogeneousSubmodule (Fin 3 ⊕ Fin 3) R) (kw_lrComul_biIdeal W).toIdeal

def kw_lrAdd_substHom : MvPolynomial (Fin 3) R →ₐ[R] P₆ := aeval (kw_lrAdd_vec W)

@[simp]
theorem kw_lrAdd_substHom_X (k : Fin 3) :
    kw_lrAdd_substHom W (X k) = kw_lrAdd_vec W k := aeval_X _ _

theorem kw_lrAdd_substHom_isHomogeneous {p : MvPolynomial (Fin 3) R} {n : ℕ}
    (hp : p.IsHomogeneous n) : (kw_lrAdd_substHom W p).IsHomogeneous (4 * n) :=
  hp.aeval (kw_lrAdd_vec W) (kw_lrAdd_vec_isHomogeneous W)

theorem kw_lrAdd_substHom_polynomial_mem :
    kw_lrAdd_substHom W W.toProjective.polynomial ∈ (kw_lrComul_biIdeal W).toIdeal := by
  exact kw_lrAdd_onCurve_mem_span W

noncomputable def kw_lrAdd_comulHom : (ℬ) →ₐ[R] (ℬ²) :=
  Ideal.Quotient.liftₐ (projModelHomogeneousIdealCR W.toProjective).toIdeal
    ((Ideal.Quotient.mkₐ R (kw_lrComul_biIdeal W).toIdeal).comp (kw_lrAdd_substHom W))
    (fun a ha => by
      refine (Ideal.Quotient.eq_zero_iff_mem).mpr ?_
      have hle : Ideal.span {W.toProjective.polynomial}
          ≤ (kw_lrComul_biIdeal W).toIdeal.comap (kw_lrAdd_substHom W).toRingHom :=
        Ideal.span_le.mpr
          (Set.singleton_subset_iff.mpr (kw_lrAdd_substHom_polynomial_mem W))
      exact hle ha)

theorem kw_lrAdd_comulHom_mk (a : MvPolynomial (Fin 3) R) :
    kw_lrAdd_comulHom W
        (Ideal.Quotient.mk (projModelHomogeneousIdealCR W.toProjective).toIdeal a)
      = Ideal.Quotient.mk (kw_lrComul_biIdeal W).toIdeal (kw_lrAdd_substHom W a) := by
  rfl

theorem kw_lrAdd_comulHom_mk_X (k : Fin 3) :
    kw_lrAdd_comulHom W
        (Ideal.Quotient.mk (projModelHomogeneousIdealCR W.toProjective).toIdeal (X k))
      = Ideal.Quotient.mk (kw_lrComul_biIdeal W).toIdeal (kw_lrAdd_vec W k) := by
  rw [kw_lrAdd_comulHom_mk, kw_lrAdd_substHom_X]

theorem kw_lrAdd_comulHom_graded {n : ℕ} {x : ℬ}
    (hx : x ∈ projModelGradingCR W.toProjective n) :
    kw_lrAdd_comulHom W x ∈ kw_lrComul_biGrading W (4 * n) := by
  obtain ⟨a, ha, rfl⟩ := (mem_quotGradingSubmodule_iff _ _).mp hx
  show Ideal.Quotient.mk (kw_lrComul_biIdeal W).toIdeal (kw_lrAdd_substHom W a)
    ∈ kw_lrComul_biGrading W (4 * n)
  exact mk_mem_quotGradingSubmodule _ _
    ((mem_homogeneousSubmodule _ _).mpr
      (kw_lrAdd_substHom_isHomogeneous W ((mem_homogeneousSubmodule _ _).mp ha)))

section TensorBridge

open Algebra.TensorProduct

noncomputable def kw_lrComul_incL : (ℬ) →ₐ[R] (ℬ) ⊗[R] (ℬ) :=
  Algebra.TensorProduct.includeLeft (R := R) (S := R) (A := ℬ) (B := ℬ)

noncomputable def kw_lrComul_incR : (ℬ) →ₐ[R] (ℬ) ⊗[R] (ℬ) :=
  Algebra.TensorProduct.includeRight (R := R) (A := ℬ) (B := ℬ)

noncomputable def kw_lrComul_tensorProj : P₆ →ₐ[R] (ℬ) ⊗[R] (ℬ) :=
  aeval (Sum.elim
    (fun i => kw_lrComul_incL W
      (Ideal.Quotient.mk (projModelHomogeneousIdealCR W.toProjective).toIdeal (X i)))
    (fun i => kw_lrComul_incR W
      (Ideal.Quotient.mk (projModelHomogeneousIdealCR W.toProjective).toIdeal (X i))))

theorem kw_lrComul_tensorProj_rename_inl :
    (kw_lrComul_tensorProj W).comp (rename Sum.inl)
      = (kw_lrComul_incL W).comp
          (Ideal.Quotient.mkₐ R (projModelHomogeneousIdealCR W.toProjective).toIdeal) := by
  refine MvPolynomial.algHom_ext fun i => ?_
  simp only [AlgHom.comp_apply, kw_lrComul_tensorProj, rename_X, aeval_X, Sum.elim_inl,
    Ideal.Quotient.mkₐ_eq_mk]

theorem kw_lrComul_tensorProj_rename_inr :
    (kw_lrComul_tensorProj W).comp (rename Sum.inr)
      = (kw_lrComul_incR W).comp
          (Ideal.Quotient.mkₐ R (projModelHomogeneousIdealCR W.toProjective).toIdeal) := by
  refine MvPolynomial.algHom_ext fun i => ?_
  simp only [AlgHom.comp_apply, kw_lrComul_tensorProj, rename_X, aeval_X, Sum.elim_inr,
    Ideal.Quotient.mkₐ_eq_mk]

theorem kw_lrComul_mk_polynomial_eq_zero :
    Ideal.Quotient.mk (projModelHomogeneousIdealCR W.toProjective).toIdeal
      W.toProjective.polynomial = 0 :=
  Ideal.Quotient.eq_zero_iff_mem.mpr (Ideal.mem_span_singleton_self _)

theorem kw_lrComul_tensorProj_WP₁ : kw_lrComul_tensorProj W WP₁ = 0 := by
  have h := DFunLike.congr_fun (kw_lrComul_tensorProj_rename_inl W) W.toProjective.polynomial
  simp only [AlgHom.comp_apply, Ideal.Quotient.mkₐ_eq_mk] at h
  show kw_lrComul_tensorProj W (rename Sum.inl W.toProjective.polynomial) = 0
  rw [h, kw_lrComul_mk_polynomial_eq_zero, map_zero]

theorem kw_lrComul_tensorProj_WP₂ : kw_lrComul_tensorProj W WP₂ = 0 := by
  have h := DFunLike.congr_fun (kw_lrComul_tensorProj_rename_inr W) W.toProjective.polynomial
  simp only [AlgHom.comp_apply, Ideal.Quotient.mkₐ_eq_mk] at h
  show kw_lrComul_tensorProj W (rename Sum.inr W.toProjective.polynomial) = 0
  rw [h, kw_lrComul_mk_polynomial_eq_zero, map_zero]

noncomputable def kw_lrComul_biToTensor : (ℬ²) →ₐ[R] (ℬ) ⊗[R] (ℬ) :=
  Ideal.Quotient.liftₐ (kw_lrComul_biIdeal W).toIdeal (kw_lrComul_tensorProj W)
    (fun a ha => by
      have hle : Ideal.span {WP₁, WP₂} ≤ RingHom.ker (kw_lrComul_tensorProj W).toRingHom :=
        Ideal.span_le.mpr (by
          rintro p (rfl | hp)
          · exact kw_lrComul_tensorProj_WP₁ W
          · rw [Set.mem_singleton_iff] at hp; subst hp; exact kw_lrComul_tensorProj_WP₂ W)
      exact hle ha)

end TensorBridge

end WeierstrassProjModel

end

end MEGA_KwLRAddQuotientGradedHom_lean

section MEGA_KwLRSymQuotientGradedHom_lean
set_option autoImplicit false
set_option linter.unusedSimpArgs false

noncomputable section

open MvPolynomial WeierstrassCurve HomogeneousIdealQuotientGrading ProjWeierstrassCubicPrime
open scoped TensorProduct

namespace WeierstrassProjModel

attribute [local instance] MvPolynomial.gradedAlgebra

universe u

variable {R : Type u} [CommRing R] (W : WeierstrassCurve R)

local notation "P₆" => MvPolynomial (Fin 3 ⊕ Fin 3) R
local notation "ℬ" => ProjModelRingCR W.toProjective
local notation "ℬ²" => KwLRBiRing W

def kw_lrSym_vec : Fin 3 → P₆ := ![kw_lrSym_X W, kw_lrSym_Y W, kw_lrSym_Z W]

theorem kw_lrSym_vec_isHomogeneous (k : Fin 3) : (kw_lrSym_vec W k).IsHomogeneous 4 := by
  fin_cases k
  · exact kw_lrSym_X_isHomogeneous W
  · exact kw_lrSym_Y_isHomogeneous W
  · exact kw_lrSym_Z_isHomogeneous W

def kw_lrSym_substHom : MvPolynomial (Fin 3) R →ₐ[R] P₆ := aeval (kw_lrSym_vec W)

@[simp]
theorem kw_lrSym_substHom_X (k : Fin 3) :
    kw_lrSym_substHom W (X k) = kw_lrSym_vec W k := aeval_X _ _

theorem kw_lrSym_substHom_isHomogeneous {p : MvPolynomial (Fin 3) R} {n : ℕ}
    (hp : p.IsHomogeneous n) : (kw_lrSym_substHom W p).IsHomogeneous (4 * n) :=
  hp.aeval (kw_lrSym_vec W) (kw_lrSym_vec_isHomogeneous W)

theorem kw_lrSym_substHom_polynomial_mem :
    kw_lrSym_substHom W W.toProjective.polynomial ∈ (kw_lrComul_biIdeal W).toIdeal := by
  exact kw_lrSym_onCurve_mem_span W

noncomputable def kw_lrSym_comulHom : (ℬ) →ₐ[R] (ℬ²) :=
  Ideal.Quotient.liftₐ (projModelHomogeneousIdealCR W.toProjective).toIdeal
    ((Ideal.Quotient.mkₐ R (kw_lrComul_biIdeal W).toIdeal).comp (kw_lrSym_substHom W))
    (fun a ha => by
      refine (Ideal.Quotient.eq_zero_iff_mem).mpr ?_
      have hle : Ideal.span {W.toProjective.polynomial}
          ≤ (kw_lrComul_biIdeal W).toIdeal.comap (kw_lrSym_substHom W).toRingHom :=
        Ideal.span_le.mpr
          (Set.singleton_subset_iff.mpr (kw_lrSym_substHom_polynomial_mem W))
      exact hle ha)

theorem kw_lrSym_comulHom_mk (a : MvPolynomial (Fin 3) R) :
    kw_lrSym_comulHom W
        (Ideal.Quotient.mk (projModelHomogeneousIdealCR W.toProjective).toIdeal a)
      = Ideal.Quotient.mk (kw_lrComul_biIdeal W).toIdeal (kw_lrSym_substHom W a) := by
  rfl

theorem kw_lrSym_comulHom_mk_X (k : Fin 3) :
    kw_lrSym_comulHom W
        (Ideal.Quotient.mk (projModelHomogeneousIdealCR W.toProjective).toIdeal (X k))
      = Ideal.Quotient.mk (kw_lrComul_biIdeal W).toIdeal (kw_lrSym_vec W k) := by
  rw [kw_lrSym_comulHom_mk, kw_lrSym_substHom_X]

theorem kw_lrSym_comulHom_graded {n : ℕ} {x : ℬ}
    (hx : x ∈ projModelGradingCR W.toProjective n) :
    kw_lrSym_comulHom W x ∈ kw_lrComul_biGrading W (4 * n) := by
  obtain ⟨a, ha, rfl⟩ := (mem_quotGradingSubmodule_iff _ _).mp hx
  show Ideal.Quotient.mk (kw_lrComul_biIdeal W).toIdeal (kw_lrSym_substHom W a)
    ∈ kw_lrComul_biGrading W (4 * n)
  exact mk_mem_quotGradingSubmodule _ _
    ((mem_homogeneousSubmodule _ _).mpr
      (kw_lrSym_substHom_isHomogeneous W ((mem_homogeneousSubmodule _ _).mp ha)))

end WeierstrassProjModel

end

end MEGA_KwLRSymQuotientGradedHom_lean

section MEGA_KwLRChartHomAway_lean
set_option autoImplicit false

noncomputable section

open MvPolynomial WeierstrassCurve HomogeneousLocalization HomogeneousIdealQuotientGrading

namespace WeierstrassProjModel

attribute [local instance] MvPolynomial.gradedAlgebra

universe u

variable {R : Type u} [CommRing R] (W : WeierstrassCurve R)

set_option quotPrecheck false in
local notation "ℬ" => ProjModelRingCR W.toProjective
set_option quotPrecheck false in
local notation "ℬ²" => KwLRBiRing W
set_option quotPrecheck false in
local notation "mk₃" => Ideal.Quotient.mk (projModelHomogeneousIdealCR W.toProjective).toIdeal
set_option quotPrecheck false in
local notation "mk₆" => Ideal.Quotient.mk (kw_lrComul_biIdeal W).toIdeal

instance kw_lrChart_biGrading_gradedAlgebra :
    GradedAlgebra (kw_lrComul_biGrading W) := inferInstance

theorem kw_lrChart_mkX_mem_one (k : Fin 3) :
    mk₃ (X k : MvPolynomial (Fin 3) R) ∈ projModelGradingCR W.toProjective 1 :=
  mk_mem_quotGradingSubmodule _ _ ((mem_homogeneousSubmodule _ _).mpr (isHomogeneous_X R k))

theorem kw_lrChart_mkAdd_mem_four (k : Fin 3) :
    mk₆ (kw_lrAdd_vec W k) ∈ kw_lrComul_biGrading W 4 :=
  mk_mem_quotGradingSubmodule _ _
    ((mem_homogeneousSubmodule _ _).mpr (kw_lrAdd_vec_isHomogeneous W k))

set_option quotPrecheck false in

local notation "𝒜" k => HomogeneousLocalization.Away (projModelGradingCR W.toProjective)
  (Ideal.Quotient.mk (projModelHomogeneousIdealCR W.toProjective).toIdeal
    (X k : MvPolynomial (Fin 3) R))

set_option quotPrecheck false in

local notation "𝒜²" k => HomogeneousLocalization.Away (kw_lrComul_biGrading W)
  (Ideal.Quotient.mk (kw_lrComul_biIdeal W).toIdeal (kw_lrAdd_vec W k))

theorem kw_lrChart_comulHom_mkX_pow (k : Fin 3) (n : ℕ) :
    kw_lrAdd_comulHom W (mk₃ (X k : MvPolynomial (Fin 3) R) ^ n)
      = mk₆ (kw_lrAdd_vec W k) ^ n := by
  rw [map_pow, kw_lrAdd_comulHom_mk_X]

theorem kw_lrChart_powers_comap_le (k : Fin 3) :
    Submonoid.powers (mk₃ (X k : MvPolynomial (Fin 3) R))
      ≤ (Submonoid.powers (mk₆ (kw_lrAdd_vec W k))).comap
          (kw_lrAdd_comulHom W).toRingHom := by
  rintro a ⟨n, rfl⟩
  exact ⟨n, (kw_lrChart_comulHom_mkX_pow W k n).symm⟩

noncomputable def kw_lrChart_locMap (k : Fin 3) :
    Localization.Away (mk₃ (X k : MvPolynomial (Fin 3) R))
      →+* Localization.Away (mk₆ (kw_lrAdd_vec W k)) :=
  IsLocalization.map _ (kw_lrAdd_comulHom W).toRingHom (kw_lrChart_powers_comap_le W k)

noncomputable def kw_lrChart_aux (k : Fin 3) :
    (𝒜 k) →+* Localization.Away (mk₆ (kw_lrAdd_vec W k)) :=
  (kw_lrChart_locMap W k).comp
    (algebraMap (𝒜 k) (Localization.Away (mk₃ (X k : MvPolynomial (Fin 3) R))))

theorem kw_lrChart_aux_mk (k : Fin 3) (n : ℕ) (a : ℬ)
    (ha : a ∈ projModelGradingCR W.toProjective (n • 1)) :
    kw_lrChart_aux W k
        (HomogeneousLocalization.Away.mk (projModelGradingCR W.toProjective)
          (kw_lrChart_mkX_mem_one W k) n a ha)
      = Localization.mk (kw_lrAdd_comulHom W a)
          (⟨mk₆ (kw_lrAdd_vec W k) ^ n, n, rfl⟩
            : Submonoid.powers (mk₆ (kw_lrAdd_vec W k))) := by
  show kw_lrChart_locMap W k
      (HomogeneousLocalization.Away.mk _ (kw_lrChart_mkX_mem_one W k) n a ha).val = _
  rw [HomogeneousLocalization.Away.val_mk, Localization.mk_eq_mk', kw_lrChart_locMap,
    IsLocalization.map_mk', ← Localization.mk_eq_mk']
  congr 1
  exact Subtype.ext (kw_lrChart_comulHom_mkX_pow W k n)

noncomputable def kw_lrChart_witness (k : Fin 3) (n : ℕ) (a : ℬ)
    (ha : a ∈ projModelGradingCR W.toProjective (n • 1)) : (𝒜² k) :=
  HomogeneousLocalization.Away.mk (kw_lrComul_biGrading W)
    (kw_lrChart_mkAdd_mem_four W k) n (kw_lrAdd_comulHom W a)
    (by
      have ha' : a ∈ projModelGradingCR W.toProjective n := by simpa using ha
      have h4n : kw_lrAdd_comulHom W a ∈ kw_lrComul_biGrading W (4 * n) :=
        kw_lrAdd_comulHom_graded W ha'
      simpa [smul_eq_mul, Nat.mul_comm] using h4n)

theorem kw_lrChart_witness_val (k : Fin 3) (n : ℕ) (a : ℬ)
    (ha : a ∈ projModelGradingCR W.toProjective (n • 1)) :
    (kw_lrChart_witness W k n a ha).val
      = kw_lrChart_aux W k
          (HomogeneousLocalization.Away.mk (projModelGradingCR W.toProjective)
            (kw_lrChart_mkX_mem_one W k) n a ha) := by
  rw [kw_lrChart_aux_mk]; rfl

theorem kw_lrChart_aux_range_subset (k : Fin 3) :
    Set.range (kw_lrChart_aux W k)
      ⊆ Set.range (algebraMap (𝒜² k) (Localization.Away (mk₆ (kw_lrAdd_vec W k)))) := by
  rintro _ ⟨z, rfl⟩
  obtain ⟨n, a, ha, rfl⟩ := HomogeneousLocalization.Away.mk_surjective
    (projModelGradingCR W.toProjective) (kw_lrChart_mkX_mem_one W k) z
  exact ⟨kw_lrChart_witness W k n a ha,
    (HomogeneousLocalization.algebraMap_apply _).trans (kw_lrChart_witness_val W k n a ha)⟩

theorem kw_lrChart_aux_range_le (k : Fin 3) :
    (kw_lrChart_aux W k).range
      ≤ (algebraMap (𝒜² k) (Localization.Away (mk₆ (kw_lrAdd_vec W k)))).range := by
  rintro _ ⟨z, rfl⟩
  exact kw_lrChart_aux_range_subset W k ⟨z, rfl⟩

noncomputable def kw_lrChart_away (k : Fin 3) : (𝒜 k) →+* (𝒜² k) := by
  let e := RingEquiv.ofLeftInverse
    (f := algebraMap (𝒜² k) (Localization.Away (mk₆ (kw_lrAdd_vec W k))))
    (h := (HomogeneousLocalization.val_injective _).hasLeftInverse.choose_spec)
  exact RingHom.comp (e.symm.toRingHom.comp (Subring.inclusion (kw_lrChart_aux_range_le W k)))
    (kw_lrChart_aux W k).rangeRestrict

end WeierstrassProjModel

end

end MEGA_KwLRChartHomAway_lean

section MEGA_KwProjPullbackAwayCoverCR_lean
set_option autoImplicit false

noncomputable section

open MvPolynomial HomogeneousLocalization

namespace WeierstrassProjModel

attribute [local instance] MvPolynomial.gradedAlgebra

universe u

variable (R : Type u) [CommRing R]

section ChartStructureMap

variable (V : WeierstrassCurve.Projective R)

set_option quotPrecheck false in

local notation "𝒜" i =>
  HomogeneousLocalization.Away (projModelGradingCR V)
    (Ideal.Quotient.mk (projModelHomogeneousIdealCR V).toIdeal (X i : MvPolynomial (Fin 3) R))

@[reducible] noncomputable def kw_pbac_awayAlgebra (i : Fin 3) : Algebra R (𝒜 i) :=
  ((fromZeroRingHom (projModelGradingCR V) _).comp
    (algebraMap R ((projModelGradingCR V) 0))).toAlgebra

end ChartStructureMap

end WeierstrassProjModel

end
end MEGA_KwProjPullbackAwayCoverCR_lean

section MEGA_A1_Properness_lean

set_option autoImplicit false

namespace WeierstrassProjModel

open HomogeneousIdealQuotientGrading

section FiniteTypeEngine

variable {ι A σ τ : Type*}
variable [CommRing A] [AddMonoid ι]
variable [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ι → σ) [SetLike.GradedMonoid 𝒜]
variable (I : Ideal A)
variable [SetLike τ (A ⧸ I)] [AddSubmonoidClass τ (A ⧸ I)] (ℬ : ι → τ) [SetLike.GradedMonoid ℬ]

theorem finiteType_gradeZero_quotient_of_mk_mem
    (hmem0 : ∀ a : A, a ∈ 𝒜 0 → Ideal.Quotient.mk I a ∈ ℬ 0)
    (hFT : Algebra.FiniteType (𝒜 0) A) :
    Algebra.FiniteType (ℬ 0) (A ⧸ I) := by
  classical
  obtain ⟨s, hs⟩ := hFT.out
  refine ⟨⟨s.image (Ideal.Quotient.mk I), ?_⟩⟩
  rw [eq_top_iff]
  rintro x -
  obtain ⟨a, rfl⟩ := Ideal.Quotient.mk_surjective x
  have ha : a ∈ Algebra.adjoin (𝒜 0) (s : Set A) := hs.ge Algebra.mem_top
  induction ha using Algebra.adjoin_induction with
  | mem y hy =>
      exact Algebra.subset_adjoin (by
        simpa using Finset.mem_image_of_mem (Ideal.Quotient.mk I) hy)
  | algebraMap r =>
      have hr : Ideal.Quotient.mk I (algebraMap (𝒜 0) A r) ∈ ℬ 0 := hmem0 _ r.2
      exact Subalgebra.algebraMap_mem _ (⟨_, hr⟩ : ℬ 0)
  | add x y hx hy ihx ihy =>
      rw [map_add]; exact add_mem ihx ihy
  | mul x y hx hy ihx ihy =>
      rw [map_mul]; exact mul_mem ihx ihy

end FiniteTypeEngine

section BaseUpgrade

variable {ι R A : Type*}
variable [CommRing R] [CommRing A] [Algebra R A] [AddMonoid ι]
variable (𝒜 : ι → Submodule R A) [SetLike.GradedMonoid 𝒜]

theorem isScalarTower_gradeZero : IsScalarTower R (𝒜 0) A :=
  IsScalarTower.of_algebraMap_eq fun _ => rfl

theorem finiteType_gradeZero_of_finiteType_base (hFT : Algebra.FiniteType R A) :
    Algebra.FiniteType (𝒜 0) A := by
  haveI : IsScalarTower R (𝒜 0) A := isScalarTower_gradeZero 𝒜
  haveI := hFT
  exact Algebra.FiniteType.of_restrictScalars_finiteType R (𝒜 0) A

end BaseUpgrade

section QuotGradingSubmoduleDegreeZero

variable {ι R A : Type*}
variable [CommRing R] [CommRing A] [Algebra R A] [AddMonoid ι]
variable (𝒜 : ι → Submodule R A) [SetLike.GradedMonoid 𝒜]
variable (I : Ideal A)

theorem quotGradingSubmodule_degreeZero_finiteType (hFT : Algebra.FiniteType (𝒜 0) A) :
    Algebra.FiniteType ((quotGradingSubmodule 𝒜 I) 0) (A ⧸ I) :=
  finiteType_gradeZero_quotient_of_mk_mem 𝒜 I (quotGradingSubmodule 𝒜 I)
    (fun _ ha => mk_mem_quotGradingSubmodule 𝒜 I ha) hFT

instance quotGradingSubmoduleDegreeZeroFiniteType [Algebra.FiniteType (𝒜 0) A] :
    Algebra.FiniteType ((quotGradingSubmodule 𝒜 I) 0) (A ⧸ I) :=
  quotGradingSubmodule_degreeZero_finiteType 𝒜 I ‹_›

end QuotGradingSubmoduleDegreeZero

section MvPolynomialVenue

open MvPolynomial

instance homogeneousSubmoduleDegreeZeroFiniteType (σs R : Type*) [Finite σs] [CommRing R] :
    Algebra.FiniteType ((homogeneousSubmodule σs R) 0) (MvPolynomial σs R) :=
  finiteType_gradeZero_of_finiteType_base (homogeneousSubmodule σs R) inferInstance

end MvPolynomialVenue

section DegreeZeroEngine

variable {ι R A : Type*}
variable [CommRing R] [CommRing A] [Algebra R A] [AddMonoid ι]
variable (𝒜 : ι → Submodule R A) [SetLike.GradedMonoid 𝒜]
variable (I : Ideal A)

end DegreeZeroEngine

section PolynomialDegreeZero

open MvPolynomial

theorem mem_homogeneousSubmodule_zero_iff_exists_C {σ R : Type*} [CommSemiring R]
    {p : MvPolynomial σ R} :
    p ∈ homogeneousSubmodule σ R 0 ↔ ∃ r : R, C r = p := by
  constructor
  · intro hp
    rw [homogeneousSubmodule_zero] at hp
    obtain ⟨r, hr⟩ := Submodule.mem_one.mp hp
    exact ⟨r, by rwa [← algebraMap_eq]⟩
  · rintro ⟨r, rfl⟩
    exact (mem_homogeneousSubmodule _ _).mpr (isHomogeneous_C _ _)

variable (σ R : Type*) [CommSemiring R]

end PolynomialDegreeZero

section ConstantCoeffKernel

open MvPolynomial

variable {σ R : Type*} [CommSemiring R]

theorem constantCoeff_eq_zero_of_isHomogeneous_of_ne_zero {p : MvPolynomial σ R} {n : ℕ}
    (hp : p.IsHomogeneous n) (hn : n ≠ 0) :
    constantCoeff p = 0 :=
  hp.coeff_eq_zero (by simpa using hn.symm)

theorem span_le_ker_constantCoeff_of_forall_constantCoeff_eq_zero
    {S : Set (MvPolynomial σ R)} (h : ∀ p ∈ S, constantCoeff p = 0) :
    Ideal.span S ≤ RingHom.ker (constantCoeff : MvPolynomial σ R →+* R) :=
  Ideal.span_le.mpr fun p hp => RingHom.mem_ker.mpr (h p hp)

theorem span_le_ker_constantCoeff_of_forall_isHomogeneous_pos
    {S : Set (MvPolynomial σ R)} (h : ∀ p ∈ S, ∃ n : ℕ, n ≠ 0 ∧ p.IsHomogeneous n) :
    Ideal.span S ≤ RingHom.ker (constantCoeff : MvPolynomial σ R →+* R) :=
  span_le_ker_constantCoeff_of_forall_constantCoeff_eq_zero fun p hp => by
    obtain ⟨n, hn, hhom⟩ := h p hp
    exact constantCoeff_eq_zero_of_isHomogeneous_of_ne_zero hhom hn

end ConstantCoeffKernel

section DegreeZeroIdentification

open MvPolynomial

variable {σ R : Type*} [CommRing R]
variable (I : Ideal (MvPolynomial σ R))

lemma quotGradingSubmodule_degreeZero_algebraMap_coe (r : R) :
    ((algebraMap R ((quotGradingSubmodule (homogeneousSubmodule σ R) I) 0) r :
        (quotGradingSubmodule (homogeneousSubmodule σ R) I) 0) : MvPolynomial σ R ⧸ I)
      = Ideal.Quotient.mk I (C r) := rfl

theorem quotGradingSubmodule_degreeZero_algebraMap_surjective :
    Function.Surjective
      (algebraMap R ((quotGradingSubmodule (homogeneousSubmodule σ R) I) 0)) := by
  rintro ⟨b, hb⟩
  obtain ⟨p, hp, rfl⟩ := (mem_quotGradingSubmodule_iff (homogeneousSubmodule σ R) I).mp hb
  obtain ⟨r, rfl⟩ := mem_homogeneousSubmodule_zero_iff_exists_C.mp hp
  exact ⟨r, Subtype.ext rfl⟩

theorem quotGradingSubmodule_degreeZero_algebraMap_injective
    (hI : I ≤ RingHom.ker (constantCoeff : MvPolynomial σ R →+* R)) :
    Function.Injective
      (algebraMap R ((quotGradingSubmodule (homogeneousSubmodule σ R) I) 0)) := by
  intro r s hrs
  have hval : Ideal.Quotient.mk I (C r) = Ideal.Quotient.mk I (C s) :=
    congrArg Subtype.val hrs
  have hsub : (C r - C s : MvPolynomial σ R) ∈ I := Ideal.Quotient.eq.mp hval
  rw [← map_sub] at hsub
  have h0 : constantCoeff (C (r - s) : MvPolynomial σ R) = 0 := RingHom.mem_ker.mp (hI hsub)
  rw [constantCoeff_C] at h0
  exact sub_eq_zero.mp h0

theorem quotGradingSubmodule_degreeZero_algebraMap_bijective
    (hI : I ≤ RingHom.ker (constantCoeff : MvPolynomial σ R →+* R)) :
    Function.Bijective
      (algebraMap R ((quotGradingSubmodule (homogeneousSubmodule σ R) I) 0)) :=
  ⟨quotGradingSubmodule_degreeZero_algebraMap_injective I hI,
   quotGradingSubmodule_degreeZero_algebraMap_surjective I⟩

end DegreeZeroIdentification

end WeierstrassProjModel

noncomputable section

open AlgebraicGeometry CategoryTheory MvPolynomial HomogeneousLocalization
open HomogeneousIdealQuotientGrading ProjWeierstrassCubicPrime

namespace WeierstrassProjModel

attribute [local instance] MvPolynomial.gradedAlgebra

variable {R : Type*} [CommRing R]

theorem projModelIdeal_le_ker_constantCoeffCR (V : WeierstrassCurve.Projective R) :
    (projModelHomogeneousIdealCR V).toIdeal
      ≤ RingHom.ker (constantCoeff : MvPolynomial (Fin 3) R →+* R) :=
  span_le_ker_constantCoeff_of_forall_isHomogeneous_pos fun p hp => by
    rcases Set.mem_singleton_iff.mp hp with rfl
    exact ⟨3, by decide, isHomogeneous_polynomial V⟩

theorem projModel_degreeZero_algebraMap_bijectiveCR (V : WeierstrassCurve.Projective R) :
    Function.Bijective (algebraMap R ((projModelGradingCR V) 0)) :=
  quotGradingSubmodule_degreeZero_algebraMap_bijective (projModelHomogeneousIdealCR V).toIdeal
    (projModelIdeal_le_ker_constantCoeffCR V)

def projModelDegreeZeroRingEquivCR (V : WeierstrassCurve.Projective R) :
    R ≃+* ((projModelGradingCR V) 0) :=
  RingEquiv.ofBijective (algebraMap R ((projModelGradingCR V) 0))
    (projModel_degreeZero_algebraMap_bijectiveCR V)

def projModelSpecDegreeZeroIsoCR (V : WeierstrassCurve.Projective R) :
    Spec (CommRingCat.of ((projModelGradingCR V) 0)) ≅ Spec (CommRingCat.of R) where
  hom := Spec.map (CommRingCat.ofHom (algebraMap R ((projModelGradingCR V) 0)))
  inv := Spec.map (CommRingCat.ofHom
    ((projModelDegreeZeroRingEquivCR V).symm : ((projModelGradingCR V) 0) →+* R))
  hom_inv_id := by
    rw [← Spec.map_comp, ← CommRingCat.ofHom_comp,
      show (algebraMap R ((projModelGradingCR V) 0)).comp
          ((projModelDegreeZeroRingEquivCR V).symm : ((projModelGradingCR V) 0) →+* R)
        = RingHom.id ((projModelGradingCR V) 0) from
        RingHom.ext fun x => (projModelDegreeZeroRingEquivCR V).apply_symm_apply x,
      CommRingCat.ofHom_id, Spec.map_id]
  inv_hom_id := by
    rw [← Spec.map_comp, ← CommRingCat.ofHom_comp,
      show ((projModelDegreeZeroRingEquivCR V).symm : ((projModelGradingCR V) 0) →+* R).comp
          (algebraMap R ((projModelGradingCR V) 0))
        = RingHom.id R from
        RingHom.ext fun x => (projModelDegreeZeroRingEquivCR V).symm_apply_apply x,
      CommRingCat.ofHom_id, Spec.map_id]

instance projModel_isIso_spec_mapCR (V : WeierstrassCurve.Projective R) :
    IsIso (Spec.map (CommRingCat.ofHom (algebraMap R ((projModelGradingCR V) 0)))) :=
  inferInstanceAs (IsIso (projModelSpecDegreeZeroIsoCR V).hom)

instance isProper_projModelStrCR (V : WeierstrassCurve.Projective R) :
    IsProper (projModelStrCR V) := by
  show IsProper (Proj.toSpecZero (projModelGradingCR V) ≫
    Spec.map (CommRingCat.ofHom (algebraMap R ((projModelGradingCR V) 0))))
  infer_instance

end WeierstrassProjModel

end

end MEGA_A1_Properness_lean

section MEGA_KwLRChartHomToTensor_lean
set_option autoImplicit false
set_option linter.unusedSimpArgs false
set_option maxHeartbeats 1600000

noncomputable section

open MvPolynomial WeierstrassCurve HomogeneousLocalization HomogeneousIdealQuotientGrading
open scoped TensorProduct

namespace WeierstrassProjModel

attribute [local instance] MvPolynomial.gradedAlgebra
attribute [local instance] kw_pbac_awayAlgebra

universe u

variable {R : Type u} [CommRing R] (W : WeierstrassCurve R)

set_option quotPrecheck false in
local notation "ℬ" => ProjModelRingCR W.toProjective
set_option quotPrecheck false in
local notation "ℬ²" => KwLRBiRing W
set_option quotPrecheck false in
local notation "mk₃" => Ideal.Quotient.mk (projModelHomogeneousIdealCR W.toProjective).toIdeal
set_option quotPrecheck false in
local notation "mk₆" => Ideal.Quotient.mk (kw_lrComul_biIdeal W).toIdeal
set_option quotPrecheck false in
local notation "𝒜" i => HomogeneousLocalization.Away (projModelGradingCR W.toProjective)
  (Ideal.Quotient.mk (projModelHomogeneousIdealCR W.toProjective).toIdeal
    (X i : MvPolynomial (Fin 3) R))
set_option quotPrecheck false in
local notation "𝒜²" k => HomogeneousLocalization.Away (kw_lrComul_biGrading W)
  (Ideal.Quotient.mk (kw_lrComul_biIdeal W).toIdeal (kw_lrAdd_vec W k))

noncomputable def kw_lrChart_gen (i m : Fin 3) : (𝒜 i) :=
  HomogeneousLocalization.mk
    ⟨1, ⟨mk₃ (X m : MvPolynomial (Fin 3) R), kw_lrChart_mkX_mem_one W m⟩,
        ⟨mk₃ (X i : MvPolynomial (Fin 3) R), kw_lrChart_mkX_mem_one W i⟩, ⟨1, pow_one _⟩⟩

theorem kw_lrChart_gen_val (i m : Fin 3) :
    (kw_lrChart_gen W i m).val
      = Localization.mk (mk₃ (X m : MvPolynomial (Fin 3) R))
          (⟨mk₃ (X i : MvPolynomial (Fin 3) R), 1, pow_one _⟩
            : Submonoid.powers (mk₃ (X i : MvPolynomial (Fin 3) R))) := rfl

noncomputable def kw_lrChart_dehom (i : Fin 3) :
    MvPolynomial (Fin 3) R →ₐ[R] (𝒜 i) :=
  aeval (kw_lrChart_gen W i)

theorem kw_lrChart_dehom_C_val (i : Fin 3) (r : R) :
    (kw_lrChart_dehom W i (C r)).val
      = Localization.mk (mk₃ (C r : MvPolynomial (Fin 3) R))
          (1 : Submonoid.powers (mk₃ (X i : MvPolynomial (Fin 3) R))) := by
  rw [kw_lrChart_dehom, aeval_C]
  show (fromZeroRingHom (projModelGradingCR W.toProjective) _
      (algebraMap R ((projModelGradingCR W.toProjective) 0) r)).val = _

  simp only [fromZeroRingHom, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
    HomogeneousLocalization.val_mk, quotGradingSubmodule_degreeZero_algebraMap_coe]
  rfl

theorem kw_lrChart_dehom_X_val (i m : Fin 3) :
    (kw_lrChart_dehom W i (X m)).val
      = Localization.mk (mk₃ (X m : MvPolynomial (Fin 3) R))
          (⟨mk₃ (X i : MvPolynomial (Fin 3) R), 1, pow_one _⟩
            : Submonoid.powers (mk₃ (X i : MvPolynomial (Fin 3) R))) := by
  rw [kw_lrChart_dehom, aeval_X, kw_lrChart_gen_val]

theorem kw_lrChart_dehom_monomial_val (i : Fin 3) (d : Fin 3 →₀ ℕ) (c : R) (n : ℕ)
    (hn : d 0 + d 1 + d 2 = n) :
    (kw_lrChart_dehom W i (monomial d c)).val
      = Localization.mk (mk₃ (monomial d c : MvPolynomial (Fin 3) R))
          (⟨mk₃ (X i : MvPolynomial (Fin 3) R) ^ n, n, rfl⟩
            : Submonoid.powers (mk₃ (X i : MvPolynomial (Fin 3) R))) := by
  have hmon : (monomial d c : MvPolynomial (Fin 3) R)
      = C c * (X 0 ^ d 0 * X 1 ^ d 1 * X 2 ^ d 2) := by
    rw [MvPolynomial.monomial_eq, Finsupp.prod_fintype _ _ fun _ => pow_zero _,
      Fin.prod_univ_three]

  rw [hmon]
  simp only [map_mul, map_pow, HomogeneousLocalization.val_mul, HomogeneousLocalization.val_pow,
    kw_lrChart_dehom_C_val, kw_lrChart_dehom_X_val,
    Localization.mk_pow, Localization.mk_mul, one_mul, mul_one, one_pow]
  rw [Localization.mk_eq_mk_iff, Localization.r_iff_exists]
  refine ⟨1, ?_⟩

  have key : (mk₃ (X i : MvPolynomial (Fin 3) R)) ^ n
      = (mk₃ (X i : MvPolynomial (Fin 3) R)) ^ d 0
        * (mk₃ (X i : MvPolynomial (Fin 3) R)) ^ d 1
        * (mk₃ (X i : MvPolynomial (Fin 3) R)) ^ d 2 := by
    rw [← pow_add, ← pow_add, hn]
  push_cast [key]
  ring

set_option maxSynthPendingDepth 3 in

theorem kw_lrChart_dehom_isHomogeneous_val (i : Fin 3) (n : ℕ)
    (p : MvPolynomial (Fin 3) R) (hp : p.IsHomogeneous n) :
    (kw_lrChart_dehom W i p).val
      = Localization.mk (mk₃ p)
          (⟨mk₃ (X i : MvPolynomial (Fin 3) R) ^ n, n, rfl⟩
            : Submonoid.powers (mk₃ (X i : MvPolynomial (Fin 3) R))) := by
  conv_lhs => rw [MvPolynomial.as_sum p]
  conv_rhs => rw [MvPolynomial.as_sum p]

  haveI : AddMonoidHomClass
      ((𝒜 i) →+* Localization (Submonoid.powers (mk₃ (X i : MvPolynomial (Fin 3) R))))
      (𝒜 i) (Localization (Submonoid.powers (mk₃ (X i : MvPolynomial (Fin 3) R)))) :=
    RingHomClass.toAddMonoidHomClass
  rw [map_sum, ← HomogeneousLocalization.algebraMap_apply, map_sum, map_sum, Localization.mk_sum]
  refine Finset.sum_congr rfl fun d hd => ?_
  rw [HomogeneousLocalization.algebraMap_apply]
  have hdeg : d.degree = n := by
    by_contra hne; exact MvPolynomial.mem_support_iff.mp hd (hp.coeff_eq_zero hne)
  exact kw_lrChart_dehom_monomial_val W i d (MvPolynomial.coeff d p) n
    (by rw [← hdeg, Finsupp.degree_eq_sum, Fin.sum_univ_three])

theorem kw_lrChart_mk_mem_of_isHomogeneous (n : ℕ) (p : MvPolynomial (Fin 3) R)
    (hp : p.IsHomogeneous n) :
    mk₃ p ∈ projModelGradingCR W.toProjective (n • 1) := by
  rw [nsmul_one, Nat.cast_id]
  exact mk_mem_quotGradingSubmodule _ _ ((mem_homogeneousSubmodule _ _).mpr hp)

theorem kw_lrChart_dehom_isHomogeneous (i : Fin 3) (n : ℕ)
    (p : MvPolynomial (Fin 3) R) (hp : p.IsHomogeneous n) :
    kw_lrChart_dehom W i p
      = HomogeneousLocalization.Away.mk (projModelGradingCR W.toProjective)
          (kw_lrChart_mkX_mem_one W i) n (mk₃ p)
          (kw_lrChart_mk_mem_of_isHomogeneous W n p hp) := by
  apply HomogeneousLocalization.val_injective
  rw [kw_lrChart_dehom_isHomogeneous_val W i n p hp, HomogeneousLocalization.Away.val_mk]

theorem kw_lrChart_dehom_polynomial (i : Fin 3) :
    kw_lrChart_dehom W i W.toProjective.polynomial = 0 := by
  rw [kw_lrChart_dehom_isHomogeneous W i 3 _
    (ProjWeierstrassCubicPrime.isHomogeneous_polynomial W.toProjective)]
  refine HomogeneousLocalization.mk_eq_zero_of_num _ ?_
  exact Subtype.ext (kw_lrComul_mk_polynomial_eq_zero W)

section TensorEv

variable (i j : Fin 3)

noncomputable def kw_lrChart_inL : (𝒜 i) →ₐ[R] (𝒜 i) ⊗[R] (𝒜 j) :=
  Algebra.TensorProduct.includeLeft (R := R) (S := R) (A := 𝒜 i) (B := 𝒜 j)

noncomputable def kw_lrChart_inR : (𝒜 j) →ₐ[R] (𝒜 i) ⊗[R] (𝒜 j) :=
  Algebra.TensorProduct.includeRight (R := R) (A := 𝒜 i) (B := 𝒜 j)

noncomputable def kw_lrChart_ev :
    MvPolynomial (Fin 3 ⊕ Fin 3) R →ₐ[R] (𝒜 i) ⊗[R] (𝒜 j) :=
  aeval (Sum.elim (fun m => kw_lrChart_inL W i j (kw_lrChart_gen W i m))
                  (fun m => kw_lrChart_inR W i j (kw_lrChart_gen W j m)))

theorem kw_lrChart_ev_rename_inl :
    (kw_lrChart_ev W i j).comp (rename Sum.inl)
      = (kw_lrChart_inL W i j).comp (kw_lrChart_dehom W i) := by
  refine MvPolynomial.algHom_ext fun m => ?_
  simp only [AlgHom.comp_apply, kw_lrChart_ev, rename_X, aeval_X, Sum.elim_inl,
    kw_lrChart_dehom]

theorem kw_lrChart_ev_rename_inr :
    (kw_lrChart_ev W i j).comp (rename Sum.inr)
      = (kw_lrChart_inR W i j).comp (kw_lrChart_dehom W j) := by
  refine MvPolynomial.algHom_ext fun m => ?_
  simp only [AlgHom.comp_apply, kw_lrChart_ev, rename_X, aeval_X, Sum.elim_inr,
    kw_lrChart_dehom]

theorem kw_lrChart_ev_WP₁ : kw_lrChart_ev W i j (kw_lrAdd_WP₁ W) = 0 := by
  have h := DFunLike.congr_fun (kw_lrChart_ev_rename_inl W i j) W.toProjective.polynomial
  simp only [AlgHom.comp_apply] at h
  show kw_lrChart_ev W i j (rename Sum.inl W.toProjective.polynomial) = 0
  rw [h, kw_lrChart_dehom_polynomial, map_zero]

theorem kw_lrChart_ev_WP₂ : kw_lrChart_ev W i j (kw_lrAdd_WP₂ W) = 0 := by
  have h := DFunLike.congr_fun (kw_lrChart_ev_rename_inr W i j) W.toProjective.polynomial
  simp only [AlgHom.comp_apply] at h
  show kw_lrChart_ev W i j (rename Sum.inr W.toProjective.polynomial) = 0
  rw [h, kw_lrChart_dehom_polynomial, map_zero]

noncomputable def kw_lrChart_ev' : (ℬ²) →ₐ[R] (𝒜 i) ⊗[R] (𝒜 j) :=
  Ideal.Quotient.liftₐ (kw_lrComul_biIdeal W).toIdeal (kw_lrChart_ev W i j)
    (fun a ha => by
      have hle : Ideal.span {kw_lrAdd_WP₁ W, kw_lrAdd_WP₂ W}
          ≤ RingHom.ker (kw_lrChart_ev W i j).toRingHom :=
        Ideal.span_le.mpr (by
          rintro p (rfl | hp)
          · exact kw_lrChart_ev_WP₁ W i j
          · rw [Set.mem_singleton_iff] at hp; subst hp; exact kw_lrChart_ev_WP₂ W i j)
      exact hle ha)

end TensorEv

section ToTensor

variable (i j k : Fin 3)

instance kw_lrChart_tensorCommRing : CommRing ((𝒜 i) ⊗[R] (𝒜 j)) := inferInstance

noncomputable def kw_lrChart_u : (𝒜 i) ⊗[R] (𝒜 j) :=
  kw_lrChart_ev' W i j (mk₆ (kw_lrAdd_vec W k))

theorem kw_lrChart_powers_ev'_comap_le :
    Submonoid.powers (mk₆ (kw_lrAdd_vec W k))
      ≤ (Submonoid.powers (kw_lrChart_u W i j k)).comap
          (kw_lrChart_ev' W i j).toRingHom := by
  rintro a ⟨n, rfl⟩
  exact ⟨n, by rw [map_pow]; rfl⟩

noncomputable def kw_lrChart_toTensorLoc :
    Localization.Away (mk₆ (kw_lrAdd_vec W k))
      →+* Localization.Away (kw_lrChart_u W i j k) :=
  IsLocalization.map _ (kw_lrChart_ev' W i j).toRingHom
    (kw_lrChart_powers_ev'_comap_le W i j k)

noncomputable def kw_lrChart_toTensor :
    (𝒜² k) →+* Localization.Away (kw_lrChart_u W i j k) :=
  (kw_lrChart_toTensorLoc W i j k).comp
    (algebraMap (𝒜² k) (Localization.Away (mk₆ (kw_lrAdd_vec W k))))

end ToTensor

section Composite

variable (i j k : Fin 3)

noncomputable def kw_lrChart_tensor :
    (𝒜 k) →+* Localization.Away (kw_lrChart_u W i j k) :=
  (kw_lrChart_toTensor W i j k).comp (kw_lrChart_away W k)

end Composite

end WeierstrassProjModel

end

end MEGA_KwLRChartHomToTensor_lean

section MEGA_KwLRSymChartHomAway_lean
set_option autoImplicit false

noncomputable section

open MvPolynomial WeierstrassCurve HomogeneousLocalization HomogeneousIdealQuotientGrading

namespace WeierstrassProjModel

attribute [local instance] MvPolynomial.gradedAlgebra

universe u

variable {R : Type u} [CommRing R] (W : WeierstrassCurve R)

set_option quotPrecheck false in
local notation "ℬ" => ProjModelRingCR W.toProjective
set_option quotPrecheck false in
local notation "ℬ²" => KwLRBiRing W
set_option quotPrecheck false in
local notation "mk₃" => Ideal.Quotient.mk (projModelHomogeneousIdealCR W.toProjective).toIdeal
set_option quotPrecheck false in
local notation "mk₆" => Ideal.Quotient.mk (kw_lrComul_biIdeal W).toIdeal

theorem kw_lrSymChart_mkSym_mem_four (k : Fin 3) :
    mk₆ (kw_lrSym_vec W k) ∈ kw_lrComul_biGrading W 4 :=
  mk_mem_quotGradingSubmodule _ _
    ((mem_homogeneousSubmodule _ _).mpr (kw_lrSym_vec_isHomogeneous W k))

set_option quotPrecheck false in

local notation "𝒜" k => HomogeneousLocalization.Away (projModelGradingCR W.toProjective)
  (Ideal.Quotient.mk (projModelHomogeneousIdealCR W.toProjective).toIdeal
    (X k : MvPolynomial (Fin 3) R))

set_option quotPrecheck false in

local notation "𝒜²ₛ" k => HomogeneousLocalization.Away (kw_lrComul_biGrading W)
  (Ideal.Quotient.mk (kw_lrComul_biIdeal W).toIdeal (kw_lrSym_vec W k))

theorem kw_lrSymChart_comulHom_mkX_pow (k : Fin 3) (n : ℕ) :
    kw_lrSym_comulHom W (mk₃ (X k : MvPolynomial (Fin 3) R) ^ n)
      = mk₆ (kw_lrSym_vec W k) ^ n := by
  rw [map_pow, kw_lrSym_comulHom_mk_X]

theorem kw_lrSymChart_powers_comap_le (k : Fin 3) :
    Submonoid.powers (mk₃ (X k : MvPolynomial (Fin 3) R))
      ≤ (Submonoid.powers (mk₆ (kw_lrSym_vec W k))).comap
          (kw_lrSym_comulHom W).toRingHom := by
  rintro a ⟨n, rfl⟩
  exact ⟨n, (kw_lrSymChart_comulHom_mkX_pow W k n).symm⟩

noncomputable def kw_lrSymChart_locMap (k : Fin 3) :
    Localization.Away (mk₃ (X k : MvPolynomial (Fin 3) R))
      →+* Localization.Away (mk₆ (kw_lrSym_vec W k)) :=
  IsLocalization.map _ (kw_lrSym_comulHom W).toRingHom (kw_lrSymChart_powers_comap_le W k)

noncomputable def kw_lrSymChart_aux (k : Fin 3) :
    (𝒜 k) →+* Localization.Away (mk₆ (kw_lrSym_vec W k)) :=
  (kw_lrSymChart_locMap W k).comp
    (algebraMap (𝒜 k) (Localization.Away (mk₃ (X k : MvPolynomial (Fin 3) R))))

theorem kw_lrSymChart_aux_mk (k : Fin 3) (n : ℕ) (a : ℬ)
    (ha : a ∈ projModelGradingCR W.toProjective (n • 1)) :
    kw_lrSymChart_aux W k
        (HomogeneousLocalization.Away.mk (projModelGradingCR W.toProjective)
          (kw_lrChart_mkX_mem_one W k) n a ha)
      = Localization.mk (kw_lrSym_comulHom W a)
          (⟨mk₆ (kw_lrSym_vec W k) ^ n, n, rfl⟩
            : Submonoid.powers (mk₆ (kw_lrSym_vec W k))) := by
  show kw_lrSymChart_locMap W k
      (HomogeneousLocalization.Away.mk _ (kw_lrChart_mkX_mem_one W k) n a ha).val = _
  rw [HomogeneousLocalization.Away.val_mk, Localization.mk_eq_mk', kw_lrSymChart_locMap,
    IsLocalization.map_mk', ← Localization.mk_eq_mk']
  congr 1
  exact Subtype.ext (kw_lrSymChart_comulHom_mkX_pow W k n)

noncomputable def kw_lrSymChart_witness (k : Fin 3) (n : ℕ) (a : ℬ)
    (ha : a ∈ projModelGradingCR W.toProjective (n • 1)) : (𝒜²ₛ k) :=
  HomogeneousLocalization.Away.mk (kw_lrComul_biGrading W)
    (kw_lrSymChart_mkSym_mem_four W k) n (kw_lrSym_comulHom W a)
    (by
      have ha' : a ∈ projModelGradingCR W.toProjective n := by simpa using ha
      have h4n : kw_lrSym_comulHom W a ∈ kw_lrComul_biGrading W (4 * n) :=
        kw_lrSym_comulHom_graded W ha'
      simpa [smul_eq_mul, Nat.mul_comm] using h4n)

theorem kw_lrSymChart_witness_val (k : Fin 3) (n : ℕ) (a : ℬ)
    (ha : a ∈ projModelGradingCR W.toProjective (n • 1)) :
    (kw_lrSymChart_witness W k n a ha).val
      = kw_lrSymChart_aux W k
          (HomogeneousLocalization.Away.mk (projModelGradingCR W.toProjective)
            (kw_lrChart_mkX_mem_one W k) n a ha) := by
  rw [kw_lrSymChart_aux_mk]; rfl

theorem kw_lrSymChart_aux_range_subset (k : Fin 3) :
    Set.range (kw_lrSymChart_aux W k)
      ⊆ Set.range (algebraMap (𝒜²ₛ k) (Localization.Away (mk₆ (kw_lrSym_vec W k)))) := by
  rintro _ ⟨z, rfl⟩
  obtain ⟨n, a, ha, rfl⟩ := HomogeneousLocalization.Away.mk_surjective
    (projModelGradingCR W.toProjective) (kw_lrChart_mkX_mem_one W k) z
  exact ⟨kw_lrSymChart_witness W k n a ha,
    (HomogeneousLocalization.algebraMap_apply _).trans (kw_lrSymChart_witness_val W k n a ha)⟩

theorem kw_lrSymChart_aux_range_le (k : Fin 3) :
    (kw_lrSymChart_aux W k).range
      ≤ (algebraMap (𝒜²ₛ k) (Localization.Away (mk₆ (kw_lrSym_vec W k)))).range := by
  rintro _ ⟨z, rfl⟩
  exact kw_lrSymChart_aux_range_subset W k ⟨z, rfl⟩

noncomputable def kw_lrSymChart_away (k : Fin 3) : (𝒜 k) →+* (𝒜²ₛ k) := by
  let e := RingEquiv.ofLeftInverse
    (f := algebraMap (𝒜²ₛ k) (Localization.Away (mk₆ (kw_lrSym_vec W k))))
    (h := (HomogeneousLocalization.val_injective _).hasLeftInverse.choose_spec)
  exact RingHom.comp (e.symm.toRingHom.comp
      (Subring.inclusion (kw_lrSymChart_aux_range_le W k)))
    (kw_lrSymChart_aux W k).rangeRestrict

end WeierstrassProjModel

end
end MEGA_KwLRSymChartHomAway_lean

section MEGA_KwLRSymChartHomToTensor_lean
set_option autoImplicit false
set_option linter.unusedSimpArgs false
set_option maxHeartbeats 1600000

noncomputable section

open MvPolynomial WeierstrassCurve HomogeneousLocalization HomogeneousIdealQuotientGrading
open scoped TensorProduct

namespace WeierstrassProjModel

attribute [local instance] MvPolynomial.gradedAlgebra
attribute [local instance] kw_pbac_awayAlgebra

universe u

variable {R : Type u} [CommRing R] (W : WeierstrassCurve R)

set_option quotPrecheck false in
local notation "ℬ" => ProjModelRingCR W.toProjective
set_option quotPrecheck false in
local notation "mk₆" => Ideal.Quotient.mk (kw_lrComul_biIdeal W).toIdeal
set_option quotPrecheck false in
local notation "𝒜" i => HomogeneousLocalization.Away (projModelGradingCR W.toProjective)
  (Ideal.Quotient.mk (projModelHomogeneousIdealCR W.toProjective).toIdeal
    (X i : MvPolynomial (Fin 3) R))
set_option quotPrecheck false in
local notation "𝒜²ₛ" k => HomogeneousLocalization.Away (kw_lrComul_biGrading W)
  (Ideal.Quotient.mk (kw_lrComul_biIdeal W).toIdeal (kw_lrSym_vec W k))

section ToTensor

variable (i j k : Fin 3)

noncomputable def kw_lrSymChart_u : (𝒜 i) ⊗[R] (𝒜 j) :=
  kw_lrChart_ev' W i j (mk₆ (kw_lrSym_vec W k))

theorem kw_lrSymChart_powers_ev'_comap_le :
    Submonoid.powers (mk₆ (kw_lrSym_vec W k))
      ≤ (Submonoid.powers (kw_lrSymChart_u W i j k)).comap
          (kw_lrChart_ev' W i j).toRingHom := by
  rintro a ⟨n, rfl⟩
  exact ⟨n, by rw [map_pow]; rfl⟩

noncomputable def kw_lrSymChart_toTensorLoc :
    Localization.Away (mk₆ (kw_lrSym_vec W k))
      →+* Localization.Away (kw_lrSymChart_u W i j k) :=
  IsLocalization.map _ (kw_lrChart_ev' W i j).toRingHom
    (kw_lrSymChart_powers_ev'_comap_le W i j k)

noncomputable def kw_lrSymChart_toTensor :
    (𝒜²ₛ k) →+* Localization.Away (kw_lrSymChart_u W i j k) :=
  (kw_lrSymChart_toTensorLoc W i j k).comp
    (algebraMap (𝒜²ₛ k) (Localization.Away (mk₆ (kw_lrSym_vec W k))))

end ToTensor

section Composite

variable (i j k : Fin 3)

noncomputable def kw_lrSymChart_tensor :
    (𝒜 k) →+* Localization.Away (kw_lrSymChart_u W i j k) :=
  (kw_lrSymChart_toTensor W i j k).comp (kw_lrSymChart_away W k)

end Composite

end WeierstrassProjModel

end

end MEGA_KwLRSymChartHomToTensor_lean

section MEGA_KwLRSixUCoverage_lean
set_option autoImplicit false
set_option linter.unusedSimpArgs false
set_option maxHeartbeats 1600000

noncomputable section

open MvPolynomial WeierstrassCurve HomogeneousLocalization
open scoped TensorProduct

namespace WeierstrassProjModel

attribute [local instance] MvPolynomial.gradedAlgebra
attribute [local instance] kw_pbac_awayAlgebra

universe u

variable {R : Type u} [CommRing R] (W : WeierstrassCurve R)

set_option quotPrecheck false in
local notation "𝒜" i => HomogeneousLocalization.Away (projModelGradingCR W.toProjective)
  (Ideal.Quotient.mk (projModelHomogeneousIdealCR W.toProjective).toIdeal
    (X i : MvPolynomial (Fin 3) R))

noncomputable def kw_lrSixU (i j : Fin 3) : Fin 3 ⊕ Fin 3 → (𝒜 i) ⊗[R] (𝒜 j) :=
  Sum.elim (kw_lrChart_u W i j) (kw_lrSymChart_u W i j)

def KwLRSixUCoverage : Prop :=
  ∀ (i j : Fin 3),
    Ideal.span (Set.range (kw_lrSixU W i j)) = (⊤ : Ideal ((𝒜 i) ⊗[R] (𝒜 j)))

end WeierstrassProjModel

end
end MEGA_KwLRSixUCoverage_lean

section MEGA_KwLRPerChartGlue_lean
set_option autoImplicit false
set_option linter.unusedSimpArgs false
set_option maxHeartbeats 1600000

noncomputable section

open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open MvPolynomial WeierstrassCurve HomogeneousLocalization
open scoped TensorProduct

namespace WeierstrassProjModel

attribute [local instance] MvPolynomial.gradedAlgebra
attribute [local instance] kw_pbac_awayAlgebra

universe u

variable {R : Type u} [CommRing R] (W : WeierstrassCurve R)

set_option quotPrecheck false in
local notation "𝒜" i => HomogeneousLocalization.Away (projModelGradingCR W.toProjective)
  (Ideal.Quotient.mk (projModelHomogeneousIdealCR W.toProjective).toIdeal
    (X i : MvPolynomial (Fin 3) R))

set_option quotPrecheck false in
local notation "E" => projModelCR W.toProjective

noncomputable def kw_lrSixU_cover (i j : Fin 3)
    (h : Ideal.span (Set.range (kw_lrSixU W i j)) = ⊤) :
    (Spec (CommRingCat.of ((𝒜 i) ⊗[R] (𝒜 j)))).AffineOpenCover :=
  Scheme.affineOpenCoverOfSpanRangeEqTop (R := .of ((𝒜 i) ⊗[R] (𝒜 j))) (kw_lrSixU W i j) h

section ToE

variable (i j : Fin 3)

noncomputable def kw_lrSixU_toE :
    ∀ l : Fin 3 ⊕ Fin 3,
      Spec (CommRingCat.of (Localization.Away (kw_lrSixU W i j l))) ⟶ E
  | .inl k => Spec.map (CommRingCat.ofHom (kw_lrChart_tensor W i j k))
      ≫ Proj.awayι (projModelGradingCR W.toProjective) _ (kw_lrChart_mkX_mem_one W k) one_pos
  | .inr k => Spec.map (CommRingCat.ofHom (kw_lrSymChart_tensor W i j k))
      ≫ Proj.awayι (projModelGradingCR W.toProjective) _ (kw_lrChart_mkX_mem_one W k) one_pos

end ToE

noncomputable def kw_lrSixU_locMap (i j : Fin 3) (l : Fin 3 ⊕ Fin 3) :
    Spec (CommRingCat.of (Localization.Away (kw_lrSixU W i j l)))
      ⟶ Spec (CommRingCat.of ((𝒜 i) ⊗[R] (𝒜 j))) :=
  Spec.map (CommRingCat.ofHom
    (algebraMap ((𝒜 i) ⊗[R] (𝒜 j)) (Localization.Away (kw_lrSixU W i j l))))

def KwLRPerChartCompat : Prop :=
  ∀ (i j : Fin 3) (l l' : Fin 3 ⊕ Fin 3),
    pullback.fst (kw_lrSixU_locMap W i j l) (kw_lrSixU_locMap W i j l')
        ≫ kw_lrSixU_toE W i j l
      = pullback.snd (kw_lrSixU_locMap W i j l) (kw_lrSixU_locMap W i j l')
        ≫ kw_lrSixU_toE W i j l'

noncomputable def kw_lrPerChart_toE (hcov : KwLRSixUCoverage W)
    (hcompat : KwLRPerChartCompat W) (i j : Fin 3) :
    Spec (CommRingCat.of ((𝒜 i) ⊗[R] (𝒜 j))) ⟶ E :=
  (kw_lrSixU_cover W i j (hcov i j)).openCover.glueMorphisms
    (kw_lrSixU_toE W i j) (hcompat i j)

end WeierstrassProjModel

end
end MEGA_KwLRPerChartGlue_lean

section MEGA_KwProjPullbackAwayCoverCRCover_lean
set_option autoImplicit false

noncomputable section

open AlgebraicGeometry CategoryTheory CategoryTheory.Limits MvPolynomial
open HomogeneousLocalization HomogeneousIdealQuotientGrading
open scoped TensorProduct

namespace WeierstrassProjModel

attribute [local instance] MvPolynomial.gradedAlgebra

universe u

variable (R : Type u) [CommRing R]

section CoverCRPort

variable (V : WeierstrassCurve.Projective R)

open MvPolynomial in

theorem kw_pbac_mk_X_mem_one_CR (i : Fin 3) :
    Ideal.Quotient.mk (projModelHomogeneousIdealCR V).toIdeal
        (X i : MvPolynomial (Fin 3) R)
      ∈ projModelGradingCR V 1 :=
  mk_mem_quotGradingSubmodule _ _ ((mem_homogeneousSubmodule _ _).mpr (isHomogeneous_X R i))

theorem kw_pbac_ambient_irrelevant_le_span_X_CR :
    (HomogeneousIdeal.irrelevant (homogeneousSubmodule (Fin 3) R)).toIdeal
      ≤ Ideal.span (Set.range (X : Fin 3 → MvPolynomial (Fin 3) R)) := by
  classical
  intro p hp
  rw [HomogeneousIdeal.toIdeal_irrelevant, RingHom.mem_ker] at hp
  have hzero : (DirectSum.decompose (homogeneousSubmodule (Fin 3) R) p 0
      : MvPolynomial (Fin 3) R) = 0 := by
    rw [← GradedRing.projZeroRingHom_apply]; exact hp
  have hc0 : MvPolynomial.coeff 0 p = 0 := by
    conv_lhs => rw [← DirectSum.sum_support_decompose (homogeneousSubmodule (Fin 3) R) p]
    rw [MvPolynomial.coeff_sum]
    refine Finset.sum_eq_zero fun n _ => ?_
    by_cases h0 : n = 0
    · rw [h0, hzero, MvPolynomial.coeff_zero]
    · have hmem : ((DirectSum.decompose (homogeneousSubmodule (Fin 3) R) p n
          : MvPolynomial (Fin 3) R)).IsHomogeneous n :=
        (MvPolynomial.mem_homogeneousSubmodule _ _).mp (SetLike.coe_mem _)
      exact hmem.coeff_eq_zero (by simpa using Ne.symm h0)
  rw [← Set.image_univ, MvPolynomial.mem_ideal_span_X_image]
  intro m hm
  have hmne : m ≠ 0 := by rintro rfl; exact (MvPolynomial.mem_support_iff.mp hm) hc0
  obtain ⟨l, hl⟩ := Finsupp.ne_iff.mp hmne
  exact ⟨l, Set.mem_univ l, by simpa using hl⟩

theorem kw_pbac_irrelevant_le_span_mk_X_CR :
    (HomogeneousIdeal.irrelevant (projModelGradingCR V)).toIdeal
      ≤ Ideal.span (Set.range fun i : Fin 3 =>
          Ideal.Quotient.mk (projModelHomogeneousIdealCR V).toIdeal
            (X i : MvPolynomial (Fin 3) R)) := by
  intro z hz
  rw [HomogeneousIdeal.toIdeal_irrelevant, RingHom.mem_ker,
    GradedRing.projZeroRingHom_apply] at hz
  obtain ⟨p, rfl⟩ := Ideal.Quotient.mk_surjective z
  rw [decompose_quotGradingSubmodule_mk_apply (homogeneousSubmodule (Fin 3) R)
      (projModelHomogeneousIdealCR V) p 0] at hz
  have hrewrite : Ideal.Quotient.mk (projModelHomogeneousIdealCR V).toIdeal p
      = Ideal.Quotient.mk (projModelHomogeneousIdealCR V).toIdeal
          (p - (DirectSum.decompose (homogeneousSubmodule (Fin 3) R) p 0
            : MvPolynomial (Fin 3) R)) := by
    rw [map_sub, hz, sub_zero]
  rw [hrewrite]
  have hirr : (p - (DirectSum.decompose (homogeneousSubmodule (Fin 3) R) p 0
        : MvPolynomial (Fin 3) R))
      ∈ (HomogeneousIdeal.irrelevant (homogeneousSubmodule (Fin 3) R)).toIdeal := by
    rw [HomogeneousIdeal.toIdeal_irrelevant, RingHom.mem_ker,
      GradedRing.projZeroRingHom_apply, DirectSum.decompose_sub,
      DirectSum.decompose_coe, DirectSum.sub_apply, DirectSum.of_eq_same,
      AddSubgroupClass.coe_sub, sub_self]
  have hmem := kw_pbac_ambient_irrelevant_le_span_X_CR R hirr
  have hmap : Ideal.Quotient.mk (projModelHomogeneousIdealCR V).toIdeal
        (p - (DirectSum.decompose (homogeneousSubmodule (Fin 3) R) p 0
          : MvPolynomial (Fin 3) R))
      ∈ Ideal.map (Ideal.Quotient.mk (projModelHomogeneousIdealCR V).toIdeal)
          (Ideal.span (Set.range (X : Fin 3 → MvPolynomial (Fin 3) R))) :=
    Ideal.mem_map_of_mem _ hmem
  rwa [Ideal.map_span, ← Set.range_comp] at hmap

noncomputable def projModelAffineOpenCoverCR :
    Scheme.AffineOpenCover (projModelCR V) :=
  Proj.affineOpenCoverOfIrrelevantLESpan (projModelGradingCR V)
    (fun i : Fin 3 =>
      Ideal.Quotient.mk (projModelHomogeneousIdealCR V).toIdeal (X i : MvPolynomial (Fin 3) R))
    (m := fun _ => 1)
    (fun i => kw_pbac_mk_X_mem_one_CR R V i) (fun _ => Nat.one_pos)
    (kw_pbac_irrelevant_le_span_mk_X_CR R V)

end CoverCRPort

section ChartStructureMap

variable (V : WeierstrassCurve.Projective R)

set_option quotPrecheck false in

local notation "𝒜" i =>
  HomogeneousLocalization.Away (projModelGradingCR V)
    (Ideal.Quotient.mk (projModelHomogeneousIdealCR V).toIdeal (X i : MvPolynomial (Fin 3) R))

attribute [local instance] kw_pbac_awayAlgebra

theorem kw_pbac_awayι_comp_projModelStrCR (i : Fin 3) :
    Proj.awayι (projModelGradingCR V) _ (kw_pbac_mk_X_mem_one_CR R V i) one_pos
        ≫ projModelStrCR V
      = Spec.map (CommRingCat.ofHom (algebraMap R (𝒜 i))) := by
  unfold projModelStrCR
  rw [← Category.assoc, Proj.awayι_toSpecZero, ← Spec.map_comp]
  rfl

end ChartStructureMap

section PullbackCover

variable (V : WeierstrassCurve.Projective R)

noncomputable def kwProjPullbackOpenCoverCR :
    (pullback (projModelStrCR V) (projModelStrCR V)).OpenCover :=
  Scheme.Pullback.openCoverOfLeftRight
    (projModelAffineOpenCoverCR R V).openCover
    (projModelAffineOpenCoverCR R V).openCover
    (projModelStrCR V) (projModelStrCR V)

end PullbackCover

section ChartIso

variable (V : WeierstrassCurve.Projective R)

set_option quotPrecheck false in

local notation "𝒜" i =>
  HomogeneousLocalization.Away (projModelGradingCR V)
    (Ideal.Quotient.mk (projModelHomogeneousIdealCR V).toIdeal (X i : MvPolynomial (Fin 3) R))

attribute [local instance] kw_pbac_awayAlgebra

noncomputable def kwProjPullbackChartIsoCR (i j : Fin 3) :
    (kwProjPullbackOpenCoverCR R V).X (i, j)
      ≅ Spec (CommRingCat.of ((𝒜 i) ⊗[R] (𝒜 j))) :=
  pullback.congrHom (kw_pbac_awayι_comp_projModelStrCR R V i)
      (kw_pbac_awayι_comp_projModelStrCR R V j)
    ≪≫ pullbackSpecIso R (𝒜 i) (𝒜 j)

end ChartIso

end WeierstrassProjModel

end

end MEGA_KwProjPullbackAwayCoverCRCover_lean

section MEGA_KwLROuterGlue_lean
set_option autoImplicit false
set_option maxHeartbeats 1600000

noncomputable section

open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open MvPolynomial WeierstrassCurve HomogeneousLocalization
open scoped TensorProduct

namespace WeierstrassProjModel

attribute [local instance] MvPolynomial.gradedAlgebra
attribute [local instance] kw_pbac_awayAlgebra

universe u

variable {R : Type u} [CommRing R] (W : WeierstrassCurve R)

set_option quotPrecheck false in
local notation "E" => projModelCR W.toProjective

noncomputable def kw_lrOuter_toE (hcov : KwLRSixUCoverage W)
    (hcompat : KwLRPerChartCompat W) :
    ∀ ij, (kwProjPullbackOpenCoverCR R W.toProjective).X ij ⟶ E :=
  fun ij => (kwProjPullbackChartIsoCR R W.toProjective ij.1 ij.2).hom
            ≫ kw_lrPerChart_toE W hcov hcompat ij.1 ij.2

def KwLROuterCompat : Prop :=
  ∀ (hcov : KwLRSixUCoverage W) (hcompat : KwLRPerChartCompat W)
    (ij ij' : Fin 3 × Fin 3),
    pullback.fst ((kwProjPullbackOpenCoverCR R W.toProjective).f ij)
                 ((kwProjPullbackOpenCoverCR R W.toProjective).f ij')
        ≫ kw_lrOuter_toE W hcov hcompat ij
      = pullback.snd ((kwProjPullbackOpenCoverCR R W.toProjective).f ij)
                     ((kwProjPullbackOpenCoverCR R W.toProjective).f ij')
        ≫ kw_lrOuter_toE W hcov hcompat ij'

noncomputable def kw_lrAddMorphism (hcov : KwLRSixUCoverage W)
    (hcompat : KwLRPerChartCompat W) (houter : KwLROuterCompat W) :
    pullback (projModelStrCR W.toProjective) (projModelStrCR W.toProjective) ⟶ E :=
  (kwProjPullbackOpenCoverCR R W.toProjective).glueMorphisms
    (kw_lrOuter_toE W hcov hcompat) (houter hcov hcompat)

end WeierstrassProjModel

end
end MEGA_KwLROuterGlue_lean

section MEGA_KwLRAddNegDiagZeroNegMor_lean
set_option autoImplicit false
set_option maxHeartbeats 1600000

noncomputable section

open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
open MvPolynomial WeierstrassCurve HomogeneousLocalization HomogeneousIdealQuotientGrading
open scoped TensorProduct

namespace WeierstrassProjModel

attribute [local instance] MvPolynomial.gradedAlgebra

universe u

variable {R : Type u} [CommRing R] (W : WeierstrassCurve R)

set_option quotPrecheck false in
local notation "𝒜" i => HomogeneousLocalization.Away (projModelGradingCR W.toProjective)
  (Ideal.Quotient.mk (projModelHomogeneousIdealCR W.toProjective).toIdeal
    (X i : MvPolynomial (Fin 3) R))
set_option quotPrecheck false in
local notation "E" => projModelCR W.toProjective
set_option quotPrecheck false in
local notation "π" => projModelStrCR W.toProjective
set_option quotPrecheck false in
local notation "ℬ" => ProjModelRingCR W.toProjective
set_option quotPrecheck false in
local notation "mk₃" => Ideal.Quotient.mk (projModelHomogeneousIdealCR W.toProjective).toIdeal

section NegMor

def kw_lrAddNegDiag_negSubstGen : Fin 3 → MvPolynomial (Fin 3) R :=
  ![X 0, -X 1 - C W.a₁ * X 0 - C W.a₃ * X 2, X 2]

def kw_lrAddNegDiag_negSubst : MvPolynomial (Fin 3) R →ₐ[R] MvPolynomial (Fin 3) R :=
  aeval (kw_lrAddNegDiag_negSubstGen W)

local notation "negSubst" => kw_lrAddNegDiag_negSubst W

theorem kw_lrAddNegDiag_negSubstGen_isHomogeneous (m : Fin 3) :
    (kw_lrAddNegDiag_negSubstGen W m).IsHomogeneous 1 := by
  fin_cases m
  · exact isHomogeneous_X R 0
  · refine ((((isHomogeneous_X R 1).neg).sub ?_).sub ?_)
    · exact (isHomogeneous_C _ W.a₁).mul (isHomogeneous_X R 0)
    · exact (isHomogeneous_C _ W.a₃).mul (isHomogeneous_X R 2)
  · exact isHomogeneous_X R 2

theorem kw_lrAddNegDiag_negSubst_isHomogeneous {p : MvPolynomial (Fin 3) R} {n : ℕ}
    (hp : p.IsHomogeneous n) : (negSubst p).IsHomogeneous n := by
  have key : (aeval (kw_lrAddNegDiag_negSubstGen W) p).IsHomogeneous (1 * n) :=
    hp.aeval _ (kw_lrAddNegDiag_negSubstGen_isHomogeneous W)
  simpa [kw_lrAddNegDiag_negSubst, one_mul] using key

theorem kw_lrAddNegDiag_negSubst_polynomial :
    negSubst W.toProjective.polynomial = W.toProjective.polynomial := by
  simp only [kw_lrAddNegDiag_negSubst, WeierstrassCurve.Projective.polynomial,
    WeierstrassCurve.toProjective, map_sub, map_add, map_mul, map_pow, aeval_C, aeval_X,
    kw_lrAddNegDiag_negSubstGen, Matrix.cons_val_zero, Matrix.cons_val_one,
    Matrix.head_cons, Matrix.cons_val_two, Matrix.tail_cons, MvPolynomial.algebraMap_eq]
  ring

theorem kw_lrAddNegDiag_negSubst_mapSpan :
    Ideal.map (negSubst : MvPolynomial (Fin 3) R →+* _)
        (Ideal.span {W.toProjective.polynomial})
      = Ideal.span {W.toProjective.polynomial} := by
  rw [Ideal.map_span, Set.image_singleton]
  exact congrArg (Ideal.span {·}) (kw_lrAddNegDiag_negSubst_polynomial W)

def kw_lrAddNegDiag_negQuotHom : ℬ →+* ℬ :=
  Ideal.Quotient.lift (projModelHomogeneousIdealCR W.toProjective).toIdeal
    ((Ideal.Quotient.mk (projModelHomogeneousIdealCR W.toProjective).toIdeal).comp
      (negSubst : MvPolynomial (Fin 3) R →+* _))
    (fun _ ha => Ideal.Quotient.eq_zero_iff_mem.mpr
      ((Ideal.map_le_iff_le_comap.mp (kw_lrAddNegDiag_negSubst_mapSpan W).le)
        (projModelHomogeneousIdealCR_toIdeal W.toProjective ▸ ha)))

def kw_lrAddNegDiag_negGradedHom :
    projModelGradingCR W.toProjective →+*ᵍ projModelGradingCR W.toProjective where
  toRingHom := kw_lrAddNegDiag_negQuotHom W
  map_mem {i x} hx := by
    obtain ⟨a, ha, rfl⟩ := (mem_quotGradingSubmodule_iff _ _).mp hx
    exact mk_mem_quotGradingSubmodule _ _
      ((mem_homogeneousSubmodule _ _).mpr
        (kw_lrAddNegDiag_negSubst_isHomogeneous W
          ((mem_homogeneousSubmodule _ _).mp ha)))

local notation "negGradedHom" => kw_lrAddNegDiag_negGradedHom W

set_option linter.unnecessarySeqFocus false in

theorem kw_lrAddNegDiag_negSubst_comp_self :
    (negSubst).comp negSubst = AlgHom.id R (MvPolynomial (Fin 3) R) := by
  refine MvPolynomial.algHom_ext fun m => ?_
  fin_cases m <;>
    simp [kw_lrAddNegDiag_negSubst, kw_lrAddNegDiag_negSubstGen,
      map_sub, map_neg, map_mul] <;>
    ring

theorem kw_lrAddNegDiag_negGradedHom_comp_self :
    (negGradedHom : ℬ →+* ℬ).comp negGradedHom = RingHom.id ℬ := by
  refine Ideal.Quotient.ringHom_ext ?_
  exact RingHom.ext fun a => congrArg mk₃
    (DFunLike.congr_fun (kw_lrAddNegDiag_negSubst_comp_self W) a)

theorem kw_lrAddNegDiag_negGradedHom_map_proj (n : ℕ) (x : ℬ) :
    GradedRing.proj (projModelGradingCR W.toProjective) n (negGradedHom x)
      = negGradedHom (GradedRing.proj (projModelGradingCR W.toProjective) n x) := by
  classical
  conv_lhs => rw [← DirectSum.sum_support_decompose (projModelGradingCR W.toProjective) x]
  conv_rhs => rw [← DirectSum.sum_support_decompose (projModelGradingCR W.toProjective) x]
  simp only [map_sum]
  refine Finset.sum_congr rfl fun m _ => ?_
  have hy : (↑((DirectSum.decompose (projModelGradingCR W.toProjective) x) m) : ℬ)
      ∈ projModelGradingCR W.toProjective m := SetLike.coe_mem _
  have hfy : negGradedHom
        (↑((DirectSum.decompose (projModelGradingCR W.toProjective) x) m) : ℬ)
      ∈ projModelGradingCR W.toProjective m := (negGradedHom).map_mem hy
  rcases eq_or_ne m n with h | h
  · subst h
    rw [GradedRing.proj_apply, DirectSum.decompose_of_mem_same _ hfy,
      GradedRing.proj_apply, DirectSum.decompose_of_mem_same _ hy]
  · rw [GradedRing.proj_apply, DirectSum.decompose_of_mem_ne _ hfy h,
      GradedRing.proj_apply, DirectSum.decompose_of_mem_ne _ hy h, map_zero]

theorem kw_lrAddNegDiag_negGradedHom_irrelevant_le :
    HomogeneousIdeal.irrelevant (projModelGradingCR W.toProjective)
      ≤ (HomogeneousIdeal.irrelevant (projModelGradingCR W.toProjective)).map
          negGradedHom := by
  intro x hx
  have heq : x = negGradedHom (negGradedHom x) :=
    (RingHom.congr_fun (kw_lrAddNegDiag_negGradedHom_comp_self W) x).symm
  rw [heq]
  refine Ideal.mem_map_of_mem _ ?_
  show negGradedHom x ∈ HomogeneousIdeal.irrelevant (projModelGradingCR W.toProjective)
  rw [HomogeneousIdeal.mem_irrelevant_iff] at hx ⊢
  rw [kw_lrAddNegDiag_negGradedHom_map_proj W 0 x, hx, map_zero]

def kw_lrAddNegDiag_negMor : E ⟶ E :=
  Proj.map negGradedHom (kw_lrAddNegDiag_negGradedHom_irrelevant_le W)

local notation "negMor" => kw_lrAddNegDiag_negMor W

end NegMor

section GeneralNaturality

variable {A : Type u} [CommRing A] {σ : Type u} [SetLike σ A] [AddSubgroupClass σ A]
variable {𝒢 : ℕ → σ} [GradedRing 𝒢]

end GeneralNaturality

section NegMor2

local notation "negGradedHom" => kw_lrAddNegDiag_negGradedHom W
local notation "negMor" => kw_lrAddNegDiag_negMor W
local notation "negSubst" => kw_lrAddNegDiag_negSubst W

end NegMor2

section PolyIdentity

noncomputable def kw_lrAddNegDiag_evalNeg :
    MvPolynomial (Fin 3 ⊕ Fin 3) R →ₐ[R] MvPolynomial (Fin 3) R :=
  aeval (Sum.elim (kw_lrAddNegDiag_negSubstGen W) X)

set_option quotPrecheck false in
local notation "evalNeg" => kw_lrAddNegDiag_evalNeg W

macro "simp_evalNeg" : tactic =>
  `(tactic| simp only [map_add, map_sub, map_mul, map_neg, map_pow, map_ofNat, map_one,
    kw_lrAddNegDiag_evalNeg_C, kw_lrAddNegDiag_evalNeg_inr,
    kw_lrAddNegDiag_evalNeg_inl, kw_lrAddNegDiag_negSubstGen,
    Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons,
    Matrix.cons_val_two, Matrix.tail_cons])

end PolyIdentity

end WeierstrassProjModel

end

end MEGA_KwLRAddNegDiagZeroNegMor_lean

section MEGA_KwProjWeierstrassRelGroupLawConstruct_lean
set_option autoImplicit false

noncomputable section

open AlgebraicGeometry CategoryTheory CategoryTheory.Limits WeierstrassCurve

universe u

namespace WeierstrassProjModel

open WeierstrassProjModel NeronModelInfra HomogeneousIdealQuotientGrading

attribute [local instance] MvPolynomial.gradedAlgebra

variable (R : Type u) [CommRing R]

section ZeroSection

variable (W : WeierstrassCurve R)

open MvPolynomial in

theorem kw_mk_X1_mem_one_CR :
    Ideal.Quotient.mk (projModelHomogeneousIdealCR W.toProjective).toIdeal
        (X 1 : MvPolynomial (Fin 3) R)
      ∈ projModelGradingCR W.toProjective 1 :=
  mk_mem_quotGradingSubmodule _ _ ((mem_homogeneousSubmodule _ _).mpr (isHomogeneous_X R 1))

open MvPolynomial in

def kwYEvalRingHom : ProjModelRingCR W.toProjective →+* R :=
  Ideal.Quotient.lift _ (MvPolynomial.eval ![(0 : R), 1, 0]) fun a ha => by
    refine (Ideal.span_le.mpr ?_ : Ideal.span _ ≤ RingHom.ker _)
      (projModelHomogeneousIdealCR_toIdeal W.toProjective ▸ ha)
    simp only [Set.singleton_subset_iff, SetLike.mem_coe, RingHom.mem_ker]

    exact WeierstrassCurve.Projective.equation_zero

open MvPolynomial in

theorem kwYEvalRingHom_mk_X1 :
    kwYEvalRingHom R W (Ideal.Quotient.mk _ (X 1 : MvPolynomial (Fin 3) R)) = 1 := by
  show (MvPolynomial.eval ![(0 : R), 1, 0]) (X 1) = 1
  simp

def kwYChartEval :
    HomogeneousLocalization.Away (projModelGradingCR W.toProjective)
      (Ideal.Quotient.mk _ (MvPolynomial.X 1 : MvPolynomial (Fin 3) R)) →+* R :=
  (IsLocalization.Away.lift (g := kwYEvalRingHom R W)
      (Ideal.Quotient.mk _ (MvPolynomial.X 1 : MvPolynomial (Fin 3) R))
      (kwYEvalRingHom_mk_X1 R W ▸ isUnit_one)).comp
    (algebraMap
      (HomogeneousLocalization.Away (projModelGradingCR W.toProjective)
        (Ideal.Quotient.mk _ (MvPolynomial.X 1 : MvPolynomial (Fin 3) R)))
      (Localization.Away
        (Ideal.Quotient.mk (projModelHomogeneousIdealCR W.toProjective).toIdeal
          (MvPolynomial.X 1 : MvPolynomial (Fin 3) R))))

open MvPolynomial in

theorem kwYEvalRingHom_comp_algebraMap :
    (kwYEvalRingHom R W).comp (algebraMap R (ProjModelRingCR W.toProjective)) = RingHom.id R :=
  RingHom.ext fun r => by
    show (MvPolynomial.eval ![(0 : R), 1, 0]) (C r) = r
    exact MvPolynomial.eval_C _

theorem kwYChartEval_section :
    (kwYChartEval R W).comp
      ((HomogeneousLocalization.fromZeroRingHom (projModelGradingCR W.toProjective) _).comp
        (algebraMap R (projModelGradingCR W.toProjective 0))) = RingHom.id R := by

  refine RingHom.ext fun r => ?_
  simp only [RingHom.comp_apply, RingHom.id_apply, kwYChartEval,
    HomogeneousLocalization.algebraMap_apply]

  have hval :
      (HomogeneousLocalization.fromZeroRingHom (projModelGradingCR W.toProjective) _
          (algebraMap R (projModelGradingCR W.toProjective 0) r)).val
        = algebraMap (ProjModelRingCR W.toProjective)
            (Localization.Away
              (Ideal.Quotient.mk (projModelHomogeneousIdealCR W.toProjective).toIdeal
                (MvPolynomial.X 1 : MvPolynomial (Fin 3) R)))
            (algebraMap R (ProjModelRingCR W.toProjective) r) := by

    rfl
  rw [hval, IsLocalization.Away.lift, IsLocalization.lift_eq]
  exact RingHom.congr_fun (kwYEvalRingHom_comp_algebraMap R W) r

def kwZeroSect : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) (projModelStrCR W.toProjective) :=
  ⟨Spec.map (CommRingCat.ofHom (kwYChartEval R W)) ≫
    Proj.awayι (projModelGradingCR W.toProjective) _ (kw_mk_X1_mem_one_CR R W) one_pos,
   by
    simp only [projModelStrCR, Category.assoc]
    rw [← Category.assoc (Proj.awayι ..), Proj.awayι_toSpecZero, ← Spec.map_comp,
      ← Spec.map_comp, ← CommRingCat.ofHom_comp, ← CommRingCat.ofHom_comp,
      kwYChartEval_section, CommRingCat.ofHom_id, Spec.map_id]⟩

end ZeroSection

section AddLawData

variable (W : WeierstrassCurve R)

local notation "E" => projModelCR W.toProjective
local notation "π" => projModelStrCR W.toProjective

end AddLawData

section Assembly

end Assembly

end WeierstrassProjModel

end
end MEGA_KwProjWeierstrassRelGroupLawConstruct_lean

section MEGA_KwLRAffinePtTorsionBridge_lean

set_option autoImplicit false

noncomputable section

open AlgebraicGeometry CategoryTheory CategoryTheory.Limits WeierstrassCurve

namespace WeierstrassProjModel

open WeierstrassProjModel NeronModelInfra

attribute [local instance] Classical.propDecidable

universe u

variable {R : Type u} [CommRing R] (W : WeierstrassCurve R)

section Bridge

variable (F : Type u) [Field F] [Algebra R F]

abbrev kw_lrAptb_tF : Spec (CommRingCat.of F) ⟶ Spec (CommRingCat.of R) :=
  Spec.map (CommRingCat.ofHom (algebraMap R F))

section Engine

end Engine

end Bridge

end WeierstrassProjModel

end

end MEGA_KwLRAffinePtTorsionBridge_lean

section MEGA_KwLRAffinePtSetEquiv_lean
set_option autoImplicit false
set_option maxHeartbeats 3200000

noncomputable section

open AlgebraicGeometry CategoryTheory CategoryTheory.Limits WeierstrassCurve MvPolynomial
open HomogeneousLocalization HomogeneousIdealQuotientGrading
open scoped WeierstrassCurve.Projective

namespace WeierstrassProjModel

open WeierstrassProjModel NeronModelInfra

attribute [local instance] Classical.propDecidable
attribute [local instance] MvPolynomial.gradedAlgebra
attribute [local instance] kw_pbac_awayAlgebra

universe u

variable {R : Type u} [CommRing R] (W : WeierstrassCurve R)
variable (F : Type u) [Field F] [Algebra R F]

set_option quotPrecheck false in
local notation "mk₃" => Ideal.Quotient.mk (projModelHomogeneousIdealCR W.toProjective).toIdeal
set_option quotPrecheck false in
local notation "𝒜" i => HomogeneousLocalization.Away (projModelGradingCR W.toProjective)
  (mk₃ (X i : MvPolynomial (Fin 3) R))
set_option quotPrecheck false in
local notation "E" => projModelCR W.toProjective
set_option quotPrecheck false in
local notation "π" => projModelStrCR W.toProjective
set_option quotPrecheck false in
local notation "coverE" => (projModelAffineOpenCoverCR R W.toProjective).openCover
set_option quotPrecheck false in
local notation "gen" => kw_lrChart_gen W
set_option quotPrecheck false in
local notation "dehom" => kw_lrChart_dehom W
set_option quotPrecheck false in
local notation "t_F" => kw_lrAptb_tF (R := R) F

set_option quotPrecheck false in
local notation "awayι₃" i => Proj.awayι (projModelGradingCR W.toProjective)
  (mk₃ (X i : MvPolynomial (Fin 3) R)) (kw_pbac_mk_X_mem_one_CR R W.toProjective i) one_pos

abbrev kw_lrApt_WF : WeierstrassCurve.Projective F := (W.baseChange F).toProjective

set_option quotPrecheck false in
local notation "W_F" => kw_lrApt_WF W F

section ChartClassification

def kw_lrApt_chartEval (i : Fin 3) (ψ : (𝒜 i) →ₐ[R] F) : Fin 3 → F :=
  fun k => ψ (gen i k)

end ChartClassification

section ChartFactorization

end ChartFactorization

section Forward

end Forward

section Nonsingular

variable {F}

end Nonsingular

section Inverse

end Inverse

section Assembly

end Assembly

end WeierstrassProjModel

end
end MEGA_KwLRAffinePtSetEquiv_lean