import Definitions.Def_AlgebraicCurve_TotallyDegenerateCovering

set_option autoImplicit false

noncomputable section

namespace CerednikDrinfeld

open Finset

variable {E₁ V₁ E₂ V₂ : Type*} [Fintype E₁] [Fintype V₁] [DecidableEq V₁] [DecidableEq E₂] [DecidableEq V₂]

theorem pushforward_apply_eq_sum_filter {E V : Type*} [Fintype E] [DecidableEq V] (f : E → V) (x : E → ℤ) (v : V) :
    CerednikDrinfeld.pushforward f x v = ∑ e ∈ univ.filter (fun e => f e = v), x e := by
  simp [CerednikDrinfeld.pushforward, Matrix.mulVec, dotProduct, degeneracyMatrix, Finset.sum_filter]

theorem pushforward_pushforward {E E' V : Type*} [Fintype E] [Fintype E'] [DecidableEq E'] [DecidableEq V]
    (g : E → E') (f : E' → V) (x : E → ℤ) :
    CerednikDrinfeld.pushforward f (CerednikDrinfeld.pushforward g x) = CerednikDrinfeld.pushforward (f ∘ g) x := by
  ext v
  rw [pushforward_apply_eq_sum_filter, pushforward_apply_eq_sum_filter,
    ← sum_fiberwise_of_maps_to (s := univ.filter (fun e => (f ∘ g) e = v)) (t := univ.filter (fun e' => f e' = v))
      (g := g) (fun e he => by simpa using he)]
  refine sum_congr rfl fun e' he' => ?_
  rw [pushforward_apply_eq_sum_filter, filter_filter]
  have hv := (mem_filter.mp he').2
  refine sum_congr (filter_congr fun e _ => ?_) fun _ _ => rfl
  simp only [Function.comp_apply]
  exact ⟨fun h => ⟨by rw [h]; exact hv, h⟩, fun h => h.2⟩

theorem ribbonGram_comm {E V : Type*} [Fintype E] [DecidableEq V] (D : DegeneracyData E V) (x y : ↥(ribbonKernel D)) :
    ribbonGram D x y = ribbonGram D y x := by
  simp only [ribbonGram_apply, mul_comm (x.1 _) (y.1 _)]

structure DegeneracyData.FiniteHom (D₁ : DegeneracyData E₁ V₁) (D₂ : DegeneracyData E₂ V₂) where

  mapV : V₁ → V₂

  mapE : E₁ → E₂

  a_mapE : ∀ e, D₂.a (mapE e) = mapV (D₁.a e)

  b_mapE : ∀ e, D₂.b (mapE e) = mapV (D₁.b e)

  deg : E₁ → ℕ+

  degV : V₁ → ℕ+

  degTotal : ℕ+

  w_mapE : ∀ e, D₂.w (mapE e) = deg e * D₁.w e

  sum_deg_a : ∀ (v : V₁) (e' : E₂), D₂.a e' = mapV v →
    ∑ e ∈ univ.filter (fun e => D₁.a e = v ∧ mapE e = e'), (deg e : ℕ) = degV v

  sum_deg_b : ∀ (v : V₁) (e' : E₂), D₂.b e' = mapV v →
    ∑ e ∈ univ.filter (fun e => D₁.b e = v ∧ mapE e = e'), (deg e : ℕ) = degV v

  sum_degV : ∀ v' : V₂, ∑ v ∈ univ.filter (fun v => mapV v = v'), (degV v : ℕ) = degTotal

namespace DegeneracyData.FiniteHom

variable {D₁ : DegeneracyData E₁ V₁} {D₂ : DegeneracyData E₂ V₂} (μ : D₁.FiniteHom D₂)

theorem sum_deg_fibre (e' : E₂) : ∑ e ∈ univ.filter (fun e => μ.mapE e = e'), (μ.deg e : ℕ) = μ.degTotal := by
  rw [← μ.sum_degV (D₂.a e'),
    ← sum_fiberwise_of_maps_to (s := univ.filter (fun e => μ.mapE e = e'))
      (t := univ.filter (fun v => μ.mapV v = D₂.a e')) (g := D₁.a)
      (fun e he => by simp only [mem_filter, mem_univ, true_and] at he ⊢; rw [← μ.a_mapE, he])]
  refine sum_congr rfl fun v hv => ?_
  rw [filter_filter, ← μ.sum_deg_a v e' (mem_filter.mp hv).2.symm]
  exact sum_congr (filter_congr fun _ _ => and_comm) fun _ _ => rfl

theorem mapV_surjective : Function.Surjective μ.mapV := fun v' => by
  by_contra h
  have h0 : ∑ v ∈ univ.filter (fun v => μ.mapV v = v'), (μ.degV v : ℕ) = 0 :=
    sum_eq_zero fun v hv => absurd ⟨v, (mem_filter.mp hv).2⟩ h
  rw [μ.sum_degV] at h0
  exact (μ.degTotal).ne_zero h0

theorem mapE_surjective : Function.Surjective μ.mapE := fun e' => by
  by_contra h
  have h0 : ∑ e ∈ univ.filter (fun e => μ.mapE e = e'), (μ.deg e : ℕ) = 0 :=
    sum_eq_zero fun e he => absurd ⟨e, (mem_filter.mp he).2⟩ h
  rw [μ.sum_deg_fibre] at h0
  exact (μ.degTotal).ne_zero h0

def pullbackFun : (E₂ → ℤ) →ₗ[ℤ] (E₁ → ℤ) :=
  LinearMap.pi fun e => (μ.deg e : ℤ) • LinearMap.proj (μ.mapE e)

@[simp] theorem pullbackFun_apply (y : E₂ → ℤ) (e : E₁) : μ.pullbackFun y e = (μ.deg e : ℤ) * y (μ.mapE e) := rfl

variable [Fintype E₂]

private theorem pushforward_deg_mul {a₁ : E₁ → V₁} {a₂ : E₂ → V₂} (ha : ∀ e, a₂ (μ.mapE e) = μ.mapV (a₁ e))
    (hsum : ∀ (v : V₁) (e' : E₂), a₂ e' = μ.mapV v →
      ∑ e ∈ univ.filter (fun e => a₁ e = v ∧ μ.mapE e = e'), (μ.deg e : ℕ) = μ.degV v)
    (y : E₂ → ℤ) (v : V₁) :
    CerednikDrinfeld.pushforward a₁ (fun e => (μ.deg e : ℤ) * y (μ.mapE e)) v =
      (μ.degV v : ℤ) * CerednikDrinfeld.pushforward a₂ y (μ.mapV v) := by
  rw [pushforward_apply_eq_sum_filter, pushforward_apply_eq_sum_filter, mul_sum,
    ← sum_fiberwise_of_maps_to (s := univ.filter (fun e => a₁ e = v)) (t := univ.filter (fun e' => a₂ e' = μ.mapV v))
      (g := μ.mapE) (fun e he => by simp only [mem_filter, mem_univ, true_and] at he ⊢; rw [ha, he])]
  refine sum_congr rfl fun e' he' => ?_
  rw [filter_filter, ← hsum v e' (mem_filter.mp he').2, Nat.cast_sum, sum_mul]
  exact sum_congr rfl fun e he => by rw [(mem_filter.mp he).2.2]

def pushforward : ↥(ribbonKernel D₁) →ₗ[ℤ] ↥(ribbonKernel D₂) :=
  (CerednikDrinfeld.pushforward μ.mapE).restrict fun x hx => by
    rw [mem_ribbonKernel] at hx ⊢
    have h : ∀ {f₁ : E₁ → V₁} {f₂ : E₂ → V₂}, (∀ e, f₂ (μ.mapE e) = μ.mapV (f₁ e)) →
        CerednikDrinfeld.pushforward f₁ x = 0 →
        CerednikDrinfeld.pushforward f₂ (CerednikDrinfeld.pushforward μ.mapE x) = 0 := fun hf h0 => by
      rw [pushforward_pushforward, show _ ∘ μ.mapE = μ.mapV ∘ _ from funext hf, ← pushforward_pushforward, h0,
        map_zero]
    intro i
    fin_cases i
    · exact h μ.a_mapE (hx 0)
    · exact h μ.b_mapE (hx 1)

@[simp] theorem pushforward_apply (x : ↥(ribbonKernel D₁)) (e' : E₂) :
    (μ.pushforward x : E₂ → ℤ) e' = ∑ e ∈ univ.filter (fun e => μ.mapE e = e'), (x : E₁ → ℤ) e :=
  pushforward_apply_eq_sum_filter _ _ _

def pullback : ↥(ribbonKernel D₂) →ₗ[ℤ] ↥(ribbonKernel D₁) :=
  μ.pullbackFun.restrict fun y hy => by
    rw [mem_ribbonKernel] at hy ⊢
    intro i
    fin_cases i
    · ext v
      change CerednikDrinfeld.pushforward D₁.a (fun e => (μ.deg e : ℤ) * y (μ.mapE e)) v = 0
      rw [μ.pushforward_deg_mul μ.a_mapE μ.sum_deg_a, show CerednikDrinfeld.pushforward D₂.a y = 0 from hy 0,
        Pi.zero_apply, mul_zero]
    · ext v
      change CerednikDrinfeld.pushforward D₁.b (fun e => (μ.deg e : ℤ) * y (μ.mapE e)) v = 0
      rw [μ.pushforward_deg_mul μ.b_mapE μ.sum_deg_b, show CerednikDrinfeld.pushforward D₂.b y = 0 from hy 1,
        Pi.zero_apply, mul_zero]

@[simp] theorem pullback_apply (y : ↥(ribbonKernel D₂)) (e : E₁) :
    (μ.pullback y : E₁ → ℤ) e = (μ.deg e : ℤ) * (y : E₂ → ℤ) (μ.mapE e) := rfl

theorem ribbonGram_pushforward (x : ↥(ribbonKernel D₁)) (y : ↥(ribbonKernel D₂)) :
    ribbonGram D₂ (μ.pushforward x) y = ribbonGram D₁ x (μ.pullback y) := by
  simp only [ribbonGram_apply, pushforward_apply, pullback_apply, sum_mul, mul_sum]
  rw [← sum_fiberwise (s := (univ : Finset E₁)) (g := μ.mapE)]
  refine sum_congr rfl fun e' _ => sum_congr rfl fun e he => ?_
  rw [← (mem_filter.mp he).2, μ.w_mapE, PNat.mul_coe, Nat.cast_mul]
  ring

theorem ribbonGram_pullback_left (y : ↥(ribbonKernel D₂)) (x : ↥(ribbonKernel D₁)) :
    ribbonGram D₁ (μ.pullback y) x = ribbonGram D₂ y (μ.pushforward x) := by
  rw [ribbonGram_comm, ← ribbonGram_pushforward, ribbonGram_comm]

theorem ribbonGram_pullback (x y : ↥(ribbonKernel D₂)) :
    ribbonGram D₁ (μ.pullback x) (μ.pullback y) = (μ.degTotal : ℤ) * ribbonGram D₂ x y := by
  simp only [ribbonGram_apply, pullback_apply, mul_sum]
  rw [← sum_fiberwise (s := (univ : Finset E₁)) (g := μ.mapE)]
  refine sum_congr rfl fun e' _ => ?_
  rw [← μ.sum_deg_fibre e', Nat.cast_sum, sum_mul]
  refine sum_congr rfl fun e he => ?_
  rw [← (mem_filter.mp he).2, μ.w_mapE, PNat.mul_coe, Nat.cast_mul]
  ring

theorem pushforward_pullback (y : ↥(ribbonKernel D₂)) : μ.pushforward (μ.pullback y) = (μ.degTotal : ℤ) • y := by
  apply Subtype.ext
  funext e'
  rw [pushforward_apply, Submodule.coe_smul, Pi.smul_apply, smul_eq_mul, ← μ.sum_deg_fibre e', Nat.cast_sum, sum_mul]
  exact sum_congr rfl fun e he => by rw [pullback_apply, (mem_filter.mp he).2]

section IdComp

omit [Fintype E₂]

protected def id (D : DegeneracyData E₁ V₁) [DecidableEq E₁] : D.FiniteHom D where
  mapV := id
  mapE := id
  a_mapE _ := rfl
  b_mapE _ := rfl
  deg _ := 1
  degV _ := 1
  degTotal := 1
  w_mapE e := (one_mul _).symm
  sum_deg_a v e' h := by
    rw [sum_eq_single_of_mem e' (mem_filter.mpr ⟨mem_univ _, h, rfl⟩)
      (fun e he hne => absurd (mem_filter.mp he).2.2 hne)]
  sum_deg_b v e' h := by
    rw [sum_eq_single_of_mem e' (mem_filter.mpr ⟨mem_univ _, h, rfl⟩)
      (fun e he hne => absurd (mem_filter.mp he).2.2 hne)]
  sum_degV v' := by
    rw [sum_eq_single_of_mem (s := univ.filter fun v => id v = v') v' (mem_filter.mpr ⟨mem_univ _, rfl⟩)
      (fun v hv hne => absurd (mem_filter.mp hv).2 hne)]

variable {E₃ V₃ : Type*} [Fintype E₂] [Fintype V₂] [DecidableEq E₃] [DecidableEq V₃] {D₃ : DegeneracyData E₃ V₃}

def comp (ν : D₂.FiniteHom D₃) (μ : D₁.FiniteHom D₂) : D₁.FiniteHom D₃ where
  mapV := ν.mapV ∘ μ.mapV
  mapE := ν.mapE ∘ μ.mapE
  a_mapE e := by simp only [Function.comp_apply, ν.a_mapE, μ.a_mapE]
  b_mapE e := by simp only [Function.comp_apply, ν.b_mapE, μ.b_mapE]
  deg e := μ.deg e * ν.deg (μ.mapE e)
  degV v := μ.degV v * ν.degV (μ.mapV v)
  degTotal := μ.degTotal * ν.degTotal
  w_mapE e := by simp only [Function.comp_apply, ν.w_mapE, μ.w_mapE]; rw [mul_assoc, mul_left_comm]
  sum_deg_a v e'' h := by
    rw [← sum_fiberwise_of_maps_to (t := univ.filter (fun e' => D₂.a e' = μ.mapV v ∧ ν.mapE e' = e''))
      (g := μ.mapE) (fun e he => by
        simp only [mem_filter, mem_univ, true_and, Function.comp_apply] at he ⊢
        exact ⟨by rw [μ.a_mapE, he.1], he.2⟩),
      PNat.mul_coe, ← ν.sum_deg_a (μ.mapV v) e'' h, mul_sum]
    refine sum_congr rfl fun e' he' => ?_
    rw [filter_filter, ← μ.sum_deg_a v e' (mem_filter.mp he').2.1, sum_mul]
    refine sum_congr (filter_congr fun e _ => ?_) fun e he => by rw [PNat.mul_coe, (mem_filter.mp he).2.2]
    simp only [Function.comp_apply]
    exact ⟨fun h => ⟨h.1.1, h.2⟩, fun h => ⟨⟨h.1, by rw [h.2]; exact (mem_filter.mp he').2.2⟩, h.2⟩⟩
  sum_deg_b v e'' h := by
    rw [← sum_fiberwise_of_maps_to (t := univ.filter (fun e' => D₂.b e' = μ.mapV v ∧ ν.mapE e' = e''))
      (g := μ.mapE) (fun e he => by
        simp only [mem_filter, mem_univ, true_and, Function.comp_apply] at he ⊢
        exact ⟨by rw [μ.b_mapE, he.1], he.2⟩),
      PNat.mul_coe, ← ν.sum_deg_b (μ.mapV v) e'' h, mul_sum]
    refine sum_congr rfl fun e' he' => ?_
    rw [filter_filter, ← μ.sum_deg_b v e' (mem_filter.mp he').2.1, sum_mul]
    refine sum_congr (filter_congr fun e _ => ?_) fun e he => by rw [PNat.mul_coe, (mem_filter.mp he).2.2]
    simp only [Function.comp_apply]
    exact ⟨fun h => ⟨h.1.1, h.2⟩, fun h => ⟨⟨h.1, by rw [h.2]; exact (mem_filter.mp he').2.2⟩, h.2⟩⟩
  sum_degV v'' := by
    rw [← sum_fiberwise_of_maps_to (t := univ.filter (fun v' => ν.mapV v' = v'')) (g := μ.mapV)
      (fun v hv => by simpa using hv), PNat.mul_coe, ← ν.sum_degV v'', mul_sum]
    refine sum_congr rfl fun v' hv' => ?_
    rw [filter_filter, ← μ.sum_degV v', sum_mul]
    refine sum_congr (filter_congr fun v _ => ?_) fun v hv => by rw [PNat.mul_coe, (mem_filter.mp hv).2]
    simp only [Function.comp_apply]
    exact ⟨fun h => h.2, fun h => ⟨by rw [h]; exact (mem_filter.mp hv').2, h⟩⟩

@[simp] theorem comp_mapE (ν : D₂.FiniteHom D₃) (μ : D₁.FiniteHom D₂) (e : E₁) :
    (ν.comp μ).mapE e = ν.mapE (μ.mapE e) := rfl
@[simp] theorem comp_deg (ν : D₂.FiniteHom D₃) (μ : D₁.FiniteHom D₂) (e : E₁) :
    (ν.comp μ).deg e = μ.deg e * ν.deg (μ.mapE e) := rfl

end IdComp

end DegeneracyData.FiniteHom

end CerednikDrinfeld

namespace AlgebraicCurve

namespace TotallyDegenerateCovering

open CerednikDrinfeld

variable {L : Type} [Field L] {A : ValuationSubring L} {ϖ : A}
variable {Fj Fk : Type} [Field Fj] [Field Fk] [Algebra L Fj] [Algebra L Fk] [Algebra Fj Fk]

def PlaceOver (P : Place L Fk) (Q : Place L Fj) : Prop :=
  P.toValuationSubring.comap (algebraMap Fj Fk) = Q.toValuationSubring

variable [IsScalarTower L Fj Fk]

structure Hom [IsScalarTower L Fj Fk] (𝒞k : TotallyDegenerateCovering A Fk ϖ) (𝒞j : TotallyDegenerateCovering A Fj ϖ)
    extends DegeneracyData.FiniteHom 𝒞k.toDegeneracyData 𝒞j.toDegeneracyData where

  side_mapV : ∀ v, 𝒞j.side (mapV v) = 𝒞k.side v

  integers_comap : ∀ v, (𝒞k.chart v).integers.comap (algebraMap Fj Fk) = (𝒞j.chart (mapV v)).integers

  dom_chart : ∀ (v : 𝒞k.V) (P : Place L Fk) (Q : Place L Fj), PlaceOver P Q →
    P ∈ (𝒞k.chart v).dom → Q ∈ (𝒞j.chart (mapV v)).dom

  dom_ann : ∀ (e : 𝒞k.E) (P : Place L Fk) (Q : Place L Fj), PlaceOver P Q →
    P ∈ (𝒞k.annOut e).dom → Q ∈ (𝒞j.annOut (mapE e)).dom

  valuation_evalAt_param : ∀ (e : 𝒞k.E) (P : Place L Fk) (Q : Place L Fj), PlaceOver P Q → P ∈ (𝒞k.annOut e).dom →
    A.valuation (Q.evalAt (𝒞j.annOut (mapE e)).param) = A.valuation (P.evalAt (𝒞k.annOut e).param) ^ (deg e : ℕ)

namespace Hom

variable {𝒞k : TotallyDegenerateCovering A Fk ϖ} {𝒞j : TotallyDegenerateCovering A Fj ϖ} (μ : 𝒞k.Hom 𝒞j)

theorem src_mapE (e : 𝒞k.E) : 𝒞j.src (μ.mapE e) = μ.mapV (𝒞k.src e) := μ.a_mapE e
theorem tgt_mapE (e : 𝒞k.E) : 𝒞j.tgt (μ.mapE e) = μ.mapV (𝒞k.tgt e) := μ.b_mapE e

theorem width_mapE (e : 𝒞k.E) : 𝒞j.width (μ.mapE e) = μ.deg e * 𝒞k.width e := μ.w_mapE e

theorem valuation_modulus_mapE (e : 𝒞k.E) :
    A.valuation ((𝒞j.annOut (μ.mapE e)).modulus : L) = A.valuation ((𝒞k.annOut e).modulus : L) ^ (μ.deg e : ℕ) := by
  rw [𝒞j.valuation_modulus, 𝒞k.valuation_modulus, ← pow_mul, μ.width_mapE, PNat.mul_coe, mul_comm]

def DegreeMatches : Prop := (μ.degTotal : ℕ) = Module.finrank Fj Fk

theorem degreeMatches_iff : μ.DegreeMatches ↔ (μ.degTotal : ℕ) = Module.finrank Fj Fk := Iff.rfl

theorem pullback_apply_eq_zero {y : ↥(ribbonKernel 𝒞j.toDegeneracyData)} {e : 𝒞k.E}
    (h : (y : 𝒞j.E → ℤ) (μ.mapE e) = 0) : (μ.pullback y : 𝒞k.E → ℤ) e = 0 := by
  rw [μ.pullback_apply, h, mul_zero]

theorem eq_of_placeOver {F : Type} [Field F] [Algebra L F] {P Q : Place L F} (h : PlaceOver P Q) : P = Q :=
  Place.ext ((SetLike.ext fun _ => Iff.rfl).trans h)

protected def id {F : Type} [Field F] [Algebra L F] (𝒞 : TotallyDegenerateCovering A F ϖ) : 𝒞.Hom 𝒞 where
  toFiniteHom := DegeneracyData.FiniteHom.id 𝒞.toDegeneracyData
  side_mapV _ := rfl
  integers_comap _ := SetLike.ext fun _ => Iff.rfl
  dom_chart _ _ _ h hP := eq_of_placeOver h ▸ hP
  dom_ann _ _ _ h hP := eq_of_placeOver h ▸ hP
  valuation_evalAt_param _ _ _ h _ := by rw [← eq_of_placeOver h]; exact (pow_one _).symm

theorem degreeMatches_id {F : Type} [Field F] [Algebra L F] (𝒞 : TotallyDegenerateCovering A F ϖ) :
    (Hom.id 𝒞).DegreeMatches := (Module.finrank_self F).symm

end Hom

end TotallyDegenerateCovering

end AlgebraicCurve

end