import Mathlib
import Definitions.Def_ModularCurve_JqCoeff
import Definitions.Def_ModularCurve_LaurentCoeff
import Definitions.Def_AlgebraicCurve_DivisorClassGroup
import Theorems.Thm_ModularCurve_coeffMap_qExpand
import Theorems.Thm_ModularCurve_coeff_jqModC_pow_self
import Theorems.Thm_ModularCurve_coeff_jqModC_pow_of_lt
import Theorems.Thm_ModularCurve_coeff_jqModC_neg_one

set_option autoImplicit false

noncomputable section

open HahnSeries IntermediateField AlgebraicCurve

namespace ModularCurve

section CoeffMapSupply

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

theorem coeffMap_ofPowerSeries (f : R →+* S) (p : PowerSeries R) :
    coeffMap f (HahnSeries.ofPowerSeries ℤ R p) = HahnSeries.ofPowerSeries ℤ S (p.map f) := by
  ext k
  rw [coeffMap_coeff]
  rcases le_or_gt 0 k with hk | hk
  · lift k to ℕ using hk
    rw [HahnSeries.ofPowerSeries_apply_coeff, HahnSeries.ofPowerSeries_apply_coeff,
      PowerSeries.coeff_map]
  · rw [ofPowerSeries_coeff_of_neg _ hk, ofPowerSeries_coeff_of_neg _ hk, map_zero]

end CoeffMapSupply

section JExpansion

variable (R : Type*) [CommRing R]

theorem jqNModC_rat (N : ℕ) [NeZero N] : jqNModC ℚ N = jqN N := rfl

variable {R} in

theorem coeffMap_jqModC {S : Type*} [CommRing S] (f : R →+* S) : coeffMap f (jqModC R) = jqModC S := by
  rw [jqModC, map_mul, coeffMap_single, map_one, coeffMap_ofPowerSeries,
    ← RingHom.comp_apply (PowerSeries.map f) (PowerSeries.map (Int.castRingHom R)),
    ← PowerSeries.map_comp, RingHom.ext_int (f.comp (Int.castRingHom R)) (Int.castRingHom S)]
  rfl

variable {R} in
theorem coeffMap_jqNModC {S : Type*} [CommRing S] (f : R →+* S) (N : ℕ) [NeZero N] :
    coeffMap f (jqNModC R N) = jqNModC S N := by
  rw [jqNModC, coeffMap_qExpand, coeffMap_jqModC, jqNModC]

variable {R} in

theorem coeff_jqModC_eq_intCast (k : ℤ) : (jqModC R).coeff k = (((jqModC ℤ).coeff k : ℤ) : R) := by
  conv_lhs => rw [← coeffMap_jqModC (Int.castRingHom R)]
  rfl

theorem jqModC_pow (n : ℕ) :
    jqModC R ^ n = HahnSeries.single (-(n : ℤ)) 1 *
      HahnSeries.ofPowerSeries ℤ R ((jNum.map (Int.castRingHom R)) ^ n) := by
  have h : n • (-1 : ℤ) = -(n : ℤ) := by simp
  rw [jqModC, mul_pow, HahnSeries.single_pow, one_pow, h, ← map_pow]

theorem coeff_jqModC_of_lt {k : ℤ} (hk : k < -1) : (jqModC R).coeff k = 0 := by
  simpa using coeff_jqModC_pow_of_lt R (b := 1) (m := k) (by simpa using hk)

theorem jqModC_ne_zero_of_nontrivial [Nontrivial R] : jqModC R ≠ 0 := fun h => by
  simpa [h] using coeff_jqModC_neg_one R

end JExpansion

section QExpandAlg

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

def qExpandAlgHomC : LaurentSeries K →ₐ[K] LaurentSeries K where
  __ := qExpand K N
  commutes' c := by
    show qExpand K N (algebraMap K (LaurentSeries K) c) = algebraMap K (LaurentSeries K) c
    rw [algebraMap_laurentSeries_eq_single, qExpand_single, mul_zero]

@[simp]
theorem qExpandAlgHomC_apply (f : LaurentSeries K) : qExpandAlgHomC K N f = qExpand K N f := rfl

end QExpandAlg

section FunctionField

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

def divisorExpansionsC : Set (LaurentSeries K) :=
  {x | ∃ (d : ℕ) (_ : NeZero d), d ∣ N ∧ x = qExpand K d (jqModC K)}

omit [NeZero N] in
theorem mem_divisorExpansionsC {d : ℕ} [NeZero d] (hd : d ∣ N) :
    qExpand K d (jqModC K) ∈ divisorExpansionsC K N :=
  ⟨d, ‹_›, hd, rfl⟩

def modularFunctionFieldFullC : IntermediateField K (LaurentSeries K) :=
  IntermediateField.adjoin K (divisorExpansionsC K N)

omit [NeZero N] in

theorem modularFunctionFieldFullC_rat : modularFunctionFieldFullC ℚ N = modularFunctionFieldFull N :=
  rfl

omit [NeZero N] in
theorem jqModCd_mem_full {d : ℕ} [NeZero d] (hd : d ∣ N) :
    qExpand K d (jqModC K) ∈ modularFunctionFieldFullC K N :=
  subset_adjoin K _ (mem_divisorExpansionsC K N hd)

omit [NeZero N] in
theorem jqModC_mem_full : jqModC K ∈ modularFunctionFieldFullC K N := by
  simpa [qExpand_one_apply] using jqModCd_mem_full K N (one_dvd N)

theorem modularFunctionFieldC_le_full : modularFunctionFieldC K N ≤ modularFunctionFieldFullC K N := by
  rw [modularFunctionFieldC, adjoin_le_iff]
  rintro x (rfl | rfl)
  · exact jqModC_mem_full K N
  · exact jqModCd_mem_full K N dvd_rfl

theorem full_degeneracyC_le {N M : ℕ} [NeZero N] [NeZero M] (h : N ∣ M) :
    modularFunctionFieldFullC K N ≤ modularFunctionFieldFullC K M := by
  rw [modularFunctionFieldFullC, adjoin_le_iff]
  rintro x ⟨d, hne, hdvd, rfl⟩
  haveI := hne
  exact jqModCd_mem_full K M (hdvd.trans h)

omit [NeZero N] in

theorem full_degeneracyC_map_le (ℓ : ℕ) [NeZero ℓ] :
    (modularFunctionFieldFullC K N).map (qExpandAlgHomC K ℓ) ≤ modularFunctionFieldFullC K (N * ℓ) := by
  rw [modularFunctionFieldFullC, adjoin_map, adjoin_le_iff]
  rintro x ⟨y, ⟨d, hne, hdvd, rfl⟩, rfl⟩
  haveI := hne
  haveI : NeZero (ℓ * d) := ⟨Nat.mul_ne_zero (NeZero.ne ℓ) (NeZero.ne d)⟩
  show qExpandAlgHomC K ℓ (qExpand K d (jqModC K)) ∈ _
  rw [qExpandAlgHomC_apply, qExpand_qExpand]
  exact jqModCd_mem_full K (N * ℓ) ((mul_dvd_mul_left ℓ hdvd).trans (dvd_of_eq (mul_comm ℓ N)))

end FunctionField

section Jacobian

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

abbrev JZeroC : Type _ := Pic0 K (modularFunctionFieldFullC K N)

example : AddCommGroup (JZeroC K N) := inferInstance

end Jacobian

end ModularCurve

end