import Definitions.Def_WeierstrassCurve_ReduceHom
import Definitions.Def_ModularCurve_SpecialisationVocab
import Mathlib.RingTheory.LocalRing.ResidueField.Basic
import Mathlib.RingTheory.Ideal.Quotient.Operations
import Mathlib.GroupTheory.OrderOfElement

set_option autoImplicit false

noncomputable section

open IsLocalRing ValuationSubring
open ModularCurve.TatePoint (Qbar H CycSubH)

namespace WeierstrassCurve

variable {L : Type*} [Field L] {A : ValuationSubring L} {W : WeierstrassCurve A}
variable [DecidableEq L] [DecidableEq (ResidueField A)]
variable (hΔ : (W.map (residue A)).Δ ≠ 0)

omit [DecidableEq (ResidueField A)] in

theorem eq_zero_of_nsmul_eq_zero_of_reducePoint_eq_zero' {N : ℕ} (hN : (N : ResidueField A) ≠ 0)
    (P : (W.map A.subtype).toAffine.Point) (hP : N • P = 0) (h0 : reducePoint hΔ P = 0) :
    P = 0 := by
  cases P with
  | zero => rfl
  | some x y h =>
    exfalso
    have hx : x ∈ A := X_mem_of_nsmul_eq_zero' W hN h hP
    rw [reducePoint_some_of_mem hΔ h hx] at h0
    exact Affine.Point.some_ne_zero _ h0

theorem reduceHom_injOn_nsmul_eq_zero {N : ℕ} (hN : (N : ResidueField A) ≠ 0)
    {P Q : (W.map A.subtype).toAffine.Point} (hP : N • P = 0) (hQ : N • Q = 0)
    (h : reduceHom hΔ P = reduceHom hΔ Q) : P = Q := by
  have h1 : N • (P - Q) = 0 := by rw [nsmul_sub, hP, hQ, sub_zero]
  have h2 : reducePoint hΔ (P - Q) = 0 := by
    show reduceHom hΔ (P - Q) = 0
    rw [map_sub, h, sub_self]
  exact sub_eq_zero.mp (eq_zero_of_nsmul_eq_zero_of_reducePoint_eq_zero' hΔ hN _ h1 h2)

end WeierstrassCurve

def CycSubOf (G : Type*) [AddGroup G] (N : ℕ) : Type _ :=
  {S : AddSubgroup G // ∃ g : G, addOrderOf g = N ∧ S = AddSubgroup.zmultiples g}

namespace CycSubOf

variable {G G' : Type*} [AddCommGroup G] [AddCommGroup G'] (f : G →+ G') {N : ℕ}
variable (hf : ∀ ⦃P Q : G⦄, N • P = 0 → N • Q = 0 → f P = f Q → P = Q)

include hf in

theorem addOrderOf_map_of_injOn {g : G} (hg : addOrderOf g = N) : addOrderOf (f g) = N := by
  apply Nat.dvd_antisymm
  · apply addOrderOf_dvd_of_nsmul_eq_zero
    rw [← map_nsmul, ← hg, addOrderOf_nsmul_eq_zero, map_zero]
  · rw [← hg]
    apply addOrderOf_dvd_of_nsmul_eq_zero
    refine hf ?_ (smul_zero _) ?_
    · rw [smul_comm, ← hg, addOrderOf_nsmul_eq_zero, smul_zero]
    · rw [map_nsmul, addOrderOf_nsmul_eq_zero, map_zero]

def map : CycSubOf G N → CycSubOf G' N := fun S =>
  ⟨S.1.map f, by
    obtain ⟨g, hg, hS⟩ := S.2
    exact ⟨f g, addOrderOf_map_of_injOn f hf hg, by rw [hS, AddMonoidHom.map_zmultiples]⟩⟩

@[simp] theorem coe_map (S : CycSubOf G N) : (map f hf S).1 = S.1.map f := rfl

end CycSubOf

namespace ModularCurve.HahnSpecialise

open ModularCurve.B3

open ModularCurve.TatePoint

def valuationSubringH : ValuationSubring H :=
  { integralO with
  mem_or_inv_mem' := fun x => by
    by_cases hx0 : x = 0
    · left; simp [hx0]
    rcases le_or_gt 0 x.orderTop with h | h
    · exact Or.inl h
    · right
      show 0 ≤ x⁻¹.orderTop
      have hinv : x⁻¹ ≠ 0 := inv_ne_zero hx0
      have h1 : (x * x⁻¹).order = x.order + x⁻¹.order := HahnSeries.order_mul hx0 hinv
      rw [mul_inv_cancel₀ hx0, HahnSeries.order_one] at h1
      have hxord : x.order < 0 := by
        have h' : ((x.order : ℚ) : WithTop ℚ) < 0 := by
          rw [HahnSeries.order_eq_orderTop_of_ne_zero hx0]; exact h
        exact_mod_cast h'
      have h2 : 0 ≤ x⁻¹.order := by linarith
      rw [← HahnSeries.order_eq_orderTop_of_ne_zero hinv]
      exact_mod_cast h2 }

theorem mem_valuationSubringH {x : H} : x ∈ valuationSubringH ↔ 0 ≤ x.orderTop := Iff.rfl

def resH : valuationSubringH →+* Qbar where
  toFun x := (x : H).coeff 0
  map_one' := by simp
  map_mul' x y := coeff_zero_mul_of_integral x.2 y.2
  map_zero' := by simp
  map_add' x y := by simp

@[simp] theorem resH_apply (x : valuationSubringH) : resH x = (x : H).coeff 0 := rfl

theorem resH_eq_resO (x : valuationSubringH) : resH x = resO ⟨(x : H), x.2⟩ := rfl

theorem resH_surjective : Function.Surjective resH := fun c => by
  refine ⟨⟨HahnSeries.C c, ?_⟩, ?_⟩
  · show 0 ≤ (HahnSeries.C c : H).orderTop
    by_cases hc : c = 0
    · simp [hc]
    · rw [HahnSeries.C_apply, HahnSeries.orderTop_single hc]; exact le_rfl
  · show (HahnSeries.C c : H).coeff 0 = c
    simp

theorem ker_resH : RingHom.ker resH = maximalIdeal valuationSubringH :=
  IsLocalRing.eq_maximalIdeal (RingHom.ker_isMaximal_of_surjective resH resH_surjective)

def residueFieldEquiv : ResidueField valuationSubringH ≃+* Qbar :=
  (Ideal.quotEquivOfEq ker_resH.symm).trans (RingHom.quotientKerEquivOfSurjective resH_surjective)

theorem residueFieldEquiv_residue (x : valuationSubringH) :
    residueFieldEquiv (residue valuationSubringH x) = (x : H).coeff 0 := rfl

end ModularCurve.HahnSpecialise

namespace ModularCurve.HahnSpecialise

open ModularCurve.B3

open WeierstrassCurve

def liftModel (E : WeierstrassCurve H) (hE : IntegralCoeffs E) : WeierstrassCurve valuationSubringH :=
  ⟨⟨E.a₁, hE.1⟩, ⟨E.a₂, hE.2.1⟩, ⟨E.a₃, hE.2.2.1⟩, ⟨E.a₄, hE.2.2.2.1⟩, ⟨E.a₆, hE.2.2.2.2⟩⟩

@[simp] theorem liftModel_map_subtype (E : WeierstrassCurve H) (hE : IntegralCoeffs E) :
    (liftModel E hE).map valuationSubringH.subtype = E := by
  cases E; rfl

theorem liftModel_map_residue_map_equiv (E : WeierstrassCurve H) (hE : IntegralCoeffs E) :
    ((liftModel E hE).map (residue valuationSubringH)).map residueFieldEquiv.toRingHom
      = specialFibre E := by
  cases E
  rw [WeierstrassCurve.map_map]
  rfl

theorem isUnit_iff_orderTop_eq_zero (x : valuationSubringH) :
    IsUnit x ↔ (x : H).orderTop = 0 := by
  constructor
  · intro hu
    obtain ⟨y, hy⟩ := hu.exists_right_inv
    have hxy : (x : H) * (y : H) = 1 := by
      have := congrArg (fun z : valuationSubringH => (z : H)) hy
      simpa using this
    have hx0 : (x : H) ≠ 0 := left_ne_zero_of_mul_eq_one hxy
    have hy0 : (y : H) ≠ 0 := right_ne_zero_of_mul_eq_one hxy
    have h1 := HahnSeries.order_mul hx0 hy0
    rw [hxy, HahnSeries.order_one] at h1
    have hx' : 0 ≤ (x : H).order := by
      have h : 0 ≤ (x : H).orderTop := x.2
      rw [← HahnSeries.order_eq_orderTop_of_ne_zero hx0] at h
      exact_mod_cast h
    have hy' : 0 ≤ (y : H).order := by
      have h : 0 ≤ (y : H).orderTop := y.2
      rw [← HahnSeries.order_eq_orderTop_of_ne_zero hy0] at h
      exact_mod_cast h
    have h2 : (x : H).order = 0 := by linarith
    rw [← HahnSeries.order_eq_orderTop_of_ne_zero hx0]
    exact_mod_cast h2
  · intro h0
    have hx0 : (x : H) ≠ 0 := by
      intro hx; rw [hx, HahnSeries.orderTop_zero] at h0; exact WithTop.top_ne_coe h0
    have hinv : 0 ≤ (x : H)⁻¹.orderTop := by
      have hi0 : (x : H)⁻¹ ≠ 0 := inv_ne_zero hx0
      have h1 : ((x : H) * (x : H)⁻¹).order = (x : H).order + (x : H)⁻¹.order :=
        HahnSeries.order_mul hx0 hi0
      rw [mul_inv_cancel₀ hx0, HahnSeries.order_one] at h1
      have hx : (x : H).order = 0 := by
        have := (HahnSeries.order_eq_orderTop_of_ne_zero hx0).trans h0
        exact_mod_cast this
      rw [← HahnSeries.order_eq_orderTop_of_ne_zero hi0]
      have : (x : H)⁻¹.order = 0 := by linarith
      exact_mod_cast this.symm.le
    exact ⟨⟨x, ⟨(x : H)⁻¹, hinv⟩, Subtype.ext (mul_inv_cancel₀ hx0),
      Subtype.ext (inv_mul_cancel₀ hx0)⟩, rfl⟩

theorem map_residue_Δ_ne_zero_of_specialFibre (E : WeierstrassCurve H) (hE : IntegralCoeffs E)
    (hΔ : (specialFibre E).Δ ≠ 0) :
    ((liftModel E hE).map (residue valuationSubringH)).Δ ≠ 0 := by
  intro h0
  apply hΔ
  rw [← liftModel_map_residue_map_equiv E hE, WeierstrassCurve.map_Δ, h0, map_zero]

theorem specialFibre_Δ_ne_zero_iff (E : WeierstrassCurve H) (hE : IntegralCoeffs E) :
    (specialFibre E).Δ ≠ 0 ↔ E.Δ.orderTop = 0 := by
  have h1 : ((liftModel E hE).map valuationSubringH.subtype).Δ =
      valuationSubringH.subtype (liftModel E hE).Δ := by
    simp only [WeierstrassCurve.map_Δ]
  rw [liftModel_map_subtype] at h1
  have h2 : (specialFibre E).Δ =
      residueFieldEquiv (((liftModel E hE).map (residue valuationSubringH)).Δ) := by
    rw [← liftModel_map_residue_map_equiv E hE, WeierstrassCurve.map_Δ]; rfl
  rw [h2, residueFieldEquiv.map_ne_zero_iff, WeierstrassCurve.map_residue_Δ_ne_zero_iff,
    isUnit_iff_orderTop_eq_zero, h1]
  rfl

end ModularCurve.HahnSpecialise

namespace ModularCurve.HahnSpecialise

open ModularCurve.B3

open WeierstrassCurve
open scoped Classical

@[reducible] def algebraQbar : Algebra valuationSubringH Qbar := resH.toAlgebra

attribute [local instance] algebraQbar

@[simp] theorem algebraMap_Qbar_apply (x : valuationSubringH) :
    algebraMap valuationSubringH Qbar x = (x : H).coeff 0 := rfl

def residueAlgEquiv : ResidueField valuationSubringH ≃ₐ[valuationSubringH] Qbar :=
  AlgEquiv.ofRingEquiv (f := residueFieldEquiv) (fun _ => rfl)

variable (E : WeierstrassCurve H) (hE : IntegralCoeffs E)

def specialFibrePointMap :
    ((liftModel E hE).map (residue valuationSubringH)).toAffine.Point →+
      (specialFibre E).toAffine.Point :=
  (Affine.Point.map (W' := (liftModel E hE).toAffine)
    (residueAlgEquiv : ResidueField valuationSubringH →ₐ[valuationSubringH] Qbar) :)

theorem specialFibrePointMap_injective : Function.Injective (specialFibrePointMap E hE) :=
  Affine.Point.map_injective _

def specialise (hΔ : (specialFibre E).Δ ≠ 0) : E.toAffine.Point →+ (specialFibre E).toAffine.Point :=
  (specialFibrePointMap E hE).comp
    ((reduceHom (map_residue_Δ_ne_zero_of_specialFibre E hE hΔ) :
      ((liftModel E hE).map valuationSubringH.subtype).toAffine.Point →+ _) :)

include hE in

theorem nonsingular_specialFibre_coeff_zero (hΔ : (specialFibre E).Δ ≠ 0) {x y : H}
    (h : E.toAffine.Nonsingular x y) (hx : 0 ≤ x.orderTop) :
    (specialFibre E).toAffine.Nonsingular (x.coeff 0) (y.coeff 0) := by
  have h' : ((liftModel E hE).map valuationSubringH.subtype).toAffine.Nonsingular x y := by
    rw [liftModel_map_subtype]; exact h
  have hy : y ∈ valuationSubringH := WeierstrassCurve.Affine.Y_mem_of_X_mem (liftModel E hE) h'.1 hx
  have hres := WeierstrassCurve.Affine.nonsingular_residue (liftModel E hE)
    (map_residue_Δ_ne_zero_of_specialFibre E hE hΔ) (x := ⟨x, hx⟩) (y := ⟨y, hy⟩) h'.1
  have hmap := ((((liftModel E hE).map (residue valuationSubringH)).toAffine.map_nonsingular
    (f := residueFieldEquiv.toRingHom) residueFieldEquiv.injective
    (residue valuationSubringH ⟨x, hx⟩) (residue valuationSubringH ⟨y, hy⟩)).mpr hres)
  rw [show ((liftModel E hE).map (residue valuationSubringH)).toAffine.map residueFieldEquiv.toRingHom
      = (specialFibre E).toAffine from liftModel_map_residue_map_equiv E hE] at hmap
  exact hmap

@[simp] theorem specialise_zero (hΔ : (specialFibre E).Δ ≠ 0) : specialise E hE hΔ 0 = 0 :=
  map_zero _

theorem specialise_some_of_nonneg (hΔ : (specialFibre E).Δ ≠ 0) {x y : H}
    (h : E.toAffine.Nonsingular x y) (hx : 0 ≤ x.orderTop) :
    specialise E hE hΔ (.some x y h) =
      .some (x.coeff 0) (y.coeff 0) (nonsingular_specialFibre_coeff_zero E hE hΔ h hx) := by
  have h' : ((liftModel E hE).map valuationSubringH.subtype).toAffine.Nonsingular x y := by
    rw [liftModel_map_subtype]; exact h
  show specialFibrePointMap E hE (reducePoint (map_residue_Δ_ne_zero_of_specialFibre E hE hΔ)
    (.some x y h')) = _
  rw [WeierstrassCurve.reducePoint_some_of_mem _ h' hx]
  show Affine.Point.map _ (Affine.Point.some _ _ _) = _
  rw [Affine.Point.map_some]
  rfl

theorem specialise_some_of_neg (hΔ : (specialFibre E).Δ ≠ 0) {x y : H}
    (h : E.toAffine.Nonsingular x y) (hx : ¬ 0 ≤ x.orderTop) :
    specialise E hE hΔ (.some x y h) = 0 := by
  have h' : ((liftModel E hE).map valuationSubringH.subtype).toAffine.Nonsingular x y := by
    rw [liftModel_map_subtype]; exact h
  show specialFibrePointMap E hE (reducePoint (map_residue_Δ_ne_zero_of_specialFibre E hE hΔ)
    (.some x y h')) = _
  rw [WeierstrassCurve.reducePoint_some_of_notMem _ h' hx, map_zero]

theorem natCast_residueField_ne_zero {N : ℕ} (hN : N ≠ 0) :
    (N : ResidueField valuationSubringH) ≠ 0 := by
  intro h
  have := congrArg residueFieldEquiv h
  rw [map_natCast, map_zero] at this
  exact (Nat.cast_ne_zero.mpr hN) this

theorem specialise_injOn_nsmul_eq_zero (hΔ : (specialFibre E).Δ ≠ 0) {N : ℕ} (hN : N ≠ 0)
    {P Q : E.toAffine.Point} (hP : N • P = 0) (hQ : N • Q = 0)
    (h : specialise E hE hΔ P = specialise E hE hΔ Q) : P = Q :=
  reduceHom_injOn_nsmul_eq_zero (W := liftModel E hE) (map_residue_Δ_ne_zero_of_specialFibre E hE hΔ)
    (natCast_residueField_ne_zero hN) hP hQ (specialFibrePointMap_injective E hE h)

theorem addOrderOf_specialise (hΔ : (specialFibre E).Δ ≠ 0) {N : ℕ} (hN : N ≠ 0)
    {g : E.toAffine.Point} (hg : addOrderOf g = N) : addOrderOf (specialise E hE hΔ g) = N :=
  CycSubOf.addOrderOf_map_of_injOn (specialise E hE hΔ)
    (fun _ _ hP hQ h => specialise_injOn_nsmul_eq_zero E hE hΔ hN hP hQ h) hg

end ModularCurve.HahnSpecialise

namespace ModularCurve.HahnSpecialise

open ModularCurve.B3

open scoped Classical

variable (E : WeierstrassCurve H) (hE : IntegralCoeffs E) (hΔ : (specialFibre E).Δ ≠ 0)

def specialiseCycSub (N : ℕ) [NeZero N] : CycSubH E N → CycSub (specialFibre E) N :=
  (CycSubOf.map (specialise E hE hΔ)
    (fun _ _ hP hQ h => specialise_injOn_nsmul_eq_zero E hE hΔ (NeZero.ne N) hP hQ h) :)

@[simp] theorem coe_specialiseCycSub (N : ℕ) [NeZero N] (S : CycSubH E N) :
    (specialiseCycSub E hE hΔ N S).1 = S.1.map (specialise E hE hΔ) := rfl

end ModularCurve.HahnSpecialise

end