import Mathlib
import Definitions.Def_ModularCurve_QAdicPlaceMod
import Definitions.Def_ModularCurve_CharLFrobeniusGeomLevel
import Definitions.Def_ModularCurve_SpecializeModuli
import Definitions.Def_AlgebraicCurve_PlaceEvaluation
import Theorems.Thm_AlgebraicCurve_Place_evalAt_congr
import Theorems.Thm_AlgebraicCurve_Place_evalAt_ne_zero
import Theorems.Thm_AlgebraicCurve_Place_evalAt_algebraMap

set_option autoImplicit false
set_option synthInstance.maxHeartbeats 400000
set_option maxHeartbeats 800000

namespace AlgebraicCurve.Place

open IsDedekindDomain WithZero IsLocalRing

variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)

theorem mk_mem_maximalIdeal_of_ord_pos {f : F} (hf : f ∈ v.toValuationSubring)
    (h : 0 < v.ord f) :
    (⟨f, hf⟩ : v.toValuationSubring) ∈ IsLocalRing.maximalIdeal v.toValuationSubring := by
  rcases eq_or_ne f 0 with rfl | hf0
  · exact Submodule.zero_mem _
  rw [v.mem_maximalIdeal_iff_adicValuation_lt_one]
  have hne : v.adicValuation f ≠ 0 := v.adicValuation_ne_zero hf0
  rw [← exp_log hne, show (1 : ℤᵐ⁰) = exp 0 from rfl, exp_lt_exp]
  have : v.ord f = -log (v.adicValuation f) := rfl
  omega

end AlgebraicCurve.Place

noncomputable section

open AlgebraicCurve Polynomial

namespace ModularCurve

variable (K : Type*) [Field K] in

def evalAtJGeom : Polynomial ℤ →+* LaurentSeries K :=
  Polynomial.eval₂RingHom (Int.castRingHom (LaurentSeries K)) (jqModC K)

variable (K : Type*) [Field K] in
theorem evalAtJGeom_X : evalAtJGeom K Polynomial.X = jqModC K :=
  Polynomial.eval₂_X _ _

variable (K : Type*) [Field K] in

theorem laurentMap_comp_evalAtJInt_geom :
    (laurentMap (Int.castRingHom K)).comp evalAtJInt = evalAtJGeom K := by
  refine Polynomial.ringHom_ext' (Subsingleton.elim _ _) ?_
  rw [RingHom.comp_apply, evalAtJInt_X, evalAtJGeom_X, jqModC, jqInt, map_mul,
    laurentMap_single, laurentMap_ofPowerSeries, map_one]

variable (K : Type*) [Field K] in
theorem laurentMap_jqIntN_geom (N : ℕ) [NeZero N] :
    laurentMap (Int.castRingHom K) (jqIntN N) = jqNModC K N := by
  rw [jqIntN, laurentMap_qExpand, jqNModC, jqModC, jqInt, map_mul,
    laurentMap_single, laurentMap_ofPowerSeries, map_one]

variable {N : ℕ} [NeZero N] in

theorem ModularPolynomialData.eval_int_eq_zero (data : ModularPolynomialData N) :
    data.Φ.eval₂ evalAtJInt (jqIntN N) = 0 := by
  refine laurentMap_injective (f := Int.castRingHom ℚ) Int.cast_injective ?_
  rw [map_zero, Polynomial.hom_eval₂, laurentMap_comp_evalAtJInt, laurentMap_jqIntN]
  exact data.eval_eq_zero

variable (K : Type*) [Field K] {N : ℕ} [NeZero N] in

theorem eval_int_eq_zero_geom (data : ModularPolynomialData N) :
    data.Φ.eval₂ (evalAtJGeom K) (jqNModC K N) = 0 := by
  have h := congrArg (laurentMap (Int.castRingHom K)) data.eval_int_eq_zero
  rwa [map_zero, Polynomial.hom_eval₂, laurentMap_comp_evalAtJInt_geom,
    laurentMap_jqIntN_geom] at h

section Generators

variable (K : Type*) [Field K] (N : ℕ) [NeZero N]

def jGeomGen : modularFunctionFieldC K N := ⟨jqModC K, jqModC_mem K N⟩

def jNGeomGen : modularFunctionFieldC K N := ⟨jqNModC K N, jqNModC_mem K N⟩

@[simp] theorem coe_jGeomGen : ((jGeomGen K N : modularFunctionFieldC K N) : LaurentSeries K)
    = jqModC K := rfl

@[simp] theorem coe_jNGeomGen :
    ((jNGeomGen K N : modularFunctionFieldC K N) : LaurentSeries K) = jqNModC K N := rfl

theorem jNGeomGen_one : jNGeomGen K 1 = jGeomGen K 1 :=
  Subtype.ext (jqNModC_one K)

theorem transcendental_jqNModC : Transcendental K (jqNModC K N) := by
  refine transcendental_iff.mpr fun p hp => ?_
  refine transcendental_iff.mp (transcendental_jqModC K) p ?_
  refine qExpand_injective N ?_
  rw [map_zero]
  calc qExpand K N (Polynomial.aeval (jqModC K) p)
      = qExpandAlgC K N (Polynomial.aeval (jqModC K) p) := rfl
    _ = Polynomial.aeval (qExpandAlgC K N (jqModC K)) p :=
        (Polynomial.aeval_algHom_apply _ _ _).symm
    _ = Polynomial.aeval (jqNModC K N) p := rfl
    _ = 0 := hp

theorem jGeomGen_sub_algebraMap_ne_zero (a : K) :
    jGeomGen K N - algebraMap K (modularFunctionFieldC K N) a ≠ 0 := by
  rw [sub_ne_zero]
  intro h
  have hcoe : jqModC K = algebraMap K (LaurentSeries K) a := by
    have := congrArg (fun z : modularFunctionFieldC K N => (z : LaurentSeries K)) h
    simpa using this
  exact transcendental_jqModC K (hcoe ▸ isAlgebraic_algebraMap a)

theorem jNGeomGen_sub_algebraMap_ne_zero (a : K) :
    jNGeomGen K N - algebraMap K (modularFunctionFieldC K N) a ≠ 0 := by
  rw [sub_ne_zero]
  intro h
  have hcoe : jqNModC K N = algebraMap K (LaurentSeries K) a := by
    have := congrArg (fun z : modularFunctionFieldC K N => (z : LaurentSeries K)) h
    simpa using this
  exact transcendental_jqNModC K N (hcoe ▸ isAlgebraic_algebraMap a)

end Generators

section Evaluation

variable {R S : Type*} [CommRing R] [CommRing S]

def evalModularPair (x y : R) (Φ : Polynomial (Polynomial ℤ)) : R :=
  Φ.eval₂ (Polynomial.eval₂RingHom (Int.castRingHom R) x) y

theorem map_evalModularPair (φ : R →+* S) (x y : R) (Φ : Polynomial (Polynomial ℤ)) :
    φ (evalModularPair x y Φ) = evalModularPair (φ x) (φ y) Φ := by
  unfold evalModularPair
  rw [Polynomial.hom_eval₂]
  congr 1
  refine Polynomial.ringHom_ext' (Subsingleton.elim _ _) ?_
  simp only [RingHom.comp_apply, coe_eval₂RingHom, eval₂_X]

theorem evalModularPair_jq_eq_zero (K : Type*) [Field K] {N : ℕ} [NeZero N]
    (data : ModularPolynomialData N) :
    evalModularPair (jqModC K) (jqNModC K N) data.Φ = 0 :=
  eval_int_eq_zero_geom K data

theorem evalModularPair_jGeomGen_eq_zero (K : Type*) [Field K] (N : ℕ) [NeZero N]
    (data : ModularPolynomialData N) :
    evalModularPair (jGeomGen K N) (jNGeomGen K N) data.Φ = 0 := by
  have hval := map_evalModularPair (modularFunctionFieldC K N).val.toRingHom
    (jGeomGen K N) (jNGeomGen K N) data.Φ
  have hgen : (modularFunctionFieldC K N).val.toRingHom (jGeomGen K N) = jqModC K := rfl
  have hgenN : (modularFunctionFieldC K N).val.toRingHom (jNGeomGen K N) = jqNModC K N := rfl
  rw [hgen, hgenN, evalModularPair_jq_eq_zero K data] at hval
  exact (map_eq_zero_iff _ (modularFunctionFieldC K N).val.toRingHom.injective).mp hval

end Evaluation

section Centre

variable (K : Type*) [Field K] (N : ℕ) [NeZero N]

def IsCentreOf (c : K × K) (w : Place K (modularFunctionFieldC K N)) : Prop :=
  0 < w.ord (jGeomGen K N - algebraMap K (modularFunctionFieldC K N) c.1) ∧
  0 < w.ord (jNGeomGen K N - algebraMap K (modularFunctionFieldC K N) c.2)

variable {K N}
variable {c : K × K} {w : Place K (modularFunctionFieldC K N)}

theorem IsCentreOf.jGeomGen_mem (h : IsCentreOf K N c w) :
    jGeomGen K N ∈ w.toValuationSubring := by
  have hmem : jGeomGen K N - algebraMap K (modularFunctionFieldC K N) c.1
      ∈ w.toValuationSubring :=
    w.mem_of_ord_nonneg (jGeomGen_sub_algebraMap_ne_zero K N c.1) h.1.le
  have := add_mem hmem (w.algebraMap_mem' c.1)
  rwa [sub_add_cancel] at this

theorem IsCentreOf.jNGeomGen_mem (h : IsCentreOf K N c w) :
    jNGeomGen K N ∈ w.toValuationSubring := by
  have hmem : jNGeomGen K N - algebraMap K (modularFunctionFieldC K N) c.2
      ∈ w.toValuationSubring :=
    w.mem_of_ord_nonneg (jNGeomGen_sub_algebraMap_ne_zero K N c.2) h.2.le
  have := add_mem hmem (w.algebraMap_mem' c.2)
  rwa [sub_add_cancel] at this

theorem IsCentreOf.evalAt_jGeomGen (h : IsCentreOf K N c w) :
    w.evalAt (jGeomGen K N) = c.1 := by
  have hcongr := w.evalAt_congr h.jGeomGen_mem
    (w.algebraMap_mem' c.1) (Or.inr h.1)
  rw [hcongr, w.evalAt_algebraMap]

theorem IsCentreOf.evalAt_jNGeomGen (h : IsCentreOf K N c w) :
    w.evalAt (jNGeomGen K N) = c.2 := by
  have hcongr := w.evalAt_congr h.jNGeomGen_mem
    (w.algebraMap_mem' c.2) (Or.inr h.2)
  rw [hcongr, w.evalAt_algebraMap]

theorem IsCentreOf.eq {c' : K × K} (h : IsCentreOf K N c w) (h' : IsCentreOf K N c' w) :
    c = c' := by
  have h1 : c.1 = c'.1 := by rw [← h.evalAt_jGeomGen, h'.evalAt_jGeomGen]
  have h2 : c.2 = c'.2 := by rw [← h.evalAt_jNGeomGen, h'.evalAt_jNGeomGen]
  exact Prod.ext h1 h2

theorem IsCentreOf.ne_of_ne {c' : K × K} {w' : Place K (modularFunctionFieldC K N)}
    (h : IsCentreOf K N c w) (h' : IsCentreOf K N c' w') (hcc : c ≠ c') : w ≠ w' := by
  rintro rfl
  exact hcc (h.eq h')

theorem IsCentreOf.mk_sub_mem_maximalIdeal_fst (h : IsCentreOf K N c w) :
    (⟨jGeomGen K N, h.jGeomGen_mem⟩ : w.toValuationSubring)
        - algebraMap K w.toValuationSubring c.1
      ∈ IsLocalRing.maximalIdeal w.toValuationSubring := by
  have hsub : ((⟨jGeomGen K N, h.jGeomGen_mem⟩ : w.toValuationSubring)
      - algebraMap K w.toValuationSubring c.1 : w.toValuationSubring)
      = ⟨jGeomGen K N - algebraMap K (modularFunctionFieldC K N) c.1,
          sub_mem h.jGeomGen_mem (w.algebraMap_mem' c.1)⟩ := by
    refine Subtype.ext ?_
    show jGeomGen K N - (algebraMap K w.toValuationSubring c.1 : modularFunctionFieldC K N)
      = jGeomGen K N - algebraMap K (modularFunctionFieldC K N) c.1
    rw [Place.coe_algebraMap]
  rw [hsub]
  exact w.mk_mem_maximalIdeal_of_ord_pos _ h.1

theorem IsCentreOf.mk_sub_mem_maximalIdeal_snd (h : IsCentreOf K N c w) :
    (⟨jNGeomGen K N, h.jNGeomGen_mem⟩ : w.toValuationSubring)
        - algebraMap K w.toValuationSubring c.2
      ∈ IsLocalRing.maximalIdeal w.toValuationSubring := by
  have hsub : ((⟨jNGeomGen K N, h.jNGeomGen_mem⟩ : w.toValuationSubring)
      - algebraMap K w.toValuationSubring c.2 : w.toValuationSubring)
      = ⟨jNGeomGen K N - algebraMap K (modularFunctionFieldC K N) c.2,
          sub_mem h.jNGeomGen_mem (w.algebraMap_mem' c.2)⟩ := by
    refine Subtype.ext ?_
    show jNGeomGen K N - (algebraMap K w.toValuationSubring c.2 : modularFunctionFieldC K N)
      = jNGeomGen K N - algebraMap K (modularFunctionFieldC K N) c.2
    rw [Place.coe_algebraMap]
  rw [hsub]
  exact w.mk_mem_maximalIdeal_of_ord_pos _ h.2

theorem IsCentreOf.residue_jGeomGen (h : IsCentreOf K N c w) :
    IsLocalRing.residue w.toValuationSubring ⟨jGeomGen K N, h.jGeomGen_mem⟩
      = algebraMap K w.ResidueField c.1 := by
  rw [← sub_eq_zero, IsScalarTower.algebraMap_apply K w.toValuationSubring w.ResidueField,
    IsLocalRing.ResidueField.algebraMap_eq, ← map_sub]
  exact (IsLocalRing.residue_eq_zero_iff _).mpr h.mk_sub_mem_maximalIdeal_fst

theorem IsCentreOf.residue_jNGeomGen (h : IsCentreOf K N c w) :
    IsLocalRing.residue w.toValuationSubring ⟨jNGeomGen K N, h.jNGeomGen_mem⟩
      = algebraMap K w.ResidueField c.2 := by
  rw [← sub_eq_zero, IsScalarTower.algebraMap_apply K w.toValuationSubring w.ResidueField,
    IsLocalRing.ResidueField.algebraMap_eq, ← map_sub]
  exact (IsLocalRing.residue_eq_zero_iff _).mpr h.mk_sub_mem_maximalIdeal_snd

end Centre

section ModularEquation

variable {K : Type*} [Field K] {N : ℕ} [NeZero N]
variable {c : K × K} {w : Place K (modularFunctionFieldC K N)}

theorem evalModularPair_mk_eq_zero (data : ModularPolynomialData N)
    (hJ : jGeomGen K N ∈ w.toValuationSubring) (hJN : jNGeomGen K N ∈ w.toValuationSubring) :
    evalModularPair (⟨jGeomGen K N, hJ⟩ : w.toValuationSubring) ⟨jNGeomGen K N, hJN⟩ data.Φ
      = 0 := by
  have hval := map_evalModularPair (SubringClass.subtype w.toValuationSubring)
    (⟨jGeomGen K N, hJ⟩ : w.toValuationSubring) ⟨jNGeomGen K N, hJN⟩ data.Φ
  have hgen : SubringClass.subtype w.toValuationSubring
      (⟨jGeomGen K N, hJ⟩ : w.toValuationSubring) = jGeomGen K N := rfl
  have hgenN : SubringClass.subtype w.toValuationSubring
      (⟨jNGeomGen K N, hJN⟩ : w.toValuationSubring) = jNGeomGen K N := rfl
  rw [hgen, hgenN, evalModularPair_jGeomGen_eq_zero K N data] at hval
  exact (map_eq_zero_iff (SubringClass.subtype w.toValuationSubring)
    Subtype.val_injective).mp hval

theorem IsCentreOf.modularEquation (data : ModularPolynomialData N)
    (h : IsCentreOf K N c w) :
    evalModularPair c.1 c.2 data.Φ = 0 := by

  have hres := congrArg (IsLocalRing.residue w.toValuationSubring)
    (evalModularPair_mk_eq_zero data h.jGeomGen_mem h.jNGeomGen_mem)
  rw [map_zero, map_evalModularPair, h.residue_jGeomGen, h.residue_jNGeomGen,
    ← map_evalModularPair] at hres

  exact (map_eq_zero_iff _ (algebraMap K w.ResidueField).injective).mp hres

end ModularEquation

section Frobenius

variable (K : Type*) [Field K] (N : ℕ) [NeZero N]
variable {ℓ : ℕ} [Fact ℓ.Prime] [CharP K ℓ]
variable (data : ModularPolynomialData ℓ) (hKr : KroneckerCongruence ℓ data)

theorem frobeniusGeomLevel_jGeomGen_sub_pow (a : K) :
    frobeniusGeomLevel K N data hKr
        (jGeomGen K N - algebraMap K (modularFunctionFieldC K N) (a ^ ℓ))
      = (jGeomGen K N - algebraMap K (modularFunctionFieldC K N) a) ^ ℓ := by
  haveI : CharP (LaurentSeries K) ℓ := charP_laurentSeries K
  have hj : frobeniusGeomLevel K N data hKr (jGeomGen K N) = jGeomGen K N ^ ℓ :=
    frobeniusGeomLevel_jq K N data hKr
  rw [map_sub, AlgHom.commutes, hj, map_pow]
  refine Subtype.ext ?_
  push_cast
  rw [sub_pow_char]

theorem frobeniusGeomLevel_jNGeomGen_sub_pow (b : K) :
    frobeniusGeomLevel K N data hKr
        (jNGeomGen K N - algebraMap K (modularFunctionFieldC K N) (b ^ ℓ))
      = (jNGeomGen K N - algebraMap K (modularFunctionFieldC K N) b) ^ ℓ := by
  haveI : CharP (LaurentSeries K) ℓ := charP_laurentSeries K
  have hj : frobeniusGeomLevel K N data hKr (jNGeomGen K N) = jNGeomGen K N ^ ℓ :=
    frobeniusGeomLevel_jqN K N data hKr
  rw [map_sub, AlgHom.commutes, hj, map_pow]
  refine Subtype.ext ?_
  push_cast
  rw [sub_pow_char]

variable {K N}

omit [Fact ℓ.Prime] [CharP K ℓ] in

private theorem ord_pow_prime (w : Place K (modularFunctionFieldC K N))
    (g : modularFunctionFieldC K N) : w.ord (g ^ ℓ) = (ℓ : ℤ) * w.ord g := by
  rw [show g ^ ℓ = g ^ ((ℓ : ℕ) : ℤ) from (zpow_natCast g ℓ).symm, w.ord_zpow]

private theorem pos_of_mul_pos_left' {e x : ℤ} (h : 0 < e * x) (he : 0 < e) : 0 < x := by
  rcases lt_trichotomy x 0 with hx | hx | hx
  · exact absurd h (not_lt.mpr (mul_nonpos_iff.mpr (Or.inl ⟨he.le, hx.le⟩)))
  · subst hx; simp at h
  · exact hx

theorem IsCentreOf.frobOnPlacesGeomLevel {c : K × K}
    {w : Place K (modularFunctionFieldC K N)} (h : IsCentreOf K N c w) :
    IsCentreOf K N (c.1 ^ ℓ, c.2 ^ ℓ) (frobOnPlacesGeomLevel K N data hKr w) := by
  obtain ⟨e, he, -, hord⟩ := exists_ramification_frobenius K N data hKr w
  have hℓ : 0 < (ℓ : ℤ) := by exact_mod_cast (Fact.out : ℓ.Prime).pos
  constructor
  ·
    have hkey := hord (jGeomGen K N - algebraMap K (modularFunctionFieldC K N) (c.1 ^ ℓ))
    rw [frobeniusGeomLevel_jGeomGen_sub_pow K N data hKr c.1, ord_pow_prime] at hkey
    refine pos_of_mul_pos_left' (e := (e : ℤ)) ?_ (by exact_mod_cast he)
    rw [← hkey]
    exact mul_pos hℓ h.1
  ·
    have hkey := hord (jNGeomGen K N - algebraMap K (modularFunctionFieldC K N) (c.2 ^ ℓ))
    rw [frobeniusGeomLevel_jNGeomGen_sub_pow K N data hKr c.2, ord_pow_prime] at hkey
    refine pos_of_mul_pos_left' (e := (e : ℤ)) ?_ (by exact_mod_cast he)
    rw [← hkey]
    exact mul_pos hℓ h.2

end Frobenius

section Existence

variable {K : Type*} [Field K] {N : ℕ} [NeZero N]

def IsAffineGeomPlace (K : Type*) [Field K] (N : ℕ) [NeZero N]
    (w : Place K (modularFunctionFieldC K N)) : Prop :=
  jGeomGen K N ∈ w.toValuationSubring ∧ jNGeomGen K N ∈ w.toValuationSubring

theorem IsCentreOf.isAffineGeomPlace {c : K × K} {w : Place K (modularFunctionFieldC K N)}
    (h : IsCentreOf K N c w) : IsAffineGeomPlace K N w :=
  ⟨h.jGeomGen_mem, h.jNGeomGen_mem⟩

theorem ord_sub_evalAt_pos_of_isRational {w : Place K (modularFunctionFieldC K N)}
    (hrat : w.IsRational) {f : modularFunctionFieldC K N} (hf : f ∈ w.toValuationSubring)
    (hne : f - algebraMap K (modularFunctionFieldC K N) (w.evalAt f) ≠ 0) :
    0 < w.ord (f - algebraMap K (modularFunctionFieldC K N) (w.evalAt f)) := by
  have hmem : f - algebraMap K (modularFunctionFieldC K N) (w.evalAt f)
      ∈ w.toValuationSubring := sub_mem hf (w.algebraMap_mem' _)
  rcases eq_or_ne (w.ord (f - algebraMap K (modularFunctionFieldC K N) (w.evalAt f))) 0
    with h0 | h0
  ·

    exfalso
    refine w.evalAt_ne_zero hrat hne h0 ?_
    have hres : algebraMap K w.ResidueField
        (w.evalAt (f - algebraMap K (modularFunctionFieldC K N) (w.evalAt f))) = 0 := by
      rw [w.algebraMap_evalAt hrat hmem]
      have hcoe : (⟨f - algebraMap K (modularFunctionFieldC K N) (w.evalAt f), hmem⟩
          : w.toValuationSubring)
          = ⟨f, hf⟩ - algebraMap K w.toValuationSubring (w.evalAt f) := by
        refine Subtype.ext ?_
        show f - algebraMap K (modularFunctionFieldC K N) (w.evalAt f)
          = f - (algebraMap K w.toValuationSubring (w.evalAt f) : modularFunctionFieldC K N)
        rw [Place.coe_algebraMap]
      rw [hcoe, map_sub, sub_eq_zero, ← w.algebraMap_evalAt hrat hf,
        IsScalarTower.algebraMap_apply K w.toValuationSubring w.ResidueField,
        IsLocalRing.ResidueField.algebraMap_eq]
    exact (map_eq_zero_iff _ (algebraMap K w.ResidueField).injective).mp hres
  · have hnonneg := w.ord_nonneg_of_mem hmem
    omega

theorem exists_isCentreOf_of_isRational {w : Place K (modularFunctionFieldC K N)}
    (hrat : w.IsRational) (haff : IsAffineGeomPlace K N w) :
    IsCentreOf K N (w.evalAt (jGeomGen K N), w.evalAt (jNGeomGen K N)) w :=
  ⟨ord_sub_evalAt_pos_of_isRational hrat haff.1
      (jGeomGen_sub_algebraMap_ne_zero K N _),
    ord_sub_evalAt_pos_of_isRational hrat haff.2
      (jNGeomGen_sub_algebraMap_ne_zero K N _)⟩

end Existence

end ModularCurve