import Definitions.Def_CohCarrier_Level

set_option autoImplicit false

namespace CohCarrier

open CongruenceSubgroup
open scoped MatrixGroups

section RightCosets

variable {Γ : Type*} [Group Γ] (S : Subgroup Γ)

noncomputable def rep (q : Quotient (QuotientGroup.rightRel S)) : Γ := q.out

abbrev cls (g : Γ) : Quotient (QuotientGroup.rightRel S) := Quotient.mk _ g

noncomputable def slip (q : Quotient (QuotientGroup.rightRel S)) (γ : Γ) : S :=
  ⟨rep S q * γ * (rep S (cls S (rep S q * γ)))⁻¹, by
    have h : QuotientGroup.rightRel S (rep S (cls S (rep S q * γ))) (rep S q * γ) :=
      Quotient.exact' (by simp [rep, cls])
    rw [QuotientGroup.rightRel_apply] at h
    simpa [mul_assoc] using h⟩

end RightCosets

section Unipotent

def uMat (t : ℤ) : SL(2, ℤ) :=
  ⟨!![1, t; 0, 1], by rw [Matrix.det_fin_two_of]; ring⟩

@[simp] theorem uMat_apply_00 (t : ℤ) : (uMat t) 0 0 = 1 := rfl
@[simp] theorem uMat_apply_01 (t : ℤ) : (uMat t) 0 1 = t := rfl
@[simp] theorem uMat_apply_10 (t : ℤ) : (uMat t) 1 0 = 0 := rfl
@[simp] theorem uMat_apply_11 (t : ℤ) : (uMat t) 1 1 = 1 := rfl

variable (M : ℕ) (H : Subgroup (ZMod M)ˣ)

theorem uMat_mem_GammaH (t : ℤ) : uMat t ∈ GammaH M H := by
  have h0 : uMat t ∈ Gamma0 M := by
    rw [Gamma0_mem]; show ((0 : ℤ) : ZMod M) = 0; exact Int.cast_zero
  refine mem_GammaH_iff.mpr ⟨h0, ?_⟩
  have e : gamma0Units M ⟨uMat t, h0⟩ = 1 := by
    apply Units.ext; rw [val_gamma0Units, Units.val_one]
    show ((1 : ℤ) : ZMod M) = 1; exact Int.cast_one
  rw [e]; exact H.one_mem

def uElt (t : ℤ) : ↥(GammaH M H) := ⟨uMat t, uMat_mem_GammaH M H t⟩

@[simp] theorem coe_uElt (t : ℤ) : ((uElt M H t : ↥(GammaH M H)) : SL(2, ℤ)) = uMat t := rfl

theorem mul_inv_apply_01 (x y : SL(2, ℤ)) :
    (x * y⁻¹ : SL(2, ℤ)) 0 1 = -(x 0 0 * y 0 1) + x 0 1 * y 0 0 := by
  rw [Matrix.SpecialLinearGroup.coe_mul, Matrix.SpecialLinearGroup.coe_inv, Matrix.adjugate_fin_two,
    Matrix.mul_apply, Fin.sum_univ_two]
  simp only [Fin.isValue, Matrix.of_apply, Matrix.cons_val', Matrix.empty_val',
    Matrix.cons_val_fin_one, Matrix.cons_val_zero, Matrix.cons_val_one]
  ring

variable (ℓ : ℕ)

theorem rightRel_mk_eq_mk_iff (x y : ↥(GammaH M H)) :
    (Quotient.mk'' x : Quotient (QuotientGroup.rightRel (GammaHUpper M H ℓ))) = Quotient.mk'' y ↔
      ((((y : SL(2, ℤ)) * (x : SL(2, ℤ))⁻¹) 0 1 : ℤ) : ZMod ℓ) = 0 := by
  rw [Quotient.eq'', QuotientGroup.rightRel_apply, Subgroup.mem_subgroupOf, mem_Gamma0Upper,
    Subgroup.coe_mul, Subgroup.coe_inv]

attribute [local instance] Subgroup.fintypeQuotientOfFiniteIndex

noncomputable def rightQuotEquivOfDvd [NeZero ℓ] (hℓM : ℓ ∣ M) :
    ZMod ℓ ≃ Quotient (QuotientGroup.rightRel (GammaHUpper M H ℓ)) := by
  refine Equiv.ofBijective (fun j => Quotient.mk'' (uElt M H (j.val : ℤ))) ⟨?_, ?_⟩
  · intro j j' h
    rw [rightRel_mk_eq_mk_iff, mul_inv_apply_01] at h
    simp only [coe_uElt, uMat_apply_00, uMat_apply_01] at h
    push_cast at h; simp only [ZMod.natCast_zmod_val] at h
    linear_combination -h
  · intro q
    induction q using Quotient.inductionOn' with
    | h g =>
      have hdet := Matrix.SpecialLinearGroup.det_coe (g : SL(2, ℤ))
      rw [Matrix.det_fin_two] at hdet
      have hdet' := congrArg (Int.cast : ℤ → ZMod ℓ) hdet
      push_cast at hdet'
      have hg0 : ((g : SL(2, ℤ)) : SL(2, ℤ)) ∈ Gamma0 M := (mem_GammaH_iff.mp g.2).1
      have hc : ((((g : SL(2, ℤ)) 1 0 : ℤ)) : ZMod ℓ) = 0 := by
        rw [ZMod.intCast_zmod_eq_zero_iff_dvd]
        rw [Gamma0_mem, ZMod.intCast_zmod_eq_zero_iff_dvd] at hg0
        exact dvd_trans (Int.natCast_dvd_natCast.mpr hℓM) hg0
      refine ⟨(((g : SL(2, ℤ)) 1 1 : ℤ) : ZMod ℓ) * (((g : SL(2, ℤ)) 0 1 : ℤ) : ZMod ℓ), ?_⟩
      show (Quotient.mk'' (uElt M H (((((g : SL(2, ℤ)) 1 1 : ℤ) : ZMod ℓ)
          * (((g : SL(2, ℤ)) 0 1 : ℤ) : ZMod ℓ)).val : ℤ)) :
          Quotient (QuotientGroup.rightRel (GammaHUpper M H ℓ))) = Quotient.mk'' g
      rw [rightRel_mk_eq_mk_iff, mul_inv_apply_01]
      simp only [coe_uElt, uMat_apply_00, uMat_apply_01]
      push_cast; rw [ZMod.natCast_zmod_val]
      linear_combination (-((((g : SL(2, ℤ)) 0 1 : ℤ)) : ZMod ℓ)) * hdet'
        + (-(((((g : SL(2, ℤ)) 0 1 : ℤ)) : ZMod ℓ) * ((((g : SL(2, ℤ)) 0 1 : ℤ)) : ZMod ℓ))) * hc

@[simp] theorem rightQuotEquivOfDvd_apply [NeZero ℓ] (hℓM : ℓ ∣ M) (j : ZMod ℓ) :
    rightQuotEquivOfDvd M H ℓ hℓM j = Quotient.mk'' (uElt M H (j.val : ℤ)) := rfl

end Unipotent

section CosetProjection

variable {M M' : ℕ} {H : Subgroup (ZMod M)ˣ} {H' : Subgroup (ZMod M')ˣ}
variable (h : LevelLE M M' H H' 1) (ℓ : ℕ)

theorem coe_iotaDeg_one (γ : ↥(GammaH M' H')) :
    ((iotaDeg M M' H H' 1 h γ : ↥(GammaH M H)) : SL(2, ℤ)) = (γ : SL(2, ℤ)) := by
  refine Matrix.SpecialLinearGroup.ext _ _ fun i j => ?_
  fin_cases i <;> fin_cases j <;> simp [iotaDeg, conjLowerMat, Matrix.of_apply, Fin.isValue]

theorem iotaDeg_one_mem_GammaHUpper_iff (z : ↥(GammaH M' H')) :
    iotaDeg M M' H H' 1 h z ∈ GammaHUpper M H ℓ ↔ z ∈ GammaHUpper M' H' ℓ := by
  simp only [GammaHUpper, Subgroup.mem_subgroupOf, mem_Gamma0Upper, coe_iotaDeg_one h]

noncomputable def πCoset :
    Quotient (QuotientGroup.rightRel (GammaHUpper M' H' ℓ)) →
      Quotient (QuotientGroup.rightRel (GammaHUpper M H ℓ)) :=
  Quotient.map' (iotaDeg M M' H H' 1 h) fun x y hxy => by
    rw [QuotientGroup.rightRel_apply] at hxy ⊢
    rw [show (iotaDeg M M' H H' 1 h y) * (iotaDeg M M' H H' 1 h x)⁻¹
      = iotaDeg M M' H H' 1 h (y * x⁻¹) from by rw [map_mul, map_inv]]
    exact (iotaDeg_one_mem_GammaHUpper_iff h ℓ _).mpr hxy

theorem πCoset_mk (γ' : ↥(GammaH M' H')) :
    πCoset h ℓ (Quotient.mk'' γ') = Quotient.mk'' (iotaDeg M M' H H' 1 h γ') :=
  Quotient.map'_mk'' _ _ γ'

end CosetProjection

section LowerLeg

variable (M : ℕ) (H : Subgroup (ZMod M)ˣ) (q : ℕ)

abbrev GammaHLower : Subgroup ↥(GammaH M H) := (Gamma0 (q * M)).subgroupOf (GammaH M H)

instance GammaHLower_finiteIndex [NeZero M] [NeZero q] : (GammaHLower M H q).FiniteIndex := by
  haveI : NeZero (q * M) := ⟨mul_ne_zero (NeZero.ne q) (NeZero.ne M)⟩
  exact Subgroup.instFiniteIndex_subgroupOf _ _

theorem qM_dvd_of_mem_GammaHLower (γ : ↥(GammaHLower M H q)) :
    ((q * M : ℕ) : ℤ) ∣ (γ : SL(2, ℤ)) 1 0 := by
  have h : ((γ : ↥(GammaH M H)) : SL(2, ℤ)) ∈ Gamma0 (q * M) := Subgroup.mem_subgroupOf.mp γ.2
  rw [Gamma0_mem] at h
  exact (ZMod.intCast_zmod_eq_zero_iff_dvd _ _).mp h

theorem dvd_of_mem_GammaHLower (γ : ↥(GammaHLower M H q)) : (q : ℤ) ∣ (γ : SL(2, ℤ)) 1 0 :=
  dvd_trans (by exact_mod_cast dvd_mul_right q M) (qM_dvd_of_mem_GammaHLower M H q γ)

theorem mem_GammaHLower_iff_of_coprime (hqM : Nat.Coprime q M) (γ : ↥(GammaH M H)) :
    γ ∈ GammaHLower M H q ↔ (q : ℤ) ∣ (γ : SL(2, ℤ)) 1 0 := by
  rw [GammaHLower, Subgroup.mem_subgroupOf, Gamma0_mem, ZMod.intCast_zmod_eq_zero_iff_dvd]
  constructor
  · intro h; exact dvd_trans (by exact_mod_cast dvd_mul_right q M) h
  · intro hq
    have hM : (M : ℤ) ∣ (γ : SL(2, ℤ)) 1 0 :=
      (ZMod.intCast_zmod_eq_zero_iff_dvd _ _).mp (Gamma0_mem.mp ((mem_GammaH_iff.mp γ.2).1))
    have hcop : IsCoprime (q : ℤ) (M : ℤ) := Nat.isCoprime_iff_coprime.mpr hqM
    exact_mod_cast hcop.mul_dvd hq hM

theorem conjLowerMat_mem_of_GammaHLower [NeZero q] (γ : ↥(GammaHLower M H q)) :
    conjLowerMat q (γ : SL(2, ℤ)) (dvd_of_mem_GammaHLower M H q γ) ∈ GammaH M H := by
  obtain ⟨hγ0, hγH⟩ := mem_GammaH_iff.mp (γ : ↥(GammaH M H)).2
  rw [mem_GammaH_iff]
  refine ⟨?_, ?_⟩
  · rw [Gamma0_mem]
    show ((((γ : SL(2, ℤ)) 1 0) / (q : ℤ) : ℤ) : ZMod M) = 0
    rw [ZMod.intCast_zmod_eq_zero_iff_dvd]
    obtain ⟨k, hk⟩ := qM_dvd_of_mem_GammaHLower M H q γ
    rw [hk, show ((q * M : ℕ) : ℤ) * k = (q : ℤ) * ((M : ℤ) * k) from by push_cast; ring,
      Int.mul_ediv_cancel_left _ (Nat.cast_ne_zero.mpr (NeZero.ne q))]
    exact Dvd.intro k rfl
  · exact hγH

noncomputable def conjLowerL [NeZero q] : ↥(GammaHLower M H q) →* ↥(GammaH M H) where
  toFun γ := ⟨conjLowerMat q (γ : SL(2, ℤ)) (dvd_of_mem_GammaHLower M H q γ),
    conjLowerMat_mem_of_GammaHLower M H q γ⟩
  map_one' := by
    apply Subtype.ext
    apply Matrix.SpecialLinearGroup.ext
    intro i j
    fin_cases i <;> fin_cases j <;> simp [conjLowerMat]
  map_mul' γ δ :=
    Subtype.ext (conjLowerMat_mul q (γ : SL(2, ℤ)) (δ : SL(2, ℤ)) (dvd_of_mem_GammaHLower M H q γ)
      (dvd_of_mem_GammaHLower M H q δ) (dvd_of_mem_GammaHLower M H q (γ * δ)))

variable (A : Type*) [AddCommGroup A]

noncomputable def heckeTlower [NeZero M] [NeZero q] : H1 M H A →+ H1 M H A where
  toFun φ :=
    MonoidHom.toAdditiveLeft
      (MonoidHom.transfer ((AddMonoidHom.toMultiplicativeRight φ).comp (conjLowerL M H q)))
  map_zero' := by
    simp only [toMultiplicativeRight_zero, MonoidHom.one_comp, transfer_one, toAdditiveLeft_one]
  map_add' φ ψ := by
    simp only [toMultiplicativeRight_add, MonoidHom.mul_comp, transfer_mul, toAdditiveLeft_mul]

end LowerLeg

end CohCarrier