import Mathlib
import Definitions.Def_AlgebraicCurve_IsCurveOver
import Definitions.Def_AlgebraicCurve_DivisorPushPull
import Definitions.Def_AlgebraicCurve_RatFuncPlaces
import Definitions.Def_AlgebraicCurve_FrobeniusEndo
import Definitions.Def_AlgebraicCurve_FrobeniusEndoPic0
import Definitions.Def_ModularCurve_JqCoeff
import Definitions.Def_ModularCurve_FibrePoly
import Definitions.Def_HeckeGalois_EichlerShimura
import Theorems.Thm_ModularCurve_frobenius_identity_geom_unconditional

set_option autoImplicit false

noncomputable section

open AlgebraicCurve Polynomial

set_option synthInstance.maxHeartbeats 400000
set_option maxHeartbeats 800000

namespace ModularCurve

section ConstantEmbedding
variable {R : Type*} [CommRing R]

theorem algebraMap_laurentSeries_apply_eq_single (c : R) :
    algebraMap R (LaurentSeries R) c = HahnSeries.single 0 c := by
  have h1 : algebraMap R (PowerSeries R) c = PowerSeries.C c := by simp
  rw [HahnSeries.algebraMap_apply', h1, HahnSeries.ofPowerSeries_C]
  rfl
end ConstantEmbedding

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

def qExpandAlgC : LaurentSeries K →ₐ[K] LaurentSeries K where
  __ := qExpand K N
  commutes' r := by
    show qExpand K N (algebraMap K (LaurentSeries K) r) = algebraMap K (LaurentSeries K) r
    rw [algebraMap_laurentSeries_apply_eq_single, qExpand_single, mul_zero]
@[simp]
theorem qExpandAlgC_apply (f : LaurentSeries K) : qExpandAlgC K N f = qExpand K N f := rfl
end QExpandAlg

section FrobId
variable (K : Type*) [Field K] {ℓ : ℕ} [Fact ℓ.Prime] [CharP K ℓ]

theorem ModularPolynomialData.frobenius_identity_geom (_data : ModularPolynomialData ℓ)
    (_hK : KroneckerCongruence ℓ _data) :
    jqNModC K ℓ = (jqModC K) ^ ℓ :=
  frobenius_identity_geom_unconditional K
end FrobId

section DegOneBridge
open AlgebraicCurve
variable (K : Type*) [Field K] (N : ℕ) [NeZero N] [IsAlgClosed K]
    [IsCurveOver K (modularFunctionFieldC K N)]

theorem deg_eq_one_modularFunctionFieldC :
    ∀ w : Place K (modularFunctionFieldC K N), w.deg = 1 :=
  IsCurveOver.forall_deg_eq_one_of_isAlgClosed
end DegOneBridge

end ModularCurve

noncomputable section

open AlgebraicCurve Polynomial

set_option synthInstance.maxHeartbeats 400000
set_option maxHeartbeats 800000

namespace ModularCurve

section FrobeniusEndomorphism

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

include data hKr in

theorem qExpand_jqModC_eq_pow : qExpand K ℓ (jqModC K) = (jqModC K) ^ ℓ :=
  data.frobenius_identity_geom K hKr

include data hKr in

theorem qExpand_jqNModC_eq_pow : qExpand K ℓ (jqNModC K N) = (jqNModC K N) ^ ℓ := by
  rw [jqNModC, qExpand_qExpand, qExpand_congr (mul_comm ℓ N), ← qExpand_qExpand,
    qExpand_jqModC_eq_pow K data hKr, map_pow]

include data hKr in

theorem frobeniusGeomLevel_map_le :
    (modularFunctionFieldC K N).map (qExpandAlgC K ℓ) ≤ modularFunctionFieldC K N := by
  show (IntermediateField.adjoin K {jqModC K, jqNModC K N}).map (qExpandAlgC K ℓ) ≤ _
  rw [IntermediateField.adjoin_map, Set.image_pair, IntermediateField.adjoin_le_iff]
  rintro x (rfl | rfl)
  · show qExpandAlgC K ℓ (jqModC K) ∈ modularFunctionFieldC K N
    rw [qExpandAlgC_apply, qExpand_jqModC_eq_pow K data hKr]
    exact pow_mem (jqModC_mem K N) ℓ
  · show qExpandAlgC K ℓ (jqNModC K N) ∈ modularFunctionFieldC K N
    rw [qExpandAlgC_apply, qExpand_jqNModC_eq_pow K N data hKr]
    exact pow_mem (jqNModC_mem K N) ℓ

def frobeniusGeomLevelImage : IntermediateField K (LaurentSeries K) :=
  (modularFunctionFieldC K N).map (qExpandAlgC K ℓ)

def frobeniusGeomLevelEquiv :
    (modularFunctionFieldC K N) ≃ₐ[K] (frobeniusGeomLevelImage K N (ℓ := ℓ)) :=
  (modularFunctionFieldC K N).equivMap (qExpandAlgC K ℓ)

omit [CharP K ℓ] in
@[simp]
theorem coe_frobeniusGeomLevelEquiv_apply (x : modularFunctionFieldC K N) :
    (frobeniusGeomLevelEquiv K N (ℓ := ℓ) x : LaurentSeries K)
      = qExpand K ℓ (x : LaurentSeries K) :=
  IntermediateField.coe_equivMap_apply _ _ x

include data hKr in

def frobeniusGeomLevel : modularFunctionFieldC K N →ₐ[K] modularFunctionFieldC K N :=
  (IntermediateField.inclusion (frobeniusGeomLevel_map_le K N data hKr)).comp
    (frobeniusGeomLevelEquiv K N (ℓ := ℓ)).toAlgHom

@[simp]
theorem frobeniusGeomLevel_apply_coe (x : modularFunctionFieldC K N) :
    (frobeniusGeomLevel K N data hKr x : LaurentSeries K)
      = qExpand K ℓ (x : LaurentSeries K) := by
  refine (IntermediateField.coe_inclusion (frobeniusGeomLevel_map_le K N data hKr)
    _).trans ?_
  exact coe_frobeniusGeomLevelEquiv_apply K N x

theorem frobeniusGeomLevel_jq :
    frobeniusGeomLevel K N data hKr ⟨jqModC K, jqModC_mem K N⟩
      = (⟨jqModC K, jqModC_mem K N⟩ : modularFunctionFieldC K N) ^ ℓ := by
  refine Subtype.ext ?_
  rw [frobeniusGeomLevel_apply_coe]
  push_cast
  exact qExpand_jqModC_eq_pow K data hKr

theorem frobeniusGeomLevel_jqN :
    frobeniusGeomLevel K N data hKr ⟨jqNModC K N, jqNModC_mem K N⟩
      = (⟨jqNModC K N, jqNModC_mem K N⟩ : modularFunctionFieldC K N) ^ ℓ := by
  refine Subtype.ext ?_
  rw [frobeniusGeomLevel_apply_coe]
  push_cast
  exact qExpand_jqNModC_eq_pow K N data hKr

theorem frobeniusGeomLevel_injective :
    Function.Injective (frobeniusGeomLevel K N data hKr) := by
  intro x y h
  have h' := congrArg (fun z : modularFunctionFieldC K N => (z : LaurentSeries K)) h
  simp only [frobeniusGeomLevel_apply_coe] at h'
  exact Subtype.ext (qExpand_injective _ h')

theorem exists_frobeniusGeomLevel_eq_iff (x : modularFunctionFieldC K N) :
    (∃ y, frobeniusGeomLevel K N data hKr y = x)
      ↔ (x : LaurentSeries K) ∈ frobeniusGeomLevelImage K N (ℓ := ℓ) := by
  constructor
  · rintro ⟨y, rfl⟩
    rw [frobeniusGeomLevel_apply_coe]
    exact ⟨(y : LaurentSeries K), y.2, rfl⟩
  · rintro ⟨y, hy, hyx⟩
    refine ⟨⟨y, hy⟩, Subtype.ext ?_⟩
    rw [frobeniusGeomLevel_apply_coe]
    exact hyx

end FrobeniusEndomorphism

section PurelyInseparable

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

omit [Fact ℓ.Prime] in

theorem charP_laurentSeries : CharP (LaurentSeries K) ℓ :=
  charP_of_injective_algebraMap (algebraMap K (LaurentSeries K)).injective ℓ

include data hKr in

theorem pow_mem_frobeniusGeomLevelImage
    {x : LaurentSeries K} (hx : x ∈ modularFunctionFieldC K N) :
    x ^ ℓ ∈ frobeniusGeomLevelImage K N (ℓ := ℓ) := by
  haveI : CharP (LaurentSeries K) ℓ := charP_laurentSeries K
  induction hx using IntermediateField.adjoin_induction with
  | mem y hy =>
    rcases hy with rfl | rfl
    · rw [← qExpand_jqModC_eq_pow K data hKr]
      exact ⟨jqModC K, jqModC_mem K N, rfl⟩
    · rw [← qExpand_jqNModC_eq_pow K N data hKr]
      exact ⟨jqNModC K N, jqNModC_mem K N, rfl⟩
  | algebraMap c =>
    rw [← map_pow]
    exact (frobeniusGeomLevelImage K N (ℓ := ℓ)).algebraMap_mem (c ^ ℓ)
  | add y z _ _ hy hz =>
    rw [add_pow_char]
    exact add_mem hy hz
  | inv y _ hy =>
    rw [inv_pow]
    exact inv_mem hy
  | mul y z _ _ hy hz =>
    rw [mul_pow]
    exact mul_mem hy hz

theorem exists_frobeniusGeomLevel_eq_pow (x : modularFunctionFieldC K N) :
    ∃ y, frobeniusGeomLevel K N data hKr y = x ^ ℓ := by
  rw [exists_frobeniusGeomLevel_eq_iff]
  show (x : LaurentSeries K) ^ ℓ ∈ frobeniusGeomLevelImage K N (ℓ := ℓ)
  exact pow_mem_frobeniusGeomLevelImage K N data hKr x.2

theorem _root_.ValuationSubring.mem_of_pow_mem' {F : Type*} [Field F]
    (A : ValuationSubring F) {x : F} {n : ℕ} (hn : n ≠ 0) (h : x ^ n ∈ A) : x ∈ A := by
  rcases A.mem_or_inv_mem x with hx | hx
  · exact hx
  rcases eq_or_ne x 0 with rfl | hx0
  · exact A.zero_mem
  have hpow : x ^ n = x * x ^ (n - 1) := by
    rw [← pow_succ']
    exact congrArg (x ^ ·) (by omega)
  have hkey : x ^ n * (x⁻¹) ^ (n - 1) = x := by
    rw [hpow, inv_pow, mul_assoc, mul_inv_cancel₀ (pow_ne_zero _ hx0), mul_one]
  rw [← hkey]
  exact A.mul_mem _ _ h (pow_mem hx _)

theorem mem_valuationSubring_iff_pow_mem {F : Type*} [Field F] (A : ValuationSubring F)
    (x : F) : x ∈ A ↔ x ^ ℓ ∈ A :=
  ⟨fun h => pow_mem h ℓ,
    fun h => ValuationSubring.mem_of_pow_mem' A (Fact.out : ℓ.Prime).pos.ne' h⟩

end PurelyInseparable

section PlaceLevel

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

include data hKr in

@[reducible] def frobImageAlgebra :
    Algebra (frobeniusGeomLevelImage K N (ℓ := ℓ)) (modularFunctionFieldC K N) :=
  (IntermediateField.inclusion (frobeniusGeomLevel_map_le K N data hKr)).toRingHom.toAlgebra

theorem frobImageTower :
    letI := frobImageAlgebra K N data hKr
    IsScalarTower K (frobeniusGeomLevelImage K N (ℓ := ℓ)) (modularFunctionFieldC K N) :=
  letI := frobImageAlgebra K N data hKr
  IsScalarTower.of_algebraMap_eq fun _ => Subtype.ext rfl

theorem frobImageIsIntegral :
    letI := frobImageAlgebra K N data hKr
    Algebra.IsIntegral (frobeniusGeomLevelImage K N (ℓ := ℓ))
      (modularFunctionFieldC K N) := by
  letI := frobImageAlgebra K N data hKr
  refine ⟨fun x => ?_⟩
  refine ⟨Polynomial.X ^ ℓ - Polynomial.C
    ⟨(x : LaurentSeries K) ^ ℓ, pow_mem_frobeniusGeomLevelImage K N data hKr x.2⟩,
    Polynomial.monic_X_pow_sub_C _ (Fact.out : ℓ.Prime).pos.ne', ?_⟩
  rw [Polynomial.eval₂_sub, Polynomial.eval₂_X_pow, Polynomial.eval₂_C, sub_eq_zero]
  exact Subtype.ext rfl

include data hKr in

def frobOnPlacesGeomLevel (w : Place K (modularFunctionFieldC K N)) :
    Place K (modularFunctionFieldC K N) :=
  letI := frobImageAlgebra K N data hKr
  letI := frobImageTower K N data hKr
  letI := frobImageIsIntegral K N data hKr
  (Place.congrEquiv (frobeniusGeomLevelEquiv K N (ℓ := ℓ)).toRingEquiv
    (fun a => (frobeniusGeomLevelEquiv K N (ℓ := ℓ)).commutes a)).symm
    (w.restrict (frobeniusGeomLevelImage K N (ℓ := ℓ)))

theorem mem_frobOnPlacesGeomLevel_iff (w : Place K (modularFunctionFieldC K N))
    (x : modularFunctionFieldC K N) :
    x ∈ (frobOnPlacesGeomLevel K N data hKr w).toValuationSubring
      ↔ frobeniusGeomLevel K N data hKr x ∈ w.toValuationSubring := by
  letI := frobImageAlgebra K N data hKr
  letI := frobImageTower K N data hKr
  letI := frobImageIsIntegral K N data hKr
  rw [show frobOnPlacesGeomLevel K N data hKr w
      = (Place.congrEquiv (frobeniusGeomLevelEquiv K N (ℓ := ℓ)).toRingEquiv
          (fun a => (frobeniusGeomLevelEquiv K N (ℓ := ℓ)).commutes a)).symm
          (w.restrict (frobeniusGeomLevelImage K N (ℓ := ℓ))) from rfl,
    Place.congrEquiv_symm_apply, Place.congrRingEquiv_toValuationSubring,
    ValuationSubring.mem_comap, RingEquiv.symm_symm]
  exact Iff.rfl

theorem frobOnPlacesGeomLevel_injective :
    Function.Injective (frobOnPlacesGeomLevel K N data hKr) := by
  intro w w' h
  ext1
  refine SetLike.ext fun x => ?_
  obtain ⟨y, hy⟩ := exists_frobeniusGeomLevel_eq_pow K N data hKr x
  rw [mem_valuationSubring_iff_pow_mem (ℓ := ℓ) w.toValuationSubring x, ← hy,
    ← mem_frobOnPlacesGeomLevel_iff K N data hKr w y, h,
    mem_frobOnPlacesGeomLevel_iff K N data hKr w' y, hy,
    ← mem_valuationSubring_iff_pow_mem (ℓ := ℓ) w'.toValuationSubring x]

include data hKr in
open Classical in

def verOnPlacesGeomLevel (u : Place K (modularFunctionFieldC K N)) :
    Place K (modularFunctionFieldC K N) :=
  if h : ∃ w, frobOnPlacesGeomLevel K N data hKr w = u then h.choose else u

theorem verOnPlacesGeomLevel_frobOnPlacesGeomLevel
    (w : Place K (modularFunctionFieldC K N)) :
    verOnPlacesGeomLevel K N data hKr (frobOnPlacesGeomLevel K N data hKr w) = w := by
  rw [verOnPlacesGeomLevel, dif_pos ⟨w, rfl⟩]
  exact frobOnPlacesGeomLevel_injective K N data hKr
    (Exists.choose_spec (⟨w, rfl⟩ : ∃ w', frobOnPlacesGeomLevel K N data hKr w'
      = frobOnPlacesGeomLevel K N data hKr w))

end PlaceLevel

section DivisorLevel

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

include data hKr in

def frobeniusPushforwardGeomLevel :
    Divisor K (modularFunctionFieldC K N) →+ Divisor K (modularFunctionFieldC K N) :=
  Finsupp.mapDomain.addMonoidHom (frobOnPlacesGeomLevel K N data hKr)

include data hKr in

def frobeniusPullbackGeomLevel :
    Divisor K (modularFunctionFieldC K N) →+ Divisor K (modularFunctionFieldC K N) :=
  Finsupp.liftAddHom fun v =>
    (Finsupp.singleAddHom (verOnPlacesGeomLevel K N data hKr v)).comp
      (AddMonoidHom.mulRight (ℓ : ℤ))

include data hKr in

def heckeFibreGeomLevel :
    Divisor K (modularFunctionFieldC K N) →+ Divisor K (modularFunctionFieldC K N) :=
  frobeniusPushforwardGeomLevel K N data hKr + frobeniusPullbackGeomLevel K N data hKr

@[simp]
theorem frobeniusPushforwardGeomLevel_single (w : Place K (modularFunctionFieldC K N))
    (n : ℤ) :
    frobeniusPushforwardGeomLevel K N data hKr (Finsupp.single w n)
      = Finsupp.single (frobOnPlacesGeomLevel K N data hKr w) n := by
  simp [frobeniusPushforwardGeomLevel, Finsupp.mapDomain.addMonoidHom_apply,
    Finsupp.mapDomain_single]

@[simp]
theorem frobeniusPullbackGeomLevel_single (w : Place K (modularFunctionFieldC K N))
    (n : ℤ) :
    frobeniusPullbackGeomLevel K N data hKr (Finsupp.single w n)
      = Finsupp.single (verOnPlacesGeomLevel K N data hKr w) (n * ℓ) := by
  simp [frobeniusPullbackGeomLevel]

theorem frobeniusPullbackGeomLevel_frobeniusPushforwardGeomLevel
    (D : Divisor K (modularFunctionFieldC K N)) :
    frobeniusPullbackGeomLevel K N data hKr
        (frobeniusPushforwardGeomLevel K N data hKr D) = (ℓ : ℤ) • D := by
  induction D using Finsupp.induction with
  | zero => simp
  | single_add v n D _ _ ih =>
    rw [map_add, map_add, ih, frobeniusPushforwardGeomLevel_single,
      frobeniusPullbackGeomLevel_single, verOnPlacesGeomLevel_frobOnPlacesGeomLevel,
      smul_add, Finsupp.smul_single, smul_eq_mul, mul_comm]

theorem eichlerShimura_special_fibre_geom_level
    (D : Divisor K (modularFunctionFieldC K N)) :
    frobeniusPushforwardGeomLevel K N data hKr
        (frobeniusPushforwardGeomLevel K N data hKr D)
      - heckeFibreGeomLevel K N data hKr (frobeniusPushforwardGeomLevel K N data hKr D)
      + (ℓ : ℤ) • D = 0 := by
  rw [heckeFibreGeomLevel, AddMonoidHom.add_apply,
    frobeniusPullbackGeomLevel_frobeniusPushforwardGeomLevel]
  abel

end DivisorLevel

section Ramification

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

theorem exists_ramification_frobenius (w : Place K (modularFunctionFieldC K N)) :
    ∃ e : ℕ, 0 < e ∧ (e : ℤ) ∣ (ℓ : ℤ) ∧
      ∀ g : modularFunctionFieldC K N,
        w.ord (frobeniusGeomLevel K N data hKr g)
          = e * (frobOnPlacesGeomLevel K N data hKr w).ord g := by
  letI := frobImageAlgebra K N data hKr
  letI := frobImageTower K N data hKr
  letI := frobImageIsIntegral K N data hKr
  refine ⟨Place.ramificationIndex (F := frobeniusGeomLevelImage K N (ℓ := ℓ)) w,
    Place.ramificationIndex_pos w, ?_, fun g => ?_⟩
  ·

    obtain ⟨π, hπ⟩ := IsDiscreteValuationRing.exists_irreducible w.toValuationSubring
    have hπ0 : (π : modularFunctionFieldC K N) ≠ 0 := by
      simpa [ne_eq, ZeroMemClass.coe_eq_zero] using hπ.ne_zero
    obtain ⟨y, hy⟩ := exists_frobeniusGeomLevel_eq_pow K N data hKr
      (π : modularFunctionFieldC K N)
    have hy0 : (frobeniusGeomLevelEquiv K N (ℓ := ℓ)) y ≠ 0 := by
      intro h0
      have : y = 0 := by
        have := congrArg (frobeniusGeomLevelEquiv K N (ℓ := ℓ)).symm h0
        rwa [AlgEquiv.symm_apply_apply, map_zero] at this
      rw [this, map_zero] at hy
      exact pow_ne_zero ℓ hπ0 hy.symm
    have hdvd := Place.ramificationIndex_dvd_ord
      (F := frobeniusGeomLevelImage K N (ℓ := ℓ)) (w := w) hy0
    rw [show (algebraMap (frobeniusGeomLevelImage K N (ℓ := ℓ))
        (modularFunctionFieldC K N)) ((frobeniusGeomLevelEquiv K N (ℓ := ℓ)) y)
        = frobeniusGeomLevel K N data hKr y from rfl, hy, ← zpow_natCast,
      Place.ord_zpow, Place.ord_coe_irreducible w hπ, mul_one] at hdvd
    exact hdvd
  ·

    rw [show frobeniusGeomLevel K N data hKr g
        = algebraMap (frobeniusGeomLevelImage K N (ℓ := ℓ)) (modularFunctionFieldC K N)
            ((frobeniusGeomLevelEquiv K N (ℓ := ℓ)).toRingEquiv g) from rfl,
      Place.ord_restrict]
    congr 1
    have h2 := Place.ord_congrRingEquiv
      (frobeniusGeomLevelEquiv K N (ℓ := ℓ)).toRingEquiv
      (fun a => (frobeniusGeomLevelEquiv K N (ℓ := ℓ)).commutes a)
      (frobOnPlacesGeomLevel K N data hKr w) g
    rw [show Place.congrRingEquiv (frobeniusGeomLevelEquiv K N (ℓ := ℓ)).toRingEquiv
        (fun a => (frobeniusGeomLevelEquiv K N (ℓ := ℓ)).commutes a)
        (frobOnPlacesGeomLevel K N data hKr w)
        = w.restrict (frobeniusGeomLevelImage K N (ℓ := ℓ)) from
      Equiv.apply_symm_apply (Place.congrEquiv _ _) _] at h2
    exact h2

end Ramification

end ModularCurve

namespace AlgebraicCurve
namespace Place

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

theorem ord_nonneg_of_mem {f : F} (hf : f ∈ v.toValuationSubring) : 0 ≤ v.ord f := by
  rcases eq_or_ne f 0 with rfl | hf0
  · simp
  obtain ⟨π, hπ⟩ := IsDiscreteValuationRing.exists_irreducible v.toValuationSubring
  obtain ⟨n, u, hu⟩ :=
    IsDiscreteValuationRing.eq_unit_mul_pow_irreducible
      (x := (⟨f, hf⟩ : v.toValuationSubring)) (by simpa [Subtype.ext_iff] using hf0) hπ
  have hcoe : f = ((u : v.toValuationSubring) : F) * ((π : F) ^ (n : ℤ)) := by
    have h := congrArg (Subtype.val) hu
    push_cast at h
    rw [zpow_natCast]
    exact h
  rw [hcoe, v.ord_unit_smul_zpow u hπ (n : ℤ)]
  exact Int.natCast_nonneg n

theorem mem_of_ord_nonneg {f : F} (hf : f ≠ 0) (h : 0 ≤ v.ord f) :
    f ∈ v.toValuationSubring := by
  obtain ⟨π, hπ⟩ := IsDiscreteValuationRing.exists_irreducible v.toValuationSubring
  obtain ⟨u, hu⟩ := v.exists_unit_mul_zpow hf hπ
  rw [hu, show v.ord f = (((v.ord f).toNat : ℕ) : ℤ) from (Int.toNat_of_nonneg h).symm,
    zpow_natCast]
  exact mul_mem (u : v.toValuationSubring).2 (pow_mem (π : v.toValuationSubring).2 _)

theorem mem_iff_ord_nonneg {f : F} (hf : f ≠ 0) :
    f ∈ v.toValuationSubring ↔ 0 ≤ v.ord f :=
  ⟨v.ord_nonneg_of_mem, v.mem_of_ord_nonneg hf⟩

theorem exists_ord_pos : ∃ f : F, f ≠ 0 ∧ 0 < v.ord f := by
  obtain ⟨π, hπ⟩ := IsDiscreteValuationRing.exists_irreducible v.toValuationSubring
  refine ⟨(π : F), ?_, ?_⟩
  · simpa [ne_eq, ZeroMemClass.coe_eq_zero] using hπ.ne_zero
  · rw [v.ord_coe_irreducible hπ]
    exact one_pos

end SinglePlace

section RestrictPriv
variable {K F F' : Type*} [Field K] [Field F] [Field F']
  [Algebra K F'] [Algebra F F']

theorem algebraMap_ne_zero {f : F} (hf : f ≠ 0) : algebraMap F F' f ≠ 0 := by
  simpa using hf

variable (w : Place K F')

theorem comap_algebraMap_ne_top [Algebra.IsIntegral F F'] :
    w.toValuationSubring.comap (algebraMap F F') ≠ ⊤ := by
  intro htop
  apply w.ne_top'

  have hF : ∀ f : F, algebraMap F F' f ∈ w.toValuationSubring := fun f =>
    ValuationSubring.mem_comap.mp (htop ▸ ValuationSubring.mem_top f)

  refine SetLike.ext fun x => ⟨fun _ => ValuationSubring.mem_top x, fun _ => ?_⟩
  letI : Algebra F w.toValuationSubring :=
    ((algebraMap F F').codRestrict w.toValuationSubring.toSubring hF).toAlgebra
  letI : IsScalarTower F w.toValuationSubring F' :=
    IsScalarTower.of_algebraMap_eq fun f => rfl
  have hx : IsIntegral w.toValuationSubring x :=
    (Algebra.IsIntegral.isIntegral (R := F) x).tower_top
  obtain ⟨y, hy⟩ := IsIntegrallyClosed.isIntegral_iff.mp hx
  exact hy ▸ y.2

variable {w} in

theorem mem_comap_iff_ord_nonneg {f : F} (hf : f ≠ 0) :
    f ∈ w.toValuationSubring.comap (algebraMap F F') ↔
      0 ≤ w.ord (algebraMap F F' f) := by
  rw [ValuationSubring.mem_comap]
  exact w.mem_iff_ord_nonneg (algebraMap_ne_zero hf)

variable {w} in

theorem isUnit_mk_comap_iff {f : F} (hf : f ≠ 0)
    (hmem : f ∈ w.toValuationSubring.comap (algebraMap F F')) :
    IsUnit (⟨f, hmem⟩ : w.toValuationSubring.comap (algebraMap F F')) ↔
      w.ord (algebraMap F F' f) = 0 := by
  constructor
  · rintro h
    obtain ⟨b, hb⟩ := isUnit_iff_exists_inv.mp h
    have hb' : f * (b : F) = 1 := by
      simpa [Subtype.ext_iff] using hb
    have hbne : (b : F) ≠ 0 := by
      intro h0
      rw [h0, mul_zero] at hb'
      exact zero_ne_one hb'
    have hsum : w.ord (algebraMap F F' f) + w.ord (algebraMap F F' (b : F)) = 0 := by
      rw [← w.ord_mul (algebraMap_ne_zero hf) (algebraMap_ne_zero hbne), ← map_mul, hb',
        map_one, w.ord_one]
    have h1 : 0 ≤ w.ord (algebraMap F F' f) := (mem_comap_iff_ord_nonneg hf).mp hmem
    have h2 : 0 ≤ w.ord (algebraMap F F' (b : F)) := (mem_comap_iff_ord_nonneg hbne).mp b.2
    omega
  · intro h0
    have hinv : f⁻¹ ∈ w.toValuationSubring.comap (algebraMap F F') :=
      (mem_comap_iff_ord_nonneg (inv_ne_zero hf)).mpr (by rw [map_inv₀, w.ord_inv]; omega)
    exact ⟨⟨⟨f, hmem⟩, ⟨f⁻¹, hinv⟩, Subtype.ext (mul_inv_cancel₀ hf),
      Subtype.ext (inv_mul_cancel₀ hf)⟩, rfl⟩

theorem exists_ord_algebraMap_pos [Algebra.IsIntegral F F'] :
    ∃ f : F, f ≠ 0 ∧ 0 < w.ord (algebraMap F F' f) := by
  have h := w.comap_algebraMap_ne_top (F := F)
  rw [ne_eq, SetLike.ext_iff, not_forall] at h
  obtain ⟨g, hg⟩ := h
  simp only [ValuationSubring.mem_top, iff_true] at hg
  have hg0 : g ≠ 0 := by
    rintro rfl
    exact hg (zero_mem _)
  refine ⟨g⁻¹, inv_ne_zero hg0, ?_⟩
  rw [map_inv₀, w.ord_inv]
  have := (mem_comap_iff_ord_nonneg hg0).not.mp hg
  omega

variable [Algebra.IsIntegral F F']

theorem ramificationIndex_set_nonempty :
    {n : ℕ | 0 < n ∧ ∃ f : F, f ≠ 0 ∧ w.ord (algebraMap F F' f) = n}.Nonempty := by
  obtain ⟨f, hf0, hf⟩ := w.exists_ord_algebraMap_pos (F := F)
  exact ⟨(w.ord (algebraMap F F' f)).toNat, by omega, f, hf0, by omega⟩

theorem isPrincipalIdealRing_comap :
    IsPrincipalIdealRing (w.toValuationSubring.comap (algebraMap F F')) := by
  obtain ⟨g, hg0, hge⟩ := w.exists_ord_eq_ramificationIndex (F := F)
  have hepos : 0 < ramificationIndex (F := F) w := w.ramificationIndex_pos (F := F)
  have hgmem : g ∈ w.toValuationSubring.comap (algebraMap F F') :=
    (mem_comap_iff_ord_nonneg hg0).mpr (by omega)
  refine (IsDiscreteValuationRing.ofHasUnitMulPowIrreducibleFactorization
    ⟨⟨g, hgmem⟩, irreducible_mk_comap w hg0 hgmem hge, ?_⟩).toIsPrincipalIdealRing
  rintro ⟨f, hmem⟩ hx
  have hf : f ≠ 0 := by simpa [Subtype.ext_iff] using hx

  obtain ⟨c, hc⟩ := w.ramificationIndex_dvd_ord (F := F) hf
  have hnonneg : 0 ≤ w.ord (algebraMap F F' f) := (mem_comap_iff_ord_nonneg hf).mp hmem
  have hcnonneg : 0 ≤ c := by
    by_contra hneg
    have hcle : c ≤ -1 := by omega
    have : (ramificationIndex (F := F) w : ℤ) * c ≤ (ramificationIndex (F := F) w : ℤ) * -1 :=
      mul_le_mul_of_nonneg_left hcle (by omega)
    omega
  set n : ℕ := c.toNat with hn
  have hcn : (n : ℤ) = c := Int.toNat_of_nonneg hcnonneg
  refine ⟨n, ?_⟩

  have hgn : g ^ n ≠ 0 := pow_ne_zero _ hg0
  have hdiv0 : f / g ^ n ≠ 0 := div_ne_zero hf hgn
  have hu0 : w.ord (algebraMap F F' (f / g ^ n)) = 0 := by
    have hkey : algebraMap F F' (f / g ^ n)
        = algebraMap F F' f * (algebraMap F F' g) ^ (-(n : ℤ)) := by
      rw [div_eq_mul_inv, map_mul, map_inv₀, map_pow, ← zpow_natCast (algebraMap F F' g) n,
        ← zpow_neg]
    rw [hkey, w.ord_mul (algebraMap_ne_zero hf) (zpow_ne_zero _ (algebraMap_ne_zero hg0)),
      w.ord_zpow, hge, hc, ← hcn]
    ring
  have humem : f / g ^ n ∈ w.toValuationSubring.comap (algebraMap F F') :=
    (mem_comap_iff_ord_nonneg hdiv0).mpr (le_of_eq hu0.symm)
  have hu : IsUnit (⟨f / g ^ n, humem⟩ : w.toValuationSubring.comap (algebraMap F F')) :=
    (isUnit_mk_comap_iff hdiv0 humem).mpr hu0
  refine ⟨hu.unit, ?_⟩
  refine Subtype.ext ?_
  have hcoe : ((hu.unit : w.toValuationSubring.comap (algebraMap F F')) : F) = f / g ^ n := by
    rw [IsUnit.unit_spec]
  push_cast
  rw [hcoe, mul_comm, div_mul_cancel₀]
  exact hgn

end RestrictPriv

end Place
end AlgebraicCurve

noncomputable section

open AlgebraicCurve Polynomial

set_option synthInstance.maxHeartbeats 400000
set_option maxHeartbeats 800000

namespace ModularCurve

section Package

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

include data hKr in

theorem exists_pow_eq_frobeniusGeomLevel (hperf : ∀ c : K, ∃ d : K, d ^ ℓ = c)
    (y : modularFunctionFieldC K N) :
    ∃ x : modularFunctionFieldC K N, frobeniusGeomLevel K N data hKr y = x ^ ℓ := by
  haveI : CharP (LaurentSeries K) ℓ := charP_laurentSeries K

  have key : ∀ z : LaurentSeries K, z ∈ modularFunctionFieldC K N →
      ∃ w : LaurentSeries K, w ∈ modularFunctionFieldC K N ∧ qExpand K ℓ z = w ^ ℓ := by
    intro z hz
    induction hz using IntermediateField.adjoin_induction with
    | mem y hy =>
      rcases hy with rfl | rfl
      · exact ⟨jqModC K, jqModC_mem K N, qExpand_jqModC_eq_pow K data hKr⟩
      · exact ⟨jqNModC K N, jqNModC_mem K N, qExpand_jqNModC_eq_pow K N data hKr⟩
    | algebraMap c =>
      obtain ⟨d, hd⟩ := hperf c
      refine ⟨algebraMap K (LaurentSeries K) d,
        (modularFunctionFieldC K N).algebraMap_mem d, ?_⟩
      rw [show qExpand K ℓ (algebraMap K (LaurentSeries K) c)
            = qExpandAlgC K ℓ (algebraMap K (LaurentSeries K) c) from rfl,
        (qExpandAlgC K ℓ).commutes c, ← map_pow, hd]
    | add y z _ _ hy hz =>
      obtain ⟨w₁, hw₁, he₁⟩ := hy
      obtain ⟨w₂, hw₂, he₂⟩ := hz
      refine ⟨w₁ + w₂, add_mem hw₁ hw₂, ?_⟩
      rw [show qExpand K ℓ (y + z) = qExpandAlgC K ℓ (y + z) from rfl, map_add,
        qExpandAlgC_apply, qExpandAlgC_apply, he₁, he₂, add_pow_char]
    | inv y _ hy =>
      obtain ⟨w, hw, he⟩ := hy
      refine ⟨w⁻¹, inv_mem hw, ?_⟩
      rw [show qExpand K ℓ y⁻¹ = qExpandAlgC K ℓ y⁻¹ from rfl, map_inv₀,
        qExpandAlgC_apply, he, inv_pow]
    | mul y z _ _ hy hz =>
      obtain ⟨w₁, hw₁, he₁⟩ := hy
      obtain ⟨w₂, hw₂, he₂⟩ := hz
      refine ⟨w₁ * w₂, mul_mem hw₁ hw₂, ?_⟩
      rw [show qExpand K ℓ (y * z) = qExpandAlgC K ℓ (y * z) from rfl, map_mul,
        qExpandAlgC_apply, qExpandAlgC_apply, he₁, he₂, mul_pow]
  obtain ⟨w, hw, he⟩ := key (y : LaurentSeries K) y.2
  refine ⟨⟨w, hw⟩, Subtype.ext ?_⟩
  rw [frobeniusGeomLevel_apply_coe]
  push_cast
  exact he

include data hKr in

theorem isFrobeniusEndo_frobeniusGeomLevel (hperf : ∀ c : K, ∃ d : K, d ^ ℓ = c) :
    IsFrobeniusEndo ℓ (frobeniusGeomLevel K N data hKr) :=
  ⟨exists_frobeniusGeomLevel_eq_pow K N data hKr,
    exists_pow_eq_frobeniusGeomLevel K N data hKr hperf⟩

include data hKr in

theorem frobeniusGeomLevel_isIntegral (hperf : ∀ c : K, ∃ d : K, d ^ ℓ = c) :
    (frobeniusGeomLevel K N data hKr).toRingHom.IsIntegral :=
  (isFrobeniusEndo_frobeniusGeomLevel K N data hKr hperf).isIntegral
    (Fact.out : ℓ.Prime).pos.ne'

theorem frobeniusGeomLevel_eq_pow_unique {g g' f : modularFunctionFieldC K N}
    (hg : frobeniusGeomLevel K N data hKr g = f ^ ℓ)
    (hg' : frobeniusGeomLevel K N data hKr g' = f ^ ℓ) : g = g' :=
  frobeniusGeomLevel_injective K N data hKr (hg.trans hg'.symm)

end Package

section Identification

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

theorem mem_restrictAlong_iff {F : Type*} [Field F] [Algebra K F] (φ : F →ₐ[K] F)
    (hφ : φ.toRingHom.IsIntegral) (w : Place K F) (x : F) :
    x ∈ (w.restrictAlong φ hφ).toValuationSubring ↔ φ x ∈ w.toValuationSubring := by
  rw [show (w.restrictAlong φ hφ).toValuationSubring
      = w.toValuationSubring.comap φ.toRingHom from rfl, ValuationSubring.mem_comap]
  exact Iff.rfl

include data hKr in

theorem restrictAlong_frobeniusGeomLevel_eq (hperf : ∀ c : K, ∃ d : K, d ^ ℓ = c)
    (w : Place K (modularFunctionFieldC K N)) :
    w.restrictAlong (frobeniusGeomLevel K N data hKr)
        (frobeniusGeomLevel_isIntegral K N data hKr hperf)
      = frobOnPlacesGeomLevel K N data hKr w := by
  refine Place.ext (SetLike.ext fun x => ?_)
  rw [mem_restrictAlong_iff, mem_frobOnPlacesGeomLevel_iff]

end Identification

section Ramification

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

include data hKr in

theorem ramificationIndexAlong_frobeniusGeomLevel (hperf : ∀ c : K, ∃ d : K, d ^ ℓ = c)
    (w : Place K (modularFunctionFieldC K N)) :
    Place.ramificationIndexAlong (frobeniusGeomLevel K N data hKr) w = ℓ :=
  (isFrobeniusEndo_frobeniusGeomLevel K N data hKr hperf).ramificationIndexAlong_eq
    (Fact.out : ℓ.Prime).pos.ne' w

include data hKr in

theorem ord_frobeniusGeomLevel_eq_mul (hperf : ∀ c : K, ∃ d : K, d ^ ℓ = c)
    (w : Place K (modularFunctionFieldC K N)) (g : modularFunctionFieldC K N) :
    w.ord (frobeniusGeomLevel K N data hKr g)
      = ℓ * (frobOnPlacesGeomLevel K N data hKr w).ord g := by
  have h := w.ord_restrictAlong (frobeniusGeomLevel K N data hKr)
    (frobeniusGeomLevel_isIntegral K N data hKr hperf) g
  rwa [ramificationIndexAlong_frobeniusGeomLevel K N data hKr hperf,
    restrictAlong_frobeniusGeomLevel_eq K N data hKr hperf] at h

include data hKr in

theorem ord_frobOnPlaces_of_pow_eq (hperf : ∀ c : K, ∃ d : K, d ^ ℓ = c)
    {f g : modularFunctionFieldC K N}
    (hg : frobeniusGeomLevel K N data hKr g = f ^ ℓ)
    (w : Place K (modularFunctionFieldC K N)) :
    (frobOnPlacesGeomLevel K N data hKr w).ord g = w.ord f := by
  have hkey : (ℓ : ℤ) * (frobOnPlacesGeomLevel K N data hKr w).ord g
      = (ℓ : ℤ) * w.ord f := by
    rw [← ord_frobeniusGeomLevel_eq_mul K N data hKr hperf w g, hg, ← zpow_natCast,
      Place.ord_zpow]
  exact mul_left_cancel₀ (Int.natCast_ne_zero.mpr (Fact.out : ℓ.Prime).pos.ne') hkey

end Ramification

section NormFormula

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

include data hKr in

theorem frobeniusPushforwardGeomLevel_apply_frob
    (D : Divisor K (modularFunctionFieldC K N))
    (w : Place K (modularFunctionFieldC K N)) :
    frobeniusPushforwardGeomLevel K N data hKr D (frobOnPlacesGeomLevel K N data hKr w)
      = D w := by
  rw [show frobeniusPushforwardGeomLevel K N data hKr D
      = Finsupp.mapDomain (frobOnPlacesGeomLevel K N data hKr) D from rfl]
  exact Finsupp.mapDomain_apply (frobOnPlacesGeomLevel_injective K N data hKr) D w

include data hKr in

theorem frobeniusPushforwardGeomLevel_apply_of_notMem_range
    (D : Divisor K (modularFunctionFieldC K N))
    {v : Place K (modularFunctionFieldC K N)}
    (hv : v ∉ Set.range (frobOnPlacesGeomLevel K N data hKr)) :
    frobeniusPushforwardGeomLevel K N data hKr D v = 0 := by
  rw [show frobeniusPushforwardGeomLevel K N data hKr D
      = Finsupp.mapDomain (frobOnPlacesGeomLevel K N data hKr) D from rfl]
  exact Finsupp.mapDomain_notin_range D v hv

include data hKr in

theorem frobeniusPushforwardGeomLevel_normFormula_apply_frob
    (hperf : ∀ c : K, ∃ d : K, d ^ ℓ = c)
    {f g : modularFunctionFieldC K N}
    (hg : frobeniusGeomLevel K N data hKr g = f ^ ℓ)
    {D : Divisor K (modularFunctionFieldC K N)}
    (hD : ∀ w, D w = w.ord f) (w : Place K (modularFunctionFieldC K N)) :
    frobeniusPushforwardGeomLevel K N data hKr D (frobOnPlacesGeomLevel K N data hKr w)
      = (frobOnPlacesGeomLevel K N data hKr w).ord g := by
  rw [frobeniusPushforwardGeomLevel_apply_frob K N data hKr D w, hD w,
    ord_frobOnPlaces_of_pow_eq K N data hKr hperf hg w]

include data hKr in

theorem frobeniusPushforwardGeomLevel_normFormula
    (hperf : ∀ c : K, ∃ d : K, d ^ ℓ = c)
    (hsurj : Function.Surjective (frobOnPlacesGeomLevel K N data hKr))
    {f g : modularFunctionFieldC K N}
    (hg : frobeniusGeomLevel K N data hKr g = f ^ ℓ)
    {D : Divisor K (modularFunctionFieldC K N)}
    (hD : ∀ w, D w = w.ord f) (v : Place K (modularFunctionFieldC K N)) :
    frobeniusPushforwardGeomLevel K N data hKr D v = v.ord g := by
  obtain ⟨w, rfl⟩ := hsurj v
  exact frobeniusPushforwardGeomLevel_normFormula_apply_frob
    K N data hKr hperf hg hD w

include data hKr in

theorem isPrincipal_frobeniusPushforwardGeomLevel
    (hperf : ∀ c : K, ∃ d : K, d ^ ℓ = c)
    (hsurj : Function.Surjective (frobOnPlacesGeomLevel K N data hKr))
    {D : Divisor K (modularFunctionFieldC K N)} (hD : D.IsPrincipal) :
    (frobeniusPushforwardGeomLevel K N data hKr D).IsPrincipal := by
  obtain ⟨f, hf, hDf⟩ := hD
  obtain ⟨g, hg⟩ := exists_frobeniusGeomLevel_eq_pow K N data hKr f
  refine ⟨g, ?_, fun v => frobeniusPushforwardGeomLevel_normFormula
    K N data hKr hperf hsurj hg hDf v⟩
  intro hg0
  rw [hg0, map_zero] at hg
  exact pow_ne_zero ℓ hf hg.symm

end NormFormula

end ModularCurve

noncomputable section

namespace AlgebraicCurve

section FrobNormHom

variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} {φ : F →ₐ[K] F}

namespace IsFrobeniusEndo

theorem frobNorm_eq_of_map_eq_pow (h : IsFrobeniusEndo ℓ φ) {f g : F}
    (hg : φ g = f ^ ℓ) : h.frobNorm f = g :=
  φ.toRingHom.injective ((h.map_frobNorm f).trans hg.symm)

theorem frobNorm_map (h : IsFrobeniusEndo ℓ φ) (x : F) : h.frobNorm (φ x) = x ^ ℓ :=
  h.frobNorm_eq_of_map_eq_pow (by rw [map_pow])

theorem frobNorm_one (h : IsFrobeniusEndo ℓ φ) : h.frobNorm 1 = 1 :=
  h.frobNorm_eq_of_map_eq_pow (by rw [map_one, one_pow])

theorem frobNorm_mul (h : IsFrobeniusEndo ℓ φ) (a b : F) :
    h.frobNorm (a * b) = h.frobNorm a * h.frobNorm b :=
  h.frobNorm_eq_of_map_eq_pow (by rw [map_mul, h.map_frobNorm, h.map_frobNorm, mul_pow])

theorem frobNorm_algebraMap (h : IsFrobeniusEndo ℓ φ) (c : K) :
    h.frobNorm (algebraMap K F c) = algebraMap K F c ^ ℓ :=
  h.frobNorm_eq_of_map_eq_pow (by rw [map_pow, φ.commutes])

variable [Fact ℓ.Prime] [CharP F ℓ]

omit [CharP F ℓ] in

theorem frobNorm_zero (h : IsFrobeniusEndo ℓ φ) : h.frobNorm 0 = 0 :=
  h.frobNorm_eq_of_map_eq_pow
    (by rw [map_zero, zero_pow (Fact.out : ℓ.Prime).pos.ne'])

theorem frobNorm_add (h : IsFrobeniusEndo ℓ φ) (a b : F) :
    h.frobNorm (a + b) = h.frobNorm a + h.frobNorm b :=
  h.frobNorm_eq_of_map_eq_pow
    (by rw [map_add, h.map_frobNorm, h.map_frobNorm, add_pow_char])

def frobNormRingHom (h : IsFrobeniusEndo ℓ φ) : F →+* F where
  toFun := h.frobNorm
  map_one' := h.frobNorm_one
  map_mul' := h.frobNorm_mul
  map_zero' := h.frobNorm_zero
  map_add' := h.frobNorm_add

@[simp]
theorem frobNormRingHom_apply (h : IsFrobeniusEndo ℓ φ) (f : F) :
    h.frobNormRingHom f = h.frobNorm f := rfl

theorem frobNormRingHom_isIntegral (h : IsFrobeniusEndo ℓ φ) :
    h.frobNormRingHom.IsIntegral := by
  intro x
  refine ⟨Polynomial.X ^ ℓ - Polynomial.C (φ x),
    Polynomial.monic_X_pow_sub_C _ (Fact.out : ℓ.Prime).pos.ne', ?_⟩
  simp [Polynomial.eval₂_sub, frobNormRingHom_apply, h.frobNorm_map x]

end IsFrobeniusEndo

end FrobNormHom

section ExtendPlace

variable {K F : Type*} [Field K] [Field F] [Algebra K F]
variable {ℓ : ℕ} [Fact ℓ.Prime] [CharP F ℓ] {φ : F →ₐ[K] F}

namespace IsFrobeniusEndo

variable (h : IsFrobeniusEndo ℓ φ)

def extendPlace (v : Place K F) : Place K F where
  toValuationSubring := v.toValuationSubring.comap h.frobNormRingHom
  algebraMap_mem' a := by
    rw [ValuationSubring.mem_comap, frobNormRingHom_apply, h.frobNorm_algebraMap]
    exact pow_mem (v.algebraMap_mem' a) ℓ
  ne_top' := by

    intro htop
    apply v.ne_top'
    refine SetLike.ext fun z => ⟨fun _ => ValuationSubring.mem_top z, fun _ => ?_⟩
    have hz : φ z ∈ v.toValuationSubring.comap h.frobNormRingHom :=
      htop ▸ ValuationSubring.mem_top (φ z)
    rw [ValuationSubring.mem_comap, frobNormRingHom_apply, h.frobNorm_map] at hz
    exact (v.toValuationSubring.pow_mem_iff (Fact.out : ℓ.Prime).pos.ne' z).mp hz
  isPrincipalIdealRing' := by

    letI : Algebra F F := h.frobNormRingHom.toAlgebra
    haveI : Algebra.IsIntegral F F := ⟨h.frobNormRingHom_isIntegral⟩
    exact v.isPrincipalIdealRing_comap (F := F)

theorem mem_extendPlace_iff (v : Place K F) (y : F) :
    y ∈ (h.extendPlace v).toValuationSubring ↔ h.frobNorm y ∈ v.toValuationSubring :=
  ValuationSubring.mem_comap

theorem restrictAlong_extendPlace (hφ : φ.toRingHom.IsIntegral) (v : Place K F) :
    (h.extendPlace v).restrictAlong φ hφ = v := by
  refine Place.ext (SetLike.ext fun x => ?_)
  rw [ModularCurve.mem_restrictAlong_iff (K := K) φ hφ (h.extendPlace v) x,
    h.mem_extendPlace_iff, h.frobNorm_map]
  exact v.toValuationSubring.pow_mem_iff (Fact.out : ℓ.Prime).pos.ne' x

include h in

theorem restrictAlong_surjective (hφ : φ.toRingHom.IsIntegral) :
    Function.Surjective (Place.restrictAlong φ hφ) := fun v =>
  ⟨h.extendPlace v, h.restrictAlong_extendPlace hφ v⟩

theorem extendPlace_restrictAlong (hℓ : ℓ ≠ 0) (hφ : φ.toRingHom.IsIntegral)
    (w : Place K F) :
    h.extendPlace (w.restrictAlong φ hφ) = w :=
  h.restrictAlong_injective hℓ hφ
    (h.restrictAlong_extendPlace hφ (w.restrictAlong φ hφ))

end IsFrobeniusEndo

end ExtendPlace

end AlgebraicCurve

namespace ModularCurve

open AlgebraicCurve

section LevelN

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

omit [Fact ℓ.Prime] in

theorem charP_modularFunctionFieldC : CharP (modularFunctionFieldC K N) ℓ :=
  charP_of_injective_algebraMap
    (algebraMap K (modularFunctionFieldC K N)).injective ℓ

include data hKr in

def extendPlaceGeomLevel (hperf : ∀ c : K, ∃ d : K, d ^ ℓ = c)
    (v : Place K (modularFunctionFieldC K N)) : Place K (modularFunctionFieldC K N) :=
  haveI : CharP (modularFunctionFieldC K N) ℓ := charP_modularFunctionFieldC K N
  (isFrobeniusEndo_frobeniusGeomLevel K N data hKr hperf).extendPlace v

include data hKr in

theorem frobOnPlacesGeomLevel_extendPlaceGeomLevel (hperf : ∀ c : K, ∃ d : K, d ^ ℓ = c)
    (v : Place K (modularFunctionFieldC K N)) :
    frobOnPlacesGeomLevel K N data hKr (extendPlaceGeomLevel K N data hKr hperf v) = v := by
  haveI : CharP (modularFunctionFieldC K N) ℓ := charP_modularFunctionFieldC K N
  rw [extendPlaceGeomLevel, ← restrictAlong_frobeniusGeomLevel_eq K N data hKr hperf]
  exact (isFrobeniusEndo_frobeniusGeomLevel K N data hKr hperf).restrictAlong_extendPlace
    (frobeniusGeomLevel_isIntegral K N data hKr hperf) v

include data hKr in

theorem frobOnPlacesGeomLevel_surjective (hperf : ∀ c : K, ∃ d : K, d ^ ℓ = c) :
    Function.Surjective (frobOnPlacesGeomLevel K N data hKr) := fun v =>
  ⟨extendPlaceGeomLevel K N data hKr hperf v,
    frobOnPlacesGeomLevel_extendPlaceGeomLevel K N data hKr hperf v⟩

include data hKr in

theorem frobOnPlacesGeomLevel_bijective (hperf : ∀ c : K, ∃ d : K, d ^ ℓ = c) :
    Function.Bijective (frobOnPlacesGeomLevel K N data hKr) :=
  ⟨frobOnPlacesGeomLevel_injective K N data hKr,
    frobOnPlacesGeomLevel_surjective K N data hKr hperf⟩

include data hKr in

theorem verOnPlacesGeomLevel_eq_extendPlaceGeomLevel (hperf : ∀ c : K, ∃ d : K, d ^ ℓ = c)
    (u : Place K (modularFunctionFieldC K N)) :
    verOnPlacesGeomLevel K N data hKr u = extendPlaceGeomLevel K N data hKr hperf u := by
  haveI : CharP (modularFunctionFieldC K N) ℓ := charP_modularFunctionFieldC K N
  obtain ⟨w, rfl⟩ := frobOnPlacesGeomLevel_surjective K N data hKr hperf u
  rw [verOnPlacesGeomLevel_frobOnPlacesGeomLevel K N data hKr w, extendPlaceGeomLevel,
    ← restrictAlong_frobeniusGeomLevel_eq K N data hKr hperf]
  exact ((isFrobeniusEndo_frobeniusGeomLevel K N data hKr
    hperf).extendPlace_restrictAlong (Fact.out : ℓ.Prime).pos.ne'
    (frobeniusGeomLevel_isIntegral K N data hKr hperf) w).symm

end LevelN

section Consumers

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

include data hKr in

theorem frobeniusPushforwardGeomLevel_normFormula'
    (hperf : ∀ c : K, ∃ d : K, d ^ ℓ = c)
    {f g : modularFunctionFieldC K N}
    (hg : frobeniusGeomLevel K N data hKr g = f ^ ℓ)
    {D : Divisor K (modularFunctionFieldC K N)}
    (hD : ∀ w, D w = w.ord f) (v : Place K (modularFunctionFieldC K N)) :
    frobeniusPushforwardGeomLevel K N data hKr D v = v.ord g :=
  frobeniusPushforwardGeomLevel_normFormula K N data hKr hperf
    (frobOnPlacesGeomLevel_surjective K N data hKr hperf) hg hD v

include data hKr in

theorem isPrincipal_frobeniusPushforwardGeomLevel'
    (hperf : ∀ c : K, ∃ d : K, d ^ ℓ = c)
    {D : Divisor K (modularFunctionFieldC K N)} (hD : D.IsPrincipal) :
    (frobeniusPushforwardGeomLevel K N data hKr D).IsPrincipal :=
  isPrincipal_frobeniusPushforwardGeomLevel K N data hKr hperf
    (frobOnPlacesGeomLevel_surjective K N data hKr hperf) hD

end Consumers

end ModularCurve

noncomputable section

open AlgebraicCurve Polynomial

set_option synthInstance.maxHeartbeats 400000
set_option maxHeartbeats 800000

namespace ModularCurve

section PlaceLevel

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

include data hKr in

theorem frobOnPlacesGeomLevel_verOnPlacesGeomLevel
    (hsurj : Function.Surjective (frobOnPlacesGeomLevel K N data hKr))
    (v : Place K (modularFunctionFieldC K N)) :
    frobOnPlacesGeomLevel K N data hKr (verOnPlacesGeomLevel K N data hKr v) = v := by
  obtain ⟨u, rfl⟩ := hsurj v
  rw [verOnPlacesGeomLevel_frobOnPlacesGeomLevel K N data hKr u]

include data hKr in

theorem verOnPlacesGeomLevel_eq_iff
    (hsurj : Function.Surjective (frobOnPlacesGeomLevel K N data hKr))
    {v w : Place K (modularFunctionFieldC K N)} :
    verOnPlacesGeomLevel K N data hKr v = w ↔ v = frobOnPlacesGeomLevel K N data hKr w := by
  constructor
  · rintro rfl
    rw [frobOnPlacesGeomLevel_verOnPlacesGeomLevel K N data hKr hsurj v]
  · rintro rfl
    rw [verOnPlacesGeomLevel_frobOnPlacesGeomLevel K N data hKr w]

end PlaceLevel

section Evaluation

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

include data hKr in

theorem frobeniusPullbackGeomLevel_apply
    (hsurj : Function.Surjective (frobOnPlacesGeomLevel K N data hKr))
    (D : Divisor K (modularFunctionFieldC K N))
    (w : Place K (modularFunctionFieldC K N)) :
    frobeniusPullbackGeomLevel K N data hKr D w
      = D (frobOnPlacesGeomLevel K N data hKr w) * ℓ := by
  induction D using Finsupp.induction with
  | zero => simp
  | single_add v n D _ _ ih =>
    rw [map_add, Finsupp.add_apply, ih, frobeniusPullbackGeomLevel_single,
      Finsupp.add_apply, add_mul]
    congr 1
    by_cases hvw : v = frobOnPlacesGeomLevel K N data hKr w
    · subst hvw
      rw [verOnPlacesGeomLevel_frobOnPlacesGeomLevel K N data hKr w,
        Finsupp.single_eq_same, Finsupp.single_eq_same]
    · have hne : verOnPlacesGeomLevel K N data hKr v ≠ w :=
        fun h => hvw ((verOnPlacesGeomLevel_eq_iff K N data hKr hsurj).mp h)
      rw [Finsupp.single_eq_of_ne' hne, Finsupp.single_eq_of_ne' hvw, zero_mul]

end Evaluation

section Principal

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

include data hKr in

theorem frobeniusPullbackGeomLevel_pullbackFormula
    (hperf : ∀ c : K, ∃ d : K, d ^ ℓ = c)
    (hsurj : Function.Surjective (frobOnPlacesGeomLevel K N data hKr))
    {f : modularFunctionFieldC K N}
    {D : Divisor K (modularFunctionFieldC K N)}
    (hD : ∀ w, D w = w.ord f) (w : Place K (modularFunctionFieldC K N)) :
    frobeniusPullbackGeomLevel K N data hKr D w
      = w.ord (frobeniusGeomLevel K N data hKr f) := by
  rw [frobeniusPullbackGeomLevel_apply K N data hKr hsurj D w,
    hD (frobOnPlacesGeomLevel K N data hKr w),
    ord_frobeniusGeomLevel_eq_mul K N data hKr hperf w f, mul_comm]

include data hKr in

theorem isPrincipal_frobeniusPullbackGeomLevel'
    (hperf : ∀ c : K, ∃ d : K, d ^ ℓ = c)
    (hsurj : Function.Surjective (frobOnPlacesGeomLevel K N data hKr))
    {D : Divisor K (modularFunctionFieldC K N)} (hD : D.IsPrincipal) :
    (frobeniusPullbackGeomLevel K N data hKr D).IsPrincipal := by
  obtain ⟨f, hf, hDf⟩ := hD
  refine ⟨frobeniusGeomLevel K N data hKr f, ?_,
    fun w => frobeniusPullbackGeomLevel_pullbackFormula K N data hKr hperf hsurj hDf w⟩
  intro h0
  exact hf (frobeniusGeomLevel_injective K N data hKr (h0.trans (map_zero _).symm))

include data hKr in

theorem isPrincipal_heckeFibreGeomLevel'
    (hperf : ∀ c : K, ∃ d : K, d ^ ℓ = c)
    (hsurj : Function.Surjective (frobOnPlacesGeomLevel K N data hKr))
    {D : Divisor K (modularFunctionFieldC K N)} (hD : D.IsPrincipal) :
    (heckeFibreGeomLevel K N data hKr D).IsPrincipal := by
  have hpush := isPrincipal_frobeniusPushforwardGeomLevel' K N data hKr hperf hD
  have hpull := isPrincipal_frobeniusPullbackGeomLevel' K N data hKr hperf hsurj hD
  obtain ⟨g, hg, hDg⟩ := hpush
  obtain ⟨h, hh, hDh⟩ := hpull
  refine ⟨g * h, mul_ne_zero hg hh, fun v => ?_⟩
  have key : heckeFibreGeomLevel K N data hKr D
      = frobeniusPushforwardGeomLevel K N data hKr D
        + frobeniusPullbackGeomLevel K N data hKr D := rfl
  rw [key, Finsupp.add_apply, hDg v, hDh v, v.ord_mul hg hh]

end Principal

end ModularCurve

noncomputable section

open AlgebraicCurve

set_option synthInstance.maxHeartbeats 400000
set_option maxHeartbeats 800000

namespace ModularCurve

section DegreePlace

variable (K : Type*) [Field K] (N : ℕ) [NeZero N]
variable {ℓ : ℕ} [Fact ℓ.Prime] [CharP K ℓ]
variable (data : ModularPolynomialData ℓ) (hKr : KroneckerCongruence ℓ data)
variable (hdeg1 : ∀ w : Place K (modularFunctionFieldC K N), w.deg = 1)

include data hKr hdeg1 in

theorem deg_frobOnPlacesGeomLevel (w : Place K (modularFunctionFieldC K N)) :
    (frobOnPlacesGeomLevel K N data hKr w).deg = w.deg := by
  rw [hdeg1 (frobOnPlacesGeomLevel K N data hKr w), hdeg1 w]

include data hKr hdeg1 in

theorem deg_verOnPlacesGeomLevel (w : Place K (modularFunctionFieldC K N)) :
    (verOnPlacesGeomLevel K N data hKr w).deg = w.deg := by
  rw [hdeg1 (verOnPlacesGeomLevel K N data hKr w), hdeg1 w]

end DegreePlace

section DegreeDivisor

variable (K : Type*) [Field K] (N : ℕ) [NeZero N]
variable {ℓ : ℕ} [Fact ℓ.Prime] [CharP K ℓ]
variable (data : ModularPolynomialData ℓ) (hKr : KroneckerCongruence ℓ data)
variable (hdeg1 : ∀ w : Place K (modularFunctionFieldC K N), w.deg = 1)

include data hKr hdeg1 in

theorem degree_frobeniusPushforwardGeomLevel (D : Divisor K (modularFunctionFieldC K N)) :
    Divisor.degree (frobeniusPushforwardGeomLevel K N data hKr D) = Divisor.degree D := by
  induction D using Finsupp.induction with
  | zero => simp
  | single_add v n D _ _ ih =>
    rw [map_add, map_add, ih, frobeniusPushforwardGeomLevel_single, map_add,
      Divisor.degree_single, Divisor.degree_single,
      deg_frobOnPlacesGeomLevel K N data hKr hdeg1 v]

include data hKr hdeg1 in

theorem degree_frobeniusPullbackGeomLevel (D : Divisor K (modularFunctionFieldC K N)) :
    Divisor.degree (frobeniusPullbackGeomLevel K N data hKr D) = ℓ * Divisor.degree D := by
  induction D using Finsupp.induction with
  | zero => simp
  | single_add v n D _ _ ih =>
    rw [map_add, map_add, ih, frobeniusPullbackGeomLevel_single, map_add,
      Divisor.degree_single, Divisor.degree_single,
      deg_verOnPlacesGeomLevel K N data hKr hdeg1 v, mul_add]
    ring

include data hKr hdeg1 in

theorem degree_heckeFibreGeomLevel (D : Divisor K (modularFunctionFieldC K N)) :
    Divisor.degree (heckeFibreGeomLevel K N data hKr D) = (ℓ + 1) * Divisor.degree D := by
  rw [show heckeFibreGeomLevel K N data hKr D
      = frobeniusPushforwardGeomLevel K N data hKr D
        + frobeniusPullbackGeomLevel K N data hKr D from rfl,
    map_add, degree_frobeniusPushforwardGeomLevel K N data hKr hdeg1 D,
    degree_frobeniusPullbackGeomLevel K N data hKr hdeg1 D]
  ring

include data hKr hdeg1 in

theorem frobeniusPushforwardGeomLevel_mem_degZero {D : Divisor K (modularFunctionFieldC K N)}
    (hD : D ∈ Divisor.degZero (K := K) (F := modularFunctionFieldC K N)) :
    frobeniusPushforwardGeomLevel K N data hKr D ∈
      Divisor.degZero (K := K) (F := modularFunctionFieldC K N) := by
  rw [Divisor.mem_degZero] at hD ⊢
  rw [degree_frobeniusPushforwardGeomLevel K N data hKr hdeg1 D, hD]

include data hKr hdeg1 in

theorem frobeniusPullbackGeomLevel_mem_degZero {D : Divisor K (modularFunctionFieldC K N)}
    (hD : D ∈ Divisor.degZero (K := K) (F := modularFunctionFieldC K N)) :
    frobeniusPullbackGeomLevel K N data hKr D ∈
      Divisor.degZero (K := K) (F := modularFunctionFieldC K N) := by
  rw [Divisor.mem_degZero] at hD ⊢
  rw [degree_frobeniusPullbackGeomLevel K N data hKr hdeg1 D, hD, mul_zero]

include data hKr hdeg1 in

theorem heckeFibreGeomLevel_mem_degZero {D : Divisor K (modularFunctionFieldC K N)}
    (hD : D ∈ Divisor.degZero (K := K) (F := modularFunctionFieldC K N)) :
    heckeFibreGeomLevel K N data hKr D ∈
      Divisor.degZero (K := K) (F := modularFunctionFieldC K N) := by
  rw [Divisor.mem_degZero] at hD ⊢
  rw [degree_heckeFibreGeomLevel K N data hKr hdeg1 D, hD, mul_zero]

include data hKr hdeg1 in

def frobeniusPushforwardGeomLevelDegZero :
    Divisor.degZero (K := K) (F := modularFunctionFieldC K N)
      →+ Divisor.degZero (K := K) (F := modularFunctionFieldC K N) :=
  ((frobeniusPushforwardGeomLevel K N data hKr).domRestrict
    (Divisor.degZero (K := K) (F := modularFunctionFieldC K N))).codRestrict _
    (fun D => frobeniusPushforwardGeomLevel_mem_degZero K N data hKr hdeg1 D.2)

@[simp]
theorem coe_frobeniusPushforwardGeomLevelDegZero
    (D : Divisor.degZero (K := K) (F := modularFunctionFieldC K N)) :
    (frobeniusPushforwardGeomLevelDegZero K N data hKr hdeg1 D
        : Divisor K (modularFunctionFieldC K N))
      = frobeniusPushforwardGeomLevel K N data hKr (D : Divisor K (modularFunctionFieldC K N)) :=
  rfl

include data hKr hdeg1 in

def frobeniusPullbackGeomLevelDegZero :
    Divisor.degZero (K := K) (F := modularFunctionFieldC K N)
      →+ Divisor.degZero (K := K) (F := modularFunctionFieldC K N) :=
  ((frobeniusPullbackGeomLevel K N data hKr).domRestrict
    (Divisor.degZero (K := K) (F := modularFunctionFieldC K N))).codRestrict _
    (fun D => frobeniusPullbackGeomLevel_mem_degZero K N data hKr hdeg1 D.2)

@[simp]
theorem coe_frobeniusPullbackGeomLevelDegZero
    (D : Divisor.degZero (K := K) (F := modularFunctionFieldC K N)) :
    (frobeniusPullbackGeomLevelDegZero K N data hKr hdeg1 D
        : Divisor K (modularFunctionFieldC K N))
      = frobeniusPullbackGeomLevel K N data hKr (D : Divisor K (modularFunctionFieldC K N)) :=
  rfl

include data hKr hdeg1 in

def heckeFibreGeomLevelDegZero :
    Divisor.degZero (K := K) (F := modularFunctionFieldC K N)
      →+ Divisor.degZero (K := K) (F := modularFunctionFieldC K N) :=
  ((heckeFibreGeomLevel K N data hKr).domRestrict
    (Divisor.degZero (K := K) (F := modularFunctionFieldC K N))).codRestrict _
    (fun D => heckeFibreGeomLevel_mem_degZero K N data hKr hdeg1 D.2)

@[simp]
theorem coe_heckeFibreGeomLevelDegZero
    (D : Divisor.degZero (K := K) (F := modularFunctionFieldC K N)) :
    (heckeFibreGeomLevelDegZero K N data hKr hdeg1 D
        : Divisor K (modularFunctionFieldC K N))
      = heckeFibreGeomLevel K N data hKr (D : Divisor K (modularFunctionFieldC K N)) :=
  rfl

include data hKr hdeg1 in

theorem heckeFibreGeomLevelDegZero_eq_add
    (D : Divisor.degZero (K := K) (F := modularFunctionFieldC K N)) :
    heckeFibreGeomLevelDegZero K N data hKr hdeg1 D
      = frobeniusPushforwardGeomLevelDegZero K N data hKr hdeg1 D
        + frobeniusPullbackGeomLevelDegZero K N data hKr hdeg1 D :=
  Subtype.ext rfl

end DegreeDivisor

section Pic0Ops

variable (K : Type*) [Field K] (N : ℕ) [NeZero N]
variable {ℓ : ℕ} [Fact ℓ.Prime] [CharP K ℓ]
variable (data : ModularPolynomialData ℓ) (hKr : KroneckerCongruence ℓ data)
variable (hperf : ∀ c : K, ∃ d : K, d ^ ℓ = c)
variable (hdeg1 : ∀ w : Place K (modularFunctionFieldC K N), w.deg = 1)

include data hKr hperf hdeg1 in

def frobeniusPushforwardGeomLevelPic0 :
    Pic0 K (modularFunctionFieldC K N) →+ Pic0 K (modularFunctionFieldC K N) :=
  QuotientAddGroup.map _ _ (frobeniusPushforwardGeomLevelDegZero K N data hKr hdeg1) (by
    rintro ⟨D, hD0⟩ hD
    simp only [AddSubgroup.mem_addSubgroupOf] at hD ⊢
    exact isPrincipal_frobeniusPushforwardGeomLevel' K N data hKr hperf hD)

@[simp]
theorem frobeniusPushforwardGeomLevelPic0_mk
    (D : Divisor.degZero (K := K) (F := modularFunctionFieldC K N)) :
    frobeniusPushforwardGeomLevelPic0 K N data hKr hperf hdeg1 (Pic0.mk D)
      = Pic0.mk (frobeniusPushforwardGeomLevelDegZero K N data hKr hdeg1 D) :=
  rfl

include data hKr hperf hdeg1 in

def frobeniusPullbackGeomLevelPic0 :
    Pic0 K (modularFunctionFieldC K N) →+ Pic0 K (modularFunctionFieldC K N) :=
  QuotientAddGroup.map _ _ (frobeniusPullbackGeomLevelDegZero K N data hKr hdeg1) (by
    rintro ⟨D, hD0⟩ hD
    simp only [AddSubgroup.mem_addSubgroupOf] at hD ⊢
    exact isPrincipal_frobeniusPullbackGeomLevel' K N data hKr hperf
      (frobOnPlacesGeomLevel_surjective K N data hKr hperf) hD)

@[simp]
theorem frobeniusPullbackGeomLevelPic0_mk
    (D : Divisor.degZero (K := K) (F := modularFunctionFieldC K N)) :
    frobeniusPullbackGeomLevelPic0 K N data hKr hperf hdeg1 (Pic0.mk D)
      = Pic0.mk (frobeniusPullbackGeomLevelDegZero K N data hKr hdeg1 D) :=
  rfl

include data hKr hperf hdeg1 in

def heckeFibreGeomLevelPic0 :
    Pic0 K (modularFunctionFieldC K N) →+ Pic0 K (modularFunctionFieldC K N) :=
  QuotientAddGroup.map _ _ (heckeFibreGeomLevelDegZero K N data hKr hdeg1) (by
    rintro ⟨D, hD0⟩ hD
    simp only [AddSubgroup.mem_addSubgroupOf] at hD ⊢
    exact isPrincipal_heckeFibreGeomLevel' K N data hKr hperf
      (frobOnPlacesGeomLevel_surjective K N data hKr hperf) hD)

@[simp]
theorem heckeFibreGeomLevelPic0_mk
    (D : Divisor.degZero (K := K) (F := modularFunctionFieldC K N)) :
    heckeFibreGeomLevelPic0 K N data hKr hperf hdeg1 (Pic0.mk D)
      = Pic0.mk (heckeFibreGeomLevelDegZero K N data hKr hdeg1 D) :=
  rfl

include data hKr hperf hdeg1 in

theorem heckeFibreGeomLevelPic0_eq_add (x : Pic0 K (modularFunctionFieldC K N)) :
    heckeFibreGeomLevelPic0 K N data hKr hperf hdeg1 x
      = frobeniusPushforwardGeomLevelPic0 K N data hKr hperf hdeg1 x
        + frobeniusPullbackGeomLevelPic0 K N data hKr hperf hdeg1 x := by
  obtain ⟨D, rfl⟩ := Pic0.mk_surjective x
  rw [heckeFibreGeomLevelPic0_mk, frobeniusPushforwardGeomLevelPic0_mk,
    frobeniusPullbackGeomLevelPic0_mk, ← Pic0.mk_add,
    heckeFibreGeomLevelDegZero_eq_add K N data hKr hdeg1 D]

include data hKr hperf hdeg1 in

theorem frobeniusPullbackGeomLevelPic0_frobeniusPushforwardGeomLevelPic0
    (x : Pic0 K (modularFunctionFieldC K N)) :
    frobeniusPullbackGeomLevelPic0 K N data hKr hperf hdeg1
        (frobeniusPushforwardGeomLevelPic0 K N data hKr hperf hdeg1 x)
      = (ℓ : ℤ) • x := by
  obtain ⟨D, rfl⟩ := Pic0.mk_surjective x
  rw [frobeniusPushforwardGeomLevelPic0_mk, frobeniusPullbackGeomLevelPic0_mk,
    show ((ℓ : ℤ) • Pic0.mk D : Pic0 K (modularFunctionFieldC K N))
      = Pic0.mk ((ℓ : ℤ) • D) from rfl]
  refine congrArg Pic0.mk (Subtype.ext ?_)
  exact frobeniusPullbackGeomLevel_frobeniusPushforwardGeomLevel K N data hKr
    (D : Divisor K (modularFunctionFieldC K N))

end Pic0Ops

section Relation

variable (K : Type*) [Field K] (N : ℕ) [NeZero N]
variable {ℓ : ℕ} [Fact ℓ.Prime] [CharP K ℓ]
variable (data : ModularPolynomialData ℓ) (hKr : KroneckerCongruence ℓ data)
variable (hperf : ∀ c : K, ∃ d : K, d ^ ℓ = c)
variable (hdeg1 : ∀ w : Place K (modularFunctionFieldC K N), w.deg = 1)

include data hKr hperf hdeg1 in

theorem eichlerShimura_special_fibre_pic0_level (x : Pic0 K (modularFunctionFieldC K N)) :
    frobeniusPushforwardGeomLevelPic0 K N data hKr hperf hdeg1
        (frobeniusPushforwardGeomLevelPic0 K N data hKr hperf hdeg1 x)
      - heckeFibreGeomLevelPic0 K N data hKr hperf hdeg1
          (frobeniusPushforwardGeomLevelPic0 K N data hKr hperf hdeg1 x)
      + (ℓ : ℤ) • x = 0 := by
  obtain ⟨D, rfl⟩ := Pic0.mk_surjective x
  rw [frobeniusPushforwardGeomLevelPic0_mk, frobeniusPushforwardGeomLevelPic0_mk,
    heckeFibreGeomLevelPic0_mk,
    show ((ℓ : ℤ) • Pic0.mk D : Pic0 K (modularFunctionFieldC K N))
      = Pic0.mk ((ℓ : ℤ) • D) from rfl,
    show (Pic0.mk _ - Pic0.mk _ + Pic0.mk ((ℓ : ℤ) • D) : Pic0 K (modularFunctionFieldC K N))
      = Pic0.mk (frobeniusPushforwardGeomLevelDegZero K N data hKr hdeg1
          (frobeniusPushforwardGeomLevelDegZero K N data hKr hdeg1 D)
        - heckeFibreGeomLevelDegZero K N data hKr hdeg1
            (frobeniusPushforwardGeomLevelDegZero K N data hKr hdeg1 D)
        + (ℓ : ℤ) • D) from rfl]
  refine congrArg Pic0.mk (Subtype.ext ?_)
  push_cast
  exact eichlerShimura_special_fibre_geom_level K N data hKr
    (D : Divisor K (modularFunctionFieldC K N))

end Relation

end ModularCurve

noncomputable section

open AlgebraicCurve

set_option synthInstance.maxHeartbeats 400000
set_option maxHeartbeats 800000

namespace ModularCurve

variable (K : Type*) [Field K]

theorem perfect_of_isAlgClosed [IsAlgClosed K] {ℓ : ℕ} [hℓ : Fact ℓ.Prime] :
    ∀ c : K, ∃ d : K, d ^ ℓ = c :=
  fun c => IsAlgClosed.exists_pow_nat_eq c hℓ.out.pos

variable (N : ℕ) [NeZero N]
variable [IsAlgClosed K] [IsCurveOver K (modularFunctionFieldC K N)]
variable {ℓ : ℕ} [Fact ℓ.Prime] [CharP K ℓ]
variable (data : ModularPolynomialData ℓ) (hKr : KroneckerCongruence ℓ data)

def frobeniusPushforwardGeomLevelPic0OfIsCurveOver :
    Pic0 K (modularFunctionFieldC K N) →+ Pic0 K (modularFunctionFieldC K N) :=
  frobeniusPushforwardGeomLevelPic0 K N data hKr (perfect_of_isAlgClosed K)
    (deg_eq_one_modularFunctionFieldC K N)

def frobeniusPullbackGeomLevelPic0OfIsCurveOver :
    Pic0 K (modularFunctionFieldC K N) →+ Pic0 K (modularFunctionFieldC K N) :=
  frobeniusPullbackGeomLevelPic0 K N data hKr (perfect_of_isAlgClosed K)
    (deg_eq_one_modularFunctionFieldC K N)

def heckeFibreGeomLevelPic0OfIsCurveOver :
    Pic0 K (modularFunctionFieldC K N) →+ Pic0 K (modularFunctionFieldC K N) :=
  heckeFibreGeomLevelPic0 K N data hKr (perfect_of_isAlgClosed K)
    (deg_eq_one_modularFunctionFieldC K N)

theorem frobeniusPushforwardGeomLevelPic0OfIsCurveOver_eq :
    frobeniusPushforwardGeomLevelPic0OfIsCurveOver K N data hKr
      = frobeniusPushforwardGeomLevelPic0 K N data hKr (perfect_of_isAlgClosed K)
          (deg_eq_one_modularFunctionFieldC K N) :=
  rfl

theorem heckeFibreGeomLevelPic0OfIsCurveOver_eq :
    heckeFibreGeomLevelPic0OfIsCurveOver K N data hKr
      = heckeFibreGeomLevelPic0 K N data hKr (perfect_of_isAlgClosed K)
          (deg_eq_one_modularFunctionFieldC K N) :=
  rfl

@[simp]
theorem frobeniusPushforwardGeomLevelPic0OfIsCurveOver_mk
    (D : Divisor.degZero (K := K) (F := modularFunctionFieldC K N)) :
    frobeniusPushforwardGeomLevelPic0OfIsCurveOver K N data hKr (Pic0.mk D)
      = Pic0.mk (frobeniusPushforwardGeomLevelDegZero K N data hKr
          (deg_eq_one_modularFunctionFieldC K N) D) :=
  rfl

@[simp]
theorem frobeniusPullbackGeomLevelPic0OfIsCurveOver_mk
    (D : Divisor.degZero (K := K) (F := modularFunctionFieldC K N)) :
    frobeniusPullbackGeomLevelPic0OfIsCurveOver K N data hKr (Pic0.mk D)
      = Pic0.mk (frobeniusPullbackGeomLevelDegZero K N data hKr
          (deg_eq_one_modularFunctionFieldC K N) D) :=
  rfl

@[simp]
theorem heckeFibreGeomLevelPic0OfIsCurveOver_mk
    (D : Divisor.degZero (K := K) (F := modularFunctionFieldC K N)) :
    heckeFibreGeomLevelPic0OfIsCurveOver K N data hKr (Pic0.mk D)
      = Pic0.mk (heckeFibreGeomLevelDegZero K N data hKr
          (deg_eq_one_modularFunctionFieldC K N) D) :=
  rfl

theorem heckeFibreGeomLevelPic0OfIsCurveOver_eq_add
    (x : Pic0 K (modularFunctionFieldC K N)) :
    heckeFibreGeomLevelPic0OfIsCurveOver K N data hKr x
      = frobeniusPushforwardGeomLevelPic0OfIsCurveOver K N data hKr x
        + frobeniusPullbackGeomLevelPic0OfIsCurveOver K N data hKr x :=
  heckeFibreGeomLevelPic0_eq_add K N data hKr (perfect_of_isAlgClosed K)
    (deg_eq_one_modularFunctionFieldC K N) x

theorem frobeniusPullbackPushforwardGeomLevelPic0OfIsCurveOver
    (x : Pic0 K (modularFunctionFieldC K N)) :
    frobeniusPullbackGeomLevelPic0OfIsCurveOver K N data hKr
        (frobeniusPushforwardGeomLevelPic0OfIsCurveOver K N data hKr x)
      = (ℓ : ℤ) • x :=
  frobeniusPullbackGeomLevelPic0_frobeniusPushforwardGeomLevelPic0 K N data hKr
    (perfect_of_isAlgClosed K) (deg_eq_one_modularFunctionFieldC K N) x

theorem eichlerShimura_special_fibre_pic0_level_of_isCurveOver
    (x : Pic0 K (modularFunctionFieldC K N)) :
    frobeniusPushforwardGeomLevelPic0OfIsCurveOver K N data hKr
        (frobeniusPushforwardGeomLevelPic0OfIsCurveOver K N data hKr x)
      - heckeFibreGeomLevelPic0OfIsCurveOver K N data hKr
          (frobeniusPushforwardGeomLevelPic0OfIsCurveOver K N data hKr x)
      + (ℓ : ℤ) • x = 0 :=
  eichlerShimura_special_fibre_pic0_level K N data hKr (perfect_of_isAlgClosed K)
    (deg_eq_one_modularFunctionFieldC K N) x

end ModularCurve

namespace ModularCurve
open AlgebraicCurve
section FamilyProps

variable (K : Type*) [Field K]

def IsCurveOverModularFunctionFieldCFamily : Prop :=
  ∀ (N : ℕ), [NeZero N] → IsCurveOver K (modularFunctionFieldC K N)

theorem isCurveOverModularFunctionFieldCFamily_iff :
    IsCurveOverModularFunctionFieldCFamily K
      ↔ ∀ (N : ℕ), [NeZero N] → IsCurveOver K (modularFunctionFieldC K N) :=
  Iff.rfl

theorem isCurveOver_modularFunctionFieldC_of_family
    (hfam : IsCurveOverModularFunctionFieldCFamily K) (N : ℕ) [NeZero N] :
    IsCurveOver K (modularFunctionFieldC K N) :=
  hfam N

variable (N : ℕ) [NeZero N]
variable [IsAlgClosed K] [IsCurveOver K (modularFunctionFieldC K N)]
variable {ℓ : ℕ} [hℓ : Fact ℓ.Prime] [CharP K ℓ]
variable (data : ModularPolynomialData ℓ) (hKr : KroneckerCongruence ℓ data)

def SpecialFibreHeckeModuleMatch
    (inst : Module HeckeAlg (Pic0 K (modularFunctionFieldC K N))) : Prop :=
  ∀ x : Pic0 K (modularFunctionFieldC K N),
    letI := inst
    heckeGen ⟨ℓ, hℓ.out⟩ • x = heckeFibreGeomLevelPic0OfIsCurveOver K N data hKr x

theorem specialFibreHeckeModuleMatch_iff
    (inst : Module HeckeAlg (Pic0 K (modularFunctionFieldC K N))) :
    SpecialFibreHeckeModuleMatch K N data hKr inst
      ↔ ∀ x, (letI := inst; heckeGen ⟨ℓ, hℓ.out⟩ • x)
          = heckeFibreGeomLevelPic0OfIsCurveOver K N data hKr x :=
  Iff.rfl

end FamilyProps
end ModularCurve