import Mathlib
import Definitions.Def_ModularCurve_JZeroNeronIdentityComponent
import Definitions.Def_GoodReductionJacobian_RelativeGroupLawBaseChange
import Definitions.Def_ModularCurve_ReductionOfPointsAgreesModL
import Definitions.Def_ModularCurve_JZeroSemistableSpecialization
import Definitions.Def_ModularCurve_JZeroNeronData
import Definitions.Def_ModularCurve_ToricDescentData
import Definitions.Def_GaloisRep_Flat
import Definitions.Def_FLTPrelim_Ramification
import Definitions.Def_ModularCurve_SupersingularNodePlaces
import Definitions.Def_JacJ1Iface

set_option autoImplicit false

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
  AlgebraicCurve IsLocalRing

noncomputable section

namespace ModularCurve

namespace JZeroNeronObjectAtP

abbrev baseRing (p : ℕ) : Type := ↥(GaloisRep.ratLocalizedAt p)

abbrev base (p : ℕ) : Scheme.{0} := Spec (CommRingCat.of (baseRing p))

abbrev genPt (p : ℕ) : Spec (CommRingCat.of (AlgebraicClosure ℚ)) ⟶ base p :=
  Spec.map (CommRingCat.ofHom (algebraMap (baseRing p) (AlgebraicClosure ℚ)))

abbrev barPt (A : ValuationSubring (AlgebraicClosure ℚ)) :
    Spec (CommRingCat.of (AlgebraicClosure ℚ)) ⟶ Spec (CommRingCat.of ↥A) :=
  Spec.map (CommRingCat.ofHom A.subtype)

abbrev resPt (A : ValuationSubring (AlgebraicClosure ℚ)) :
    Spec (CommRingCat.of (ResidueField ↥A)) ⟶ Spec (CommRingCat.of ↥A) :=
  Spec.map (CommRingCat.ofHom (residue ↥A))

def overId {B T X : Scheme.{0}} {ι : T ⟶ B} {f : X ⟶ B} (x : SchemeHomOver ι f) :
    SchemeHomOver (𝟙 T ≫ ι) f :=
  ⟨x.1, by rw [Category.id_comp]; exact x.2⟩

def toFibrePt {R R' : Type} [CommRing R] [CommRing R'] {X : Scheme.{0}}
    {ι : Spec (CommRingCat.of R') ⟶ Spec (CommRingCat.of R)} {f : X ⟶ Spec (CommRingCat.of R)}
    (x : SchemeHomOver ι f) : SchemeHomOver (𝟙 _) (RelativeGroupLaw.baseChangeStr ι f) :=
  RelativeGroupLaw.baseChangePointOfBase ι (overId x)

def ofFibrePt {R R' : Type} [CommRing R] [CommRing R'] {X : Scheme.{0}}
    {ι : Spec (CommRingCat.of R') ⟶ Spec (CommRingCat.of R)} {f : X ⟶ Spec (CommRingCat.of R)}
    (y : SchemeHomOver (𝟙 _) (RelativeGroupLaw.baseChangeStr ι f)) : SchemeHomOver ι f :=
  ⟨(RelativeGroupLaw.baseChangePointToBase ι y).1, by
    simpa only [Category.id_comp] using (RelativeGroupLaw.baseChangePointToBase ι y).2⟩

def fibreMap {R R' : Type} [CommRing R] [CommRing R'] {X Y : Scheme.{0}}
    {ι : Spec (CommRingCat.of R') ⟶ Spec (CommRingCat.of R)} {f : X ⟶ Spec (CommRingCat.of R)}
    {g : Y ⟶ Spec (CommRingCat.of R)}
    (φ : SchemeHomOver (RelativeGroupLaw.baseChangeStr ι g) (RelativeGroupLaw.baseChangeStr ι f))
    (x : SchemeHomOver ι g) : SchemeHomOver ι f :=
  ofFibrePt (NeronModelInfra.schemeHomOverComp (toFibrePt x) φ)

abbrev muCoord (S : Type) [CommRing S] (t m : ℕ) : Type := AddMonoidAlgebra S (Fin t → ZMod m)

abbrev muScheme (S : Type) [CommRing S] (t m : ℕ) : Scheme.{0} := Spec (CommRingCat.of (muCoord S t m))

abbrev muStr (S : Type) [CommRing S] (t m : ℕ) : muScheme S t m ⟶ Spec (CommRingCat.of S) :=
  Spec.map (CommRingCat.ofHom (algebraMap S (muCoord S t m)))

abbrev torusCoord (S : Type) [CommRing S] (t : ℕ) : Type := AddMonoidAlgebra S (Fin t → ℤ)

abbrev torusScheme (S : Type) [CommRing S] (t : ℕ) : Scheme.{0} := Spec (CommRingCat.of (torusCoord S t))

abbrev torusStr (S : Type) [CommRing S] (t : ℕ) : torusScheme S t ⟶ Spec (CommRingCat.of S) :=
  Spec.map (CommRingCat.ofHom (algebraMap S (torusCoord S t)))

abbrev muToTorus (S : Type) [CommRing S] (t m : ℕ) : muScheme S t m ⟶ torusScheme S t :=
  Spec.map (CommRingCat.ofHom (AddMonoidAlgebra.mapDomainRingHom S
    (AddMonoidHom.pi fun i => (Int.castAddHom (ZMod m)).comp (Pi.evalAddMonoidHom (fun _ : Fin t => ℤ) i))))

abbrev muIncl (S : Type) [CommRing S] (t : ℕ) {m m' : ℕ} (h : m ∣ m') : muScheme S t m ⟶ muScheme S t m' :=
  Spec.map (CommRingCat.ofHom (AddMonoidAlgebra.mapDomainRingHom S
    (AddMonoidHom.pi fun i => ((ZMod.castHom h (ZMod m)).toAddMonoidHom).comp
      (Pi.evalAddMonoidHom (fun _ : Fin t => ZMod m') i))))

abbrev muBaseChange {S S' : Type} [CommRing S] [CommRing S'] (φ : S →+* S') (t m : ℕ) :
    muScheme S' t m ⟶ muScheme S t m :=
  Spec.map (CommRingCat.ofHom (AddMonoidAlgebra.mapRingHom (Fin t → ZMod m) φ))

def muPt (A : ValuationSubring (AlgebraicClosure ℚ)) (t m : ℕ)
    (χ : muCoord ↥A t m →ₐ[↥A] AlgebraicClosure ℚ) : SchemeHomOver (barPt A) (muStr ↥A t m) :=
  ⟨Spec.map (CommRingCat.ofHom χ.toRingHom), by
    rw [← Spec.map_comp, ← CommRingCat.ofHom_comp]
    congr 2
    exact χ.comp_algebraMap⟩

def torusPt (S : Type) [CommRing S] (t : ℕ) (χ : torusCoord S t →ₐ[S] S) : SchemeHomOver (𝟙 _) (torusStr S t) :=
  ⟨Spec.map (CommRingCat.ofHom χ.toRingHom), by
    rw [← Spec.map_comp, ← CommRingCat.ofHom_comp]
    have h : χ.toRingHom.comp (algebraMap S (torusCoord S t)) = RingHom.id S := by
      rw [AlgHom.toRingHom_eq_coe, AlgHom.comp_algebraMap]; rfl
    rw [h, CommRingCat.ofHom_id, Spec.map_id]⟩

def castOver {B T X : Scheme.{0}} {ι ι' : T ⟶ B} {f : X ⟶ B} (h : ι = ι') (x : SchemeHomOver ι f) :
    SchemeHomOver ι' f :=
  ⟨x.1, x.2.trans h⟩

def genOfBaseChangePt {p : ℕ} {A : ValuationSubring (AlgebraicClosure ℚ)}
    {σA : Spec (CommRingCat.of ↥A) ⟶ base p} (hσA : barPt A ≫ σA = genPt p)
    {X : Scheme.{0}} {f : X ⟶ base p}
    (y : SchemeHomOver (barPt A) (RelativeGroupLaw.baseChangeStr σA f)) : SchemeHomOver (genPt p) f :=
  castOver hσA (RelativeGroupLaw.baseChangePointToBase σA y)

def ExtendsToPlace {p : ℕ} (A : ValuationSubring (AlgebraicClosure ℚ))
    (σA : Spec (CommRingCat.of ↥A) ⟶ base p) {X : Scheme.{0}} {f : X ⟶ base p}
    (x : SchemeHomOver (genPt p) f) : Prop :=
  ∃ s : SchemeHomOver σA f, x.1 = barPt A ≫ s.1

def castOverEquiv {B T X : Scheme.{0}} {ι ι' : T ⟶ B} {f : X ⟶ B} (h : ι = ι') :
    SchemeHomOver ι f ≃ SchemeHomOver ι' f where
  toFun := castOver h
  invFun := castOver h.symm
  left_inv _ := Subtype.ext rfl
  right_inv _ := Subtype.ext rfl

structure LevelData (N₀ p : ℕ) [NeZero N₀] (A : ValuationSubring (AlgebraicClosure ℚ)) where

  σA : Spec (CommRingCat.of ↥A) ⟶ base p

  hσA : barPt A ≫ σA = genPt p

  X : Scheme.{0}

  f : X ⟶ base p

  L : RelativeGroupLaw (baseRing p) f

  pts : JZero N₀ ≃ SchemeHomOver (genPt p) f

  ptsSp : JZeroC (ResidueField ↥A) N₀ ≃ SchemeHomOver (resPt A ≫ σA) f

namespace LevelData

variable {N₀ p : ℕ} [NeZero N₀] {A : ValuationSubring (AlgebraicClosure ℚ)}

def ptsA (Λ : LevelData N₀ p A) : JZero N₀ ≃ SchemeHomOver (barPt A ≫ Λ.σA) Λ.f :=
  Λ.pts.trans (castOverEquiv Λ.hσA.symm)

def IsJacobian (Λ : LevelData N₀ p A) : Prop :=
  letI := heckeModuleBar N₀
  AbelianSchemePropertyBundle (baseRing p) Λ.f ∧
  (∀ {T : Scheme.{0}} (t : T ⟶ base p) (x y : SchemeHomOver t Λ.f), Λ.L.mul t x y = Λ.L.mul t y x) ∧
  (∀ x y : JZero N₀, Λ.pts (x + y) = Λ.L.mul _ (Λ.pts x) (Λ.pts y)) ∧
  (∀ (σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) (x : JZero N₀),
    (Λ.pts (σ • x)).1 = Spec.map (CommRingCat.ofHom (σ : AlgebraicClosure ℚ →+* AlgebraicClosure ℚ)) ≫ (Λ.pts x).1) ∧
  (∀ u v : JZeroC (ResidueField ↥A) N₀, Λ.ptsSp (u + v) = Λ.L.mul _ (Λ.ptsSp u) (Λ.ptsSp v)) ∧
  (ReductionInputsModL A N₀ → ReductionOfPointsAgreesModL N₀ A Λ.f Λ.σA Λ.ptsA Λ.ptsSp) ∧
  (∀ t : HeckeAlg, ∃ φ : SchemeHomOver Λ.f Λ.f,
    (∀ {T : Scheme.{0}} (s : T ⟶ base p) (x y : SchemeHomOver s Λ.f),
      NeronModelInfra.schemeHomOverComp (Λ.L.mul s x y) φ =
        Λ.L.mul s (NeronModelInfra.schemeHomOverComp x φ) (NeronModelInfra.schemeHomOverComp y φ)) ∧
    ∀ x : JZero N₀, (Λ.pts (t • x)).1 = (Λ.pts x).1 ≫ φ.1)

end LevelData

end JZeroNeronObjectAtP

open JZeroNeronObjectAtP

attribute [local instance] instDecidableEqResidueFieldSemistable
  instAlgebraResidueFieldModularFunctionFieldCSemistable

set_option synthInstance.maxHeartbeats 400000 in
set_option maxHeartbeats 4000000 in

structure JZeroNeronObjectAtP (N₀ p : ℕ) [NeZero N₀] [Fact p.Prime] [NeZero p] (hpN₀ : ¬ p ∣ N₀)
    (A : ValuationSubring (AlgebraicClosure ℚ)) (hA : A.LiesOverPrime p)
    (Λ : JZeroNeronObjectAtP.LevelData N₀ p A) where

  G : Scheme.{0}

  g : G ⟶ base p

  L : RelativeGroupLaw (baseRing p) g

  pts : JZero (N₀ * p) ≃ SchemeHomOver (genPt p) g

  comm : L.IsCommutative

  smooth : Smooth g
  separated : IsSeparated g
  locallyOfFiniteType : LocallyOfFiniteType g
  quasiCompact : QuasiCompact g
  surjective : Surjective g
  fibre_preconnected : ∀ s : base p, _root_.IsPreconnected (g.base ⁻¹' {s})

  pts_add : ∀ x y : JZero (N₀ * p), pts (x + y) = L.mul _ (pts x) (pts y)

  pts_galois : ∀ (σ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ) (x : JZero (N₀ * p)),
    (pts (σ • x)).1 =
      Spec.map (CommRingCat.ofHom (σ : AlgebraicClosure ℚ →+* AlgebraicClosure ℚ)) ≫ (pts x).1

  hecke : letI := heckeModuleBar (N₀ * p)
    ∀ t : HeckeAlg, ∃ φ : SchemeHomOver g g,
      (∀ {T : Scheme.{0}} (s : T ⟶ base p) (x y : SchemeHomOver s g),
        NeronModelInfra.schemeHomOverComp (L.mul s x y) φ =
          L.mul s (NeronModelInfra.schemeHomOverComp x φ) (NeronModelInfra.schemeHomOverComp y φ)) ∧
      ∀ x : JZero (N₀ * p), (pts (t • x)).1 = (pts x).1 ≫ φ.1

  nsmul_flat : ∀ n : ℕ, 0 < n → Flat (L.schemeNsmul n)
  nsmul_surjective : ∀ n : ℕ, 0 < n → Surjective (L.schemeNsmul n)

  proper_generic : IsProper (pullback.snd g (Spec.map (CommRingCat.ofHom (algebraMap (baseRing p) ℚ))))

  toricRank : ℕ

  torusFibre : SchemeHomOver (torusStr (ResidueField ↥A) toricRank)
      (RelativeGroupLaw.baseChangeStr (resPt A ≫ Λ.σA) g)

  torusFibre_isClosedImmersion : IsClosedImmersion torusFibre.1

  torusFibre_mul :
    ∀ χ χ' : WithConv (torusCoord (ResidueField ↥A) toricRank →ₐ[ResidueField ↥A] ResidueField ↥A),
      NeronModelInfra.schemeHomOverComp (torusPt _ _ (χ * χ').ofConv) torusFibre =
        (L.baseChange (resPt A ≫ Λ.σA)).mul _
          (NeronModelInfra.schemeHomOverComp (torusPt _ _ χ.ofConv) torusFibre)
          (NeronModelInfra.schemeHomOverComp (torusPt _ _ χ'.ofConv) torusFibre)

  abqFibre : Fin 2 → SchemeHomOver (RelativeGroupLaw.baseChangeStr (resPt A ≫ Λ.σA) g)
      (RelativeGroupLaw.baseChangeStr (resPt A ≫ Λ.σA) Λ.f)

  abqFibre_mul : ∀ (i : Fin 2) {T : Scheme.{0}} (s : T ⟶ Spec (CommRingCat.of (ResidueField ↥A)))
      (x y : SchemeHomOver s (RelativeGroupLaw.baseChangeStr (resPt A ≫ Λ.σA) g)),
      NeronModelInfra.schemeHomOverComp ((L.baseChange (resPt A ≫ Λ.σA)).mul s x y) (abqFibre i) =
        (Λ.L.baseChange (resPt A ≫ Λ.σA)).mul s (NeronModelInfra.schemeHomOverComp x (abqFibre i))
          (NeronModelInfra.schemeHomOverComp y (abqFibre i))

  abqFibre_flat : Flat (pullback.lift (abqFibre 0).1 (abqFibre 1).1 ((abqFibre 0).2.trans (abqFibre 1).2.symm))

  abqFibre_surjective :
    Surjective (pullback.lift (abqFibre 0).1 (abqFibre 1).1 ((abqFibre 0).2.trans (abqFibre 1).2.symm))

  abqFibre_eq_one_iff : ∀ {T : Scheme.{0}} (s : T ⟶ Spec (CommRingCat.of (ResidueField ↥A)))
      (x : SchemeHomOver s (RelativeGroupLaw.baseChangeStr (resPt A ≫ Λ.σA) g)),
      (∀ i, NeronModelInfra.schemeHomOverComp x (abqFibre i) = (Λ.L.baseChange (resPt A ≫ Λ.σA)).one s) ↔
        ∃ y : SchemeHomOver s (torusStr (ResidueField ↥A) toricRank),
          NeronModelInfra.schemeHomOverComp y torusFibre = x

  abqFibre_twist : ∀ (τ : SchemeHomOver (resPt A ≫ Λ.σA) (resPt A ≫ Λ.σA)) (i : Fin 2)
      (x : SchemeHomOver (resPt A ≫ Λ.σA) g),
      fibreMap (abqFibre i) (GoodReductionJacobian.schemeHomOverComp τ.1 τ.2 x) =
        GoodReductionJacobian.schemeHomOverComp τ.1 τ.2 (fibreMap (abqFibre i) x)

  degeneracyHom : Fin 2 → SchemeHomOver g Λ.f

  degeneracyHom_mul : ∀ (i : Fin 2) {T : Scheme.{0}} (s : T ⟶ base p) (x y : SchemeHomOver s g),
      NeronModelInfra.schemeHomOverComp (L.mul s x y) (degeneracyHom i) =
        Λ.L.mul s (NeronModelInfra.schemeHomOverComp x (degeneracyHom i))
          (NeronModelInfra.schemeHomOverComp y (degeneracyHom i))

  degeneracyHom_pts : ∀ (i : Fin 2) (x : JZero (N₀ * p)),
      (Λ.pts (degeneracyPushforwardPair N₀ p i x)).1 = (pts x).1 ≫ (degeneracyHom i).1

  frobSp : JZeroC (ResidueField ↥A) N₀ →+ JZeroC (ResidueField ↥A) N₀

  frobSp_reductionModL : ∀ φ : AlgebraicClosure ℚ ≃ₐ[ℚ] AlgebraicClosure ℚ, A.IsFrobeniusAt φ p →
      ∀ y : JZero N₀, reductionModL A N₀ (φ • y) = frobSp (reductionModL A N₀ y)

  degeneracyHom_special : ∀ x : SchemeHomOver (resPt A ≫ Λ.σA) g,
      Λ.ptsSp.symm (NeronModelInfra.schemeHomOverComp x (degeneracyHom 0)) =
          Λ.ptsSp.symm (fibreMap (abqFibre 0) x) + frobSp (Λ.ptsSp.symm (fibreMap (abqFibre 1) x)) ∧
      Λ.ptsSp.symm (NeronModelInfra.schemeHomOverComp x (degeneracyHom 1)) =
          frobSp (Λ.ptsSp.symm (fibreMap (abqFibre 0) x)) + Λ.ptsSp.symm (fibreMap (abqFibre 1) x)

  ker_degeneracyHom_special_isReduced :
    let dκ := fun i : Fin 2 =>
      (NeronSpecialFibreInfra.fibreRestrictAlong (resPt A ≫ Λ.σA) Λ.f g (degeneracyHom i)).1
    let eκ := ((Λ.L.baseChange (resPt A ≫ Λ.σA)).one (𝟙 _)).1
    IsReduced (pullback (pullback.fst (dκ 0) eκ) (pullback.fst (dκ 1) eκ))

  toricLift : ∀ m : ℕ, 0 < m → SchemeHomOver (muStr ↥A toricRank m) (RelativeGroupLaw.baseChangeStr Λ.σA g)

  toricLift_isClosedImmersion : ∀ (m : ℕ) (hm : 0 < m), IsClosedImmersion (toricLift m hm).1

  toricLift_mul : ∀ (m : ℕ) (hm : 0 < m) (χ χ' : WithConv (muCoord ↥A toricRank m →ₐ[↥A] AlgebraicClosure ℚ)),
      NeronModelInfra.schemeHomOverComp (muPt A toricRank m (χ * χ').ofConv) (toricLift m hm) =
        (L.baseChange Λ.σA).mul _ (NeronModelInfra.schemeHomOverComp (muPt A toricRank m χ.ofConv) (toricLift m hm))
          (NeronModelInfra.schemeHomOverComp (muPt A toricRank m χ'.ofConv) (toricLift m hm))

  toricLift_compat : ∀ (m m' : ℕ) (hm : 0 < m) (hm' : 0 < m') (h : m ∣ m'),
      muIncl ↥A toricRank h ≫ (toricLift m' hm').1 = (toricLift m hm).1

  toricLift_special : ∀ (m : ℕ) (hm : 0 < m),
      muBaseChange (residue ↥A) toricRank m ≫ (toricLift m hm).1 ≫ pullback.fst g Λ.σA =
        muToTorus (ResidueField ↥A) toricRank m ≫ torusFibre.1 ≫ pullback.fst g (resPt A ≫ Λ.σA)

  toricLift_inertia : ∀ (m : ℕ) (hm : 0 < m), ∀ σ ∈ A.inertiaSubgroupIn ℚ, ∀ c : ℕ,
      (∀ ζ : AlgebraicClosure ℚ, ζ ^ m = 1 → σ ζ = ζ ^ c) →
      ∀ χ : muCoord ↥A toricRank m →ₐ[↥A] AlgebraicClosure ℚ,
        σ • pts.symm (genOfBaseChangePt Λ.hσA
            (NeronModelInfra.schemeHomOverComp (muPt A toricRank m χ) (toricLift m hm))) =
          c • pts.symm (genOfBaseChangePt Λ.hσA
            (NeronModelInfra.schemeHomOverComp (muPt A toricRank m χ) (toricLift m hm)))

  toricLift_dec : ∀ (m : ℕ) (hm : 0 < m), ∀ σ ∈ A.decompositionSubgroup ℚ,
      ∀ χ : muCoord ↥A toricRank m →ₐ[↥A] AlgebraicClosure ℚ,
        ∃ χ' : muCoord ↥A toricRank m →ₐ[↥A] AlgebraicClosure ℚ,
          σ • pts.symm (genOfBaseChangePt Λ.hσA
              (NeronModelInfra.schemeHomOverComp (muPt A toricRank m χ) (toricLift m hm))) =
            pts.symm (genOfBaseChangePt Λ.hσA
              (NeronModelInfra.schemeHomOverComp (muPt A toricRank m χ') (toricLift m hm)))

  ssFinset : Finset (Place (ResidueField ↥A) (modularFunctionFieldC (ResidueField ↥A) N₀))

  mem_ssFinset_iff : ∀ w, w ∈ ssFinset ↔ w ∈ ssPlaces p N₀ (ResidueField ↥A)

  frob : SemilinearAut (ResidueField ↥A) (modularFunctionFieldC (ResidueField ↥A) N₀)

  baseAut_frob : ∀ a : ResidueField ↥A, SemilinearAut.baseAut frob a = a ^ p

  frob_jGeomGen : frob • (jGeomGen (ResidueField ↥A) N₀ : modularFunctionFieldC (ResidueField ↥A) N₀) =
    jGeomGen (ResidueField ↥A) N₀
  frob_jNGeomGen : frob • (jNGeomGen (ResidueField ↥A) N₀ : modularFunctionFieldC (ResidueField ↥A) N₀) =
    jNGeomGen (ResidueField ↥A) N₀

  toricRank_succ_eq_card : toricRank + 1 = ssFinset.card

  width : ↥(nodePairsOfPlaces frob ssFinset) → ℕ

  width_pos : ∀ s, 0 < width s

  comp : ↥(inertiaInvariants A (N₀ * p)) →+ componentGroup width

  comp_heckeGen : letI := heckeModuleBar (N₀ * p)
    ∀ ℓ : Nat.Primes, ¬ (ℓ : ℕ) ∣ N₀ * p →
    ∀ (x : ↥(inertiaInvariants A (N₀ * p)))
      (hx : heckeGen ℓ • (x : JZero (N₀ * p)) ∈ inertiaInvariants A (N₀ * p)),
      comp ⟨heckeGen ℓ • (x : JZero (N₀ * p)), hx⟩ = (((ℓ : ℕ) : ℤ) + 1) • comp x

  comp_surjective : Function.Surjective comp

  comp_eq_zero_iff : ∀ x : ↥(inertiaInvariants A (N₀ * p)),
      comp x = 0 ↔ ExtendsToPlace A Λ.σA (pts (x : JZero (N₀ * p)))

attribute [nolint docBlame] JZeroNeronObjectAtP.separated JZeroNeronObjectAtP.locallyOfFiniteType
  JZeroNeronObjectAtP.quasiCompact JZeroNeronObjectAtP.surjective JZeroNeronObjectAtP.fibre_preconnected
  JZeroNeronObjectAtP.nsmul_surjective JZeroNeronObjectAtP.frob_jNGeomGen

namespace JZeroNeronObjectAtP

variable {N₀ p : ℕ} [NeZero N₀] [Fact p.Prime] [NeZero p] {hpN₀ : ¬ p ∣ N₀}
  {A : ValuationSubring (AlgebraicClosure ℚ)} {hA : A.LiesOverPrime p}
  {Λ : LevelData N₀ p A}

abbrev nodes (O : JZeroNeronObjectAtP N₀ p hpN₀ A hA Λ) :
    Finset (Place (ResidueField ↥A) (modularFunctionFieldC (ResidueField ↥A) N₀) ×
      Place (ResidueField ↥A) (modularFunctionFieldC (ResidueField ↥A) N₀)) :=
  nodePairsOfPlaces O.frob O.ssFinset

def toricPoint (O : JZeroNeronObjectAtP N₀ p hpN₀ A hA Λ) (m : ℕ) (hm : 0 < m)
    (χ : muCoord ↥A O.toricRank m →ₐ[↥A] AlgebraicClosure ℚ) : JZero (N₀ * p) :=
  O.pts.symm (genOfBaseChangePt Λ.hσA
    (NeronModelInfra.schemeHomOverComp (muPt A O.toricRank m χ) (O.toricLift m hm)))

def toricPts (O : JZeroNeronObjectAtP N₀ p hpN₀ A hA Λ) (m : ℕ) : AddSubgroup (JZero (N₀ * p)) :=
  if hm : 0 < m then AddSubgroup.closure (Set.range (O.toricPoint m hm)) else ⊥

def finPts (O : JZeroNeronObjectAtP N₀ p hpN₀ A hA Λ) (m : ℕ) : AddSubgroup (JZero (N₀ * p)) :=
  AddSubgroup.closure {x | x ∈ jZeroTorsion (N₀ * p) m ∧ ExtendsToPlace A Λ.σA (O.pts x)}

end JZeroNeronObjectAtP

end ModularCurve

end