import Mathlib
import Definitions.Def_ModularCurve_X1

set_option autoImplicit false

noncomputable section

open HahnSeries IntermediateField AlgebraicCurve

namespace ModularCurve

section Spec

variable {L : Type*} [Field L] [Algebra ℚ L] (A : ValuationSubring L)
variable {k : Type*} [Field k] (π : A →+* k)
variable (F₀ : IntermediateField ℚ (LaurentSeries ℚ)) (Fbar : IntermediateField k (LaurentSeries k))

def IsLaurentPlaceReduction (r : Place L (laurentBaseChange L F₀) → Place k Fbar) : Prop :=
  (∀ P, (r P).deg = P.deg) ∧
    ∀ (y : LaurentSeries A) (hy : coeffMap A.subtype y ∈ laurentBaseChange L F₀)
      (hyk : coeffMap π y ∈ Fbar), coeffMap π y ≠ 0 →
        ∀ D : Divisor L (laurentBaseChange L F₀),
          (∀ P, D P = P.ord (⟨coeffMap A.subtype y, hy⟩ : laurentBaseChange L F₀)) →
            ∀ Q, Finsupp.mapDomain r D Q = Q.ord (⟨coeffMap π y, hyk⟩ : Fbar)

def laurentIntegralPrincipalDivisors : Set (Divisor L (laurentBaseChange L F₀)) :=
  {D | ∃ (y : LaurentSeries A) (hy : coeffMap A.subtype y ∈ laurentBaseChange L F₀),
      coeffMap π y ∈ Fbar ∧ coeffMap π y ≠ 0 ∧
        ∀ P, D P = P.ord (⟨coeffMap A.subtype y, hy⟩ : laurentBaseChange L F₀)}

def LaurentPrincipalGeneratedByIntegral : Prop :=
  Divisor.principal (K := L) (F := laurentBaseChange L F₀) ≤
    AddSubgroup.closure (laurentIntegralPrincipalDivisors A π F₀ Fbar)

def LaurentReductionInputs : Prop :=
  ∃ r, IsLaurentPlaceReduction A π F₀ Fbar r ∧ LaurentPrincipalGeneratedByIntegral A π F₀ Fbar

end Spec

section SpecLemmas

variable {L : Type*} [Field L] [Algebra ℚ L] {A : ValuationSubring L}
variable {k : Type*} [Field k] {π : A →+* k}
variable {F₀ : IntermediateField ℚ (LaurentSeries ℚ)} {Fbar : IntermediateField k (LaurentSeries k)}
variable {r : Place L (laurentBaseChange L F₀) → Place k Fbar}

theorem IsLaurentPlaceReduction.deg_eq (hr : IsLaurentPlaceReduction A π F₀ Fbar r)
    (P : Place L (laurentBaseChange L F₀)) : (r P).deg = P.deg :=
  hr.1 P

theorem IsLaurentPlaceReduction.isPrincipal_mapDomain (hr : IsLaurentPlaceReduction A π F₀ Fbar r)
    {D : Divisor L (laurentBaseChange L F₀)} (hD : D ∈ laurentIntegralPrincipalDivisors A π F₀ Fbar) :
    Divisor.IsPrincipal (Finsupp.mapDomain r D) := by
  obtain ⟨y, hy, hyk, hne, hDy⟩ := hD
  refine ⟨⟨coeffMap π y, hyk⟩, fun h => hne (congrArg Subtype.val h), fun Q => ?_⟩
  exact hr.2 y hy hyk hne D hDy Q

theorem degree_mapDomain_of_laurent_deg_eq (hdeg : ∀ P, (r P).deg = P.deg)
    (D : Divisor L (laurentBaseChange L F₀)) :
    Divisor.degree (Finsupp.mapDomain r D) = Divisor.degree D := by
  induction D using Finsupp.induction with
  | zero => simp
  | single_add P n D _ _ ih =>
    rw [Finsupp.mapDomain_add, map_add, map_add, ih, Finsupp.mapDomain_single,
      Divisor.degree_single, Divisor.degree_single, hdeg]

theorem mapDomain_mem_degZero_of_laurent_deg_eq (hdeg : ∀ P, (r P).deg = P.deg)
    {D : Divisor L (laurentBaseChange L F₀)}
    (hD : D ∈ Divisor.degZero (K := L) (F := laurentBaseChange L F₀)) :
    Finsupp.mapDomain r D ∈ Divisor.degZero (K := k) (F := Fbar) := by
  rw [Divisor.mem_degZero] at hD ⊢
  rw [degree_mapDomain_of_laurent_deg_eq hdeg, hD]

theorem IsLaurentPlaceReduction.mapDomain_mem_principal (hr : IsLaurentPlaceReduction A π F₀ Fbar r)
    (hgen : LaurentPrincipalGeneratedByIntegral A π F₀ Fbar)
    {D : Divisor L (laurentBaseChange L F₀)}
    (hD : D ∈ Divisor.principal (K := L) (F := laurentBaseChange L F₀)) :
    Finsupp.mapDomain r D ∈ Divisor.principal (K := k) (F := Fbar) := by
  have hD' := hgen hD
  clear hD
  induction hD' using AddSubgroup.closure_induction with
  | mem E hE => exact hr.isPrincipal_mapDomain hE
  | zero => rw [Finsupp.mapDomain_zero]; exact AddSubgroup.zero_mem _
  | add E E' _ _ hE hE' => rw [Finsupp.mapDomain_add]; exact AddSubgroup.add_mem _ hE hE'
  | neg E _ hE =>
    rw [← Finsupp.mapDomain.addMonoidHom_apply, map_neg, Finsupp.mapDomain.addMonoidHom_apply]
    exact AddSubgroup.neg_mem _ hE

end SpecLemmas

section Descent

variable {L : Type*} [Field L] [Algebra ℚ L] {A : ValuationSubring L}
variable {k : Type*} [Field k] {π : A →+* k}
variable {F₀ : IntermediateField ℚ (LaurentSeries ℚ)} {Fbar : IntermediateField k (LaurentSeries k)}
variable (r : Place L (laurentBaseChange L F₀) → Place k Fbar)

def laurentReductionDiv : Divisor L (laurentBaseChange L F₀) →+ Divisor k Fbar :=
  Finsupp.mapDomain.addMonoidHom r

@[simp]
theorem laurentReductionDiv_apply (D : Divisor L (laurentBaseChange L F₀)) :
    laurentReductionDiv r D = Finsupp.mapDomain r D :=
  rfl

theorem laurentReductionDiv_single (P : Place L (laurentBaseChange L F₀)) (n : ℤ) :
    laurentReductionDiv r (Finsupp.single P n) = Finsupp.single (r P) n :=
  Finsupp.mapDomain_single

def laurentReductionDegZero (hdeg : ∀ P, (r P).deg = P.deg) :
    Divisor.degZero (K := L) (F := laurentBaseChange L F₀) →+ Divisor.degZero (K := k) (F := Fbar) :=
  ((laurentReductionDiv r).domRestrict _).codRestrict _
    fun D => mapDomain_mem_degZero_of_laurent_deg_eq hdeg D.2

@[simp]
theorem coe_laurentReductionDegZero (hdeg : ∀ P, (r P).deg = P.deg)
    (D : Divisor.degZero (K := L) (F := laurentBaseChange L F₀)) :
    (laurentReductionDegZero r hdeg D : Divisor k Fbar) =
      Finsupp.mapDomain r (D : Divisor L (laurentBaseChange L F₀)) :=
  rfl

def laurentReductionPic0 (hr : IsLaurentPlaceReduction A π F₀ Fbar r)
    (hgen : LaurentPrincipalGeneratedByIntegral A π F₀ Fbar) :
    Pic0 L (laurentBaseChange L F₀) →+ Pic0 k Fbar :=
  QuotientAddGroup.map _ _ (laurentReductionDegZero r hr.1) (by
    rintro ⟨D, hD0⟩ hD
    simp only [AddSubgroup.mem_addSubgroupOf] at hD ⊢
    exact hr.mapDomain_mem_principal hgen hD)

theorem laurentReductionPic0_mk (hr : IsLaurentPlaceReduction A π F₀ Fbar r)
    (hgen : LaurentPrincipalGeneratedByIntegral A π F₀ Fbar)
    (D : Divisor.degZero (K := L) (F := laurentBaseChange L F₀)) :
    laurentReductionPic0 r hr hgen (Pic0.mk D) = Pic0.mk (laurentReductionDegZero r hr.1 D) :=
  rfl

end Descent

section Total

variable {L : Type*} [Field L] [Algebra ℚ L] (A : ValuationSubring L)
variable {k : Type*} [Field k] (π : A →+* k)
variable (F₀ : IntermediateField ℚ (LaurentSeries ℚ)) (Fbar : IntermediateField k (LaurentSeries k))

open Classical in

def laurentReduction : Pic0 L (laurentBaseChange L F₀) →+ Pic0 k Fbar :=
  if h : LaurentReductionInputs A π F₀ Fbar then
    laurentReductionPic0 h.choose h.choose_spec.1 h.choose_spec.2
  else 0

variable {A π F₀ Fbar}

theorem laurentReduction_eq (h : LaurentReductionInputs A π F₀ Fbar) :
    laurentReduction A π F₀ Fbar = laurentReductionPic0 h.choose h.choose_spec.1 h.choose_spec.2 := by
  rw [laurentReduction, dif_pos h]

theorem laurentReduction_mk (h : LaurentReductionInputs A π F₀ Fbar)
    (D : Divisor.degZero (K := L) (F := laurentBaseChange L F₀)) :
    laurentReduction A π F₀ Fbar (Pic0.mk D) =
      Pic0.mk (laurentReductionDegZero h.choose h.choose_spec.1.1 D) := by
  rw [laurentReduction_eq h]
  rfl

theorem laurentReduction_of_not (h : ¬ LaurentReductionInputs A π F₀ Fbar) :
    laurentReduction A π F₀ Fbar = 0 := by
  rw [laurentReduction, dif_neg h]

end Total

section Uniqueness

variable {L : Type*} [Field L] [Algebra ℚ L] {A : ValuationSubring L}
variable {k : Type*} [Field k] {π : A →+* k}
variable {F₀ : IntermediateField ℚ (LaurentSeries ℚ)} {Fbar : IntermediateField k (LaurentSeries k)}

private theorem int_eq_zero_of_forall_dvd' {a : ℤ} (h : ∀ n : ℕ, n ≠ 0 → (n : ℤ) ∣ a) : a = 0 :=
  Int.eq_zero_of_dvd_of_natAbs_lt_natAbs (h (a.natAbs + 1) (Nat.succ_ne_zero _))
    (by rw [Int.natAbs_natCast]; exact Nat.lt_succ_self _)

theorem IsLaurentPlaceReduction.eq_or_const_of_agree
    {r₁ r₂ : Place L (laurentBaseChange L F₀) → Place k Fbar}
    (hgen : LaurentPrincipalGeneratedByIntegral A π F₀ Fbar)
    (hagree : ∀ D ∈ laurentIntegralPrincipalDivisors A π F₀ Fbar,
      Finsupp.mapDomain r₁ D = Finsupp.mapDomain r₂ D)
    (hdeg : ∀ P : Place L (laurentBaseChange L F₀), P.deg = 1)
    (hdiv : ∀ n : ℕ, n ≠ 0 → ∀ x : Pic0 L (laurentBaseChange L F₀),
      ∃ y : Pic0 L (laurentBaseChange L F₀), n • y = x) :
    r₁ = r₂ ∨ ∀ P Q, r₁ P = r₁ Q := by
  classical

  set δ : Divisor L (laurentBaseChange L F₀) →+ Divisor k Fbar :=
    Finsupp.mapDomain.addMonoidHom r₁ - Finsupp.mapDomain.addMonoidHom r₂ with hδ
  have hδapp : ∀ D, δ D = Finsupp.mapDomain r₁ D - Finsupp.mapDomain r₂ D := fun D => rfl

  have hδprin : ∀ D ∈ Divisor.principal (K := L) (F := laurentBaseChange L F₀), δ D = 0 := by
    intro D hD
    have hD' := hgen hD
    clear hD
    induction hD' using AddSubgroup.closure_induction with
    | mem E hE => rw [hδapp, hagree E hE, sub_self]
    | zero => exact map_zero δ
    | add E E' _ _ hE hE' => rw [map_add, hE, hE', add_zero]
    | neg E _ hE => rw [map_neg, hE, neg_zero]

  have hδdeg0 : ∀ D ∈ Divisor.degZero (K := L) (F := laurentBaseChange L F₀), δ D = 0 := by
    intro D hD
    ext Q
    rw [Finsupp.zero_apply]
    refine int_eq_zero_of_forall_dvd' fun n hn => ?_
    obtain ⟨y, hy⟩ := hdiv n hn (Pic0.mk ⟨D, hD⟩)
    obtain ⟨E, rfl⟩ := Pic0.mk_surjective y

    have hmem : ((⟨D, hD⟩ : Divisor.degZero (K := L) (F := laurentBaseChange L F₀))
        - n • E : Divisor.degZero (K := L) (F := laurentBaseChange L F₀)) ∈
          (Divisor.principal (K := L) (F := laurentBaseChange L F₀)).addSubgroupOf
            (Divisor.degZero (K := L) (F := laurentBaseChange L F₀)) := by
      rw [← QuotientAddGroup.eq_iff_sub_mem, QuotientAddGroup.mk_nsmul]
      exact hy.symm
    rw [AddSubgroup.mem_addSubgroupOf, AddSubgroupClass.coe_sub, AddSubgroupClass.coe_nsmul] at hmem
    have h0 := hδprin _ hmem
    rw [map_sub, map_nsmul, sub_eq_zero] at h0
    refine ⟨δ (E : Divisor L (laurentBaseChange L F₀)) Q, ?_⟩
    rw [h0, Finsupp.smul_apply, nsmul_eq_mul]

  have hconst : ∀ P Q : Place L (laurentBaseChange L F₀),
      Finsupp.single (r₁ P) (1 : ℤ) - Finsupp.single (r₂ P) 1 =
        Finsupp.single (r₁ Q) 1 - Finsupp.single (r₂ Q) 1 := by
    intro P Q
    have hPQ : Finsupp.single P (1 : ℤ) - Finsupp.single Q 1 ∈
        Divisor.degZero (K := L) (F := laurentBaseChange L F₀) := by
      rw [Divisor.mem_degZero, map_sub, Divisor.degree_single, Divisor.degree_single, hdeg, hdeg, sub_self]
    have h := hδdeg0 _ hPQ
    rw [hδapp, Finsupp.mapDomain_sub, Finsupp.mapDomain_sub, Finsupp.mapDomain_single,
      Finsupp.mapDomain_single, Finsupp.mapDomain_single, Finsupp.mapDomain_single, sub_eq_zero] at h
    exact sub_eq_sub_iff_sub_eq_sub.mpr h

  rw [or_iff_not_imp_left]
  intro hne
  obtain ⟨P₀, hP₀⟩ : ∃ P₀, r₁ P₀ ≠ r₂ P₀ := by
    by_contra hall
    push Not at hall
    exact hne (funext hall)
  have hr₁const : ∀ Q, r₁ Q = r₁ P₀ := by
    intro Q
    have h := congrArg (fun E => E (r₁ P₀)) (hconst Q P₀)
    simp only [Finsupp.sub_apply, Finsupp.single_apply, if_neg (Ne.symm hP₀)] at h
    by_contra hQ
    rw [if_neg hQ] at h
    split_ifs at h <;> omega
  exact fun P Q => (hr₁const P).trans (hr₁const Q).symm

theorem IsLaurentPlaceReduction.eq_of_agree
    {r₁ r₂ : Place L (laurentBaseChange L F₀) → Place k Fbar}
    (hgen : LaurentPrincipalGeneratedByIntegral A π F₀ Fbar)
    (hagree : ∀ D ∈ laurentIntegralPrincipalDivisors A π F₀ Fbar,
      Finsupp.mapDomain r₁ D = Finsupp.mapDomain r₂ D)
    (hdeg : ∀ P : Place L (laurentBaseChange L F₀), P.deg = 1)
    (hprin0 : ∀ D ∈ Divisor.principal (K := L) (F := laurentBaseChange L F₀), Divisor.degree D = 0)
    (hdiv : ∀ n : ℕ, n ≠ 0 → ∀ x : Pic0 L (laurentBaseChange L F₀),
      ∃ y : Pic0 L (laurentBaseChange L F₀), n • y = x)
    (hnc : ∃ D ∈ Divisor.principal (K := L) (F := laurentBaseChange L F₀), Finsupp.mapDomain r₁ D ≠ 0) :
    r₁ = r₂ := by
  rcases IsLaurentPlaceReduction.eq_or_const_of_agree hgen hagree hdeg hdiv with h | hconst
  · exact h
  obtain ⟨D, hDprin, hDne⟩ := hnc
  obtain ⟨P₀⟩ : Nonempty (Place L (laurentBaseChange L F₀)) := by
    by_contra hempty
    rw [not_nonempty_iff] at hempty
    exact hDne (by rw [Subsingleton.elim D 0, Finsupp.mapDomain_zero])
  exfalso
  apply hDne
  have hmapconst : ∀ D : Divisor L (laurentBaseChange L F₀),
      Finsupp.mapDomain r₁ D = Finsupp.single (r₁ P₀) (Divisor.degree D) := by
    intro D
    induction D using Finsupp.induction with
    | zero => simp
    | single_add P n D _ _ ih =>
      rw [Finsupp.mapDomain_add, ih, Finsupp.mapDomain_single, hconst P P₀, map_add,
        Divisor.degree_single, hdeg, Nat.cast_one, mul_one, ← Finsupp.single_add, add_comm]
  rw [hmapconst D, hprin0 D hDprin, Finsupp.single_zero]

end Uniqueness

section CharL

set_option synthInstance.maxHeartbeats 400000

variable (A : ValuationSubring (AlgebraicClosure ℚ)) (Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ))

abbrev IsPlaceReductionQExpModL
    (r : Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (qExpFunctionFieldC ℚ Γ)) →
      Place (IsLocalRing.ResidueField A) (qExpFunctionFieldC (IsLocalRing.ResidueField A) Γ)) : Prop :=
  IsLaurentPlaceReduction A (IsLocalRing.residue A) (qExpFunctionFieldC ℚ Γ)
    (qExpFunctionFieldC (IsLocalRing.ResidueField A) Γ) r

abbrev ReductionInputsQExpModL : Prop :=
  LaurentReductionInputs A (IsLocalRing.residue A) (qExpFunctionFieldC ℚ Γ)
    (qExpFunctionFieldC (IsLocalRing.ResidueField A) Γ)

variable {A Γ} in

def placeReductionQExpModL (h : ReductionInputsQExpModL A Γ) :
    Place (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (qExpFunctionFieldC ℚ Γ)) →
      Place (IsLocalRing.ResidueField A) (qExpFunctionFieldC (IsLocalRing.ResidueField A) Γ) :=
  h.choose

variable {A Γ} in
theorem isPlaceReductionQExpModL_placeReductionQExpModL (h : ReductionInputsQExpModL A Γ) :
    IsPlaceReductionQExpModL A Γ (placeReductionQExpModL h) :=
  h.choose_spec.1

abbrev reductionQExpModL :
    Pic0 (AlgebraicClosure ℚ) (laurentBaseChange (AlgebraicClosure ℚ) (qExpFunctionFieldC ℚ Γ)) →+
      Pic0 (IsLocalRing.ResidueField A) (qExpFunctionFieldC (IsLocalRing.ResidueField A) Γ) :=
  laurentReduction A (IsLocalRing.residue A) (qExpFunctionFieldC ℚ Γ)
    (qExpFunctionFieldC (IsLocalRing.ResidueField A) Γ)

variable {A Γ} in
theorem reductionQExpModL_mk (h : ReductionInputsQExpModL A Γ)
    (D : Divisor.degZero (K := AlgebraicClosure ℚ)
      (F := laurentBaseChange (AlgebraicClosure ℚ) (qExpFunctionFieldC ℚ Γ))) :
    reductionQExpModL A Γ (Pic0.mk D) =
      Pic0.mk (laurentReductionDegZero (placeReductionQExpModL h)
        (isPlaceReductionQExpModL_placeReductionQExpModL h).1 D) :=
  laurentReduction_mk h D

variable {A Γ} in
theorem reductionQExpModL_of_not (h : ¬ ReductionInputsQExpModL A Γ) : reductionQExpModL A Γ = 0 :=
  laurentReduction_of_not h

example (M : ℕ) (z : JOne M) : JOneC M (IsLocalRing.ResidueField A) :=
  reductionQExpModL A (CongruenceSubgroup.Gamma1 M) z

end CharL

end ModularCurve

end