import Mathlib
import Definitions.Def_AlgebraicGeometry_ResolvedModelGlueComponents
import Definitions.Def_ModularCurve_DRResolvedModelPackageV4
import Definitions.Def_ModularCurve_DRModelPackage
import Definitions.Def_MvPolynomial_CrossingResolutionScheme
import Definitions.Def_MvPolynomial_CrossingResolutionFibrePoints

set_option autoImplicit false
set_option maxHeartbeats 1600000
set_option synthInstance.maxHeartbeats 400000

open CategoryTheory CategoryTheory.Limits AlgebraicGeometry

noncomputable section

namespace V3Glue.SiteAux

theorem locallyOfFinitePresentation_of_isLocallyNoetherian {X Y : Scheme.{0}} (f : X ⟶ Y)
    [IsLocallyNoetherian Y] [LocallyOfFiniteType f] : LocallyOfFinitePresentation f := by
  refine ⟨fun {U} hU {V} hV e => ?_⟩
  haveI : IsNoetherianRing Γ(Y, U) := IsLocallyNoetherian.component_noetherian ⟨U, hU⟩
  have hft : (f.appLE U V e).hom.FiniteType := f.finiteType_appLE hU hV e
  letI := (f.appLE U V e).hom.toAlgebra
  have : Algebra.FiniteType Γ(Y, U) Γ(X, V) := hft
  exact (Algebra.FinitePresentation.of_finiteType (R := Γ(Y, U)) (A := Γ(X, V))).mp this

end V3Glue.SiteAux

end

noncomputable section

namespace V3Glue.Site

open ModularCurve MvPolynomial MvPolynomial.CrossingQuotient

variable (p : ℕ) [Fact p.Prime] (𝔛 : DRModelPackage p) (O : Type) [CommRing O] [IsDomain O]
  [IsDiscreteValuationRing O]
  (κ : Type) [Field κ] [CharP κ p] [IsAlgClosed κ]

abbrev XO : Scheme.{0} := pullback (DRModel.toBase p) (Spec.map (CommRingCat.ofHom (algebraMap ℤ O)))

abbrev Node : Type := ↥(pullback (𝔛.compInf κ) (𝔛.compZero κ))

variable (bc : pullback (DRModel.toBase p) (Spec.map (CommRingCat.ofHom (algebraMap ℤ κ))) ⟶ XO p O)

variable {p O κ} in

abbrev xpt (n : Node p 𝔛 κ) : XO p O :=
  (pullback.fst (𝔛.compInf κ) (𝔛.compZero κ) ≫ 𝔛.compInf κ ≫ bc).base n

def HasOrientedCrossingCharts : Prop :=
    ∀ n : ↥(pullback (𝔛.compInf κ) (𝔛.compZero κ)),
      ∃ (e : ℕ) (_ : 1 ≤ e)
        (U : (pullback (DRModel.toBase p) (Spec.map (CommRingCat.ofHom (algebraMap ℤ O)))).Opens)
        (_ : (pullback.fst (𝔛.compInf κ) (𝔛.compZero κ) ≫ 𝔛.compInf κ ≫ bc).base n ∈ U)
        (f : (U : Scheme.{0}) ⟶ CrossingQuotient.crossingScheme (((p : ℕ) : O) ^ e)),

        f ≫ Spec.map (CommRingCat.ofHom (algebraMap O (CrossingQuotient O (((p : ℕ) : O) ^ e)))) =
            U.ι ≫ pullback.snd _ _ ∧

        (∀ y : ↥(U : Scheme.{0}),
            (CrossingQuotient.U (((p : ℕ) : O) ^ e) ∈ (f.base y).asIdeal ∧
              CrossingQuotient.V (((p : ℕ) : O) ^ e) ∈ (f.base y).asIdeal) ↔
            U.ι.base y = (pullback.fst (𝔛.compInf κ) (𝔛.compZero κ) ≫ 𝔛.compInf κ ≫ bc).base n) ∧

        (∀ y : ↥(U : Scheme.{0}), U.ι.base y = (pullback.fst (𝔛.compInf κ) (𝔛.compZero κ) ≫ 𝔛.compInf κ ≫ bc).base n →
            (f.stalkMap y).hom.Flat ∧
            Ideal.map (f.stalkMap y).hom (IsLocalRing.maximalIdeal _) = IsLocalRing.maximalIdeal _ ∧
            IsIso (f.residueFieldMap y)) ∧

        (∀ y : ↥(U : Scheme.{0}), CrossingQuotient.V (((p : ℕ) : O) ^ e) ∈ (f.base y).asIdeal →
            U.ι.base y ∈ Set.range (𝔛.compInf κ ≫ bc).base) ∧
        (∀ y : ↥(U : Scheme.{0}), CrossingQuotient.U (((p : ℕ) : O) ^ e) ∈ (f.base y).asIdeal →
            U.ι.base y ∈ Set.range (𝔛.compZero κ ≫ bc).base) ∧

        (∀ y : ↥(U : Scheme.{0}), U.ι.base y ∈ Set.range (𝔛.compInf κ ≫ bc).base →
            CrossingQuotient.V (((p : ℕ) : O) ^ e) ∈ (f.base y).asIdeal) ∧
        (∀ y : ↥(U : Scheme.{0}), U.ι.base y ∈ Set.range (𝔛.compZero κ ≫ bc).base →
            CrossingQuotient.U (((p : ℕ) : O) ^ e) ∈ (f.base y).asIdeal)

structure ModelHyps : Prop where

  L6 : ∀ e : ℕ, 0 < e → IsIso (Resolution.toCrossing ((p : ℕ) : O) e ∣_
    (PrimeSpectrum.basicOpen (CrossingQuotient.U (((p : ℕ) : O) ^ e)) ⊔ PrimeSpectrum.basicOpen (CrossingQuotient.V (((p : ℕ) : O) ^ e))))

  P6 : ∀ e : ℕ, IsProper (Resolution.toCrossing ((p : ℕ) : O) e)

  flat : ∀ e : ℕ, Flat (Resolution.toCrossing ((p : ℕ) : O) e ≫
    Spec.map (CommRingCat.ofHom (algebraMap O (CrossingQuotient O (((p : ℕ) : O) ^ e)))))

  noeth : ∀ e : ℕ, IsLocallyNoetherian (Resolution ((p : ℕ) : O) e)

  interior : ∀ e : ℕ, interior ((Resolution.toCrossing ((p : ℕ) : O) e).base ⁻¹'
    ((PrimeSpectrum.basicOpen (CrossingQuotient.U (((p : ℕ) : O) ^ e)) ⊔
      PrimeSpectrum.basicOpen (CrossingQuotient.V (((p : ℕ) : O) ^ e)) : (crossingScheme (((p : ℕ) : O) ^ e)).Opens) :
        Set (crossingScheme (((p : ℕ) : O) ^ e)))ᶜ) = ∅

def EtNbhd : Prop :=
  ∀ {U S : Scheme.{0}} (f : U ⟶ S) [LocallyOfFinitePresentation f] (x : U),
    (f.stalkMap x).hom.Flat →
    Ideal.map (f.stalkMap x).hom (IsLocalRing.maximalIdeal (S.presheaf.stalk (f.base x))) =
      IsLocalRing.maximalIdeal (U.presheaf.stalk x) →
    ∀ [IsIso (f.residueFieldMap x)], ∃ V : U.Opens, x ∈ V ∧ Etale (V.ι ≫ f)

structure ChartData (n : Node p 𝔛 κ) where
  e : ℕ
  one_le_e : 1 ≤ e
  U : (XO p O).Opens
  x_mem_U : xpt 𝔛 bc n ∈ U
  f : (U : Scheme.{0}) ⟶ crossingScheme (((p : ℕ) : O) ^ e)
  f_over : f ≫ Spec.map (CommRingCat.ofHom (algebraMap O (CrossingQuotient O (((p : ℕ) : O) ^ e)))) = U.ι ≫ pullback.snd _ _
  f_fibre : ∀ y : ↥(U : Scheme.{0}),
    (CrossingQuotient.U (((p : ℕ) : O) ^ e) ∈ (f.base y).asIdeal ∧ CrossingQuotient.V (((p : ℕ) : O) ^ e) ∈ (f.base y).asIdeal) ↔
      U.ι.base y = xpt 𝔛 bc n
  f_node : ∀ y : ↥(U : Scheme.{0}), U.ι.base y = xpt 𝔛 bc n →
    (f.stalkMap y).hom.Flat ∧
      Ideal.map (f.stalkMap y).hom (IsLocalRing.maximalIdeal _) = IsLocalRing.maximalIdeal _ ∧ IsIso (f.residueFieldMap y)

  orient_inf : ∀ y : ↥(U : Scheme.{0}), CrossingQuotient.V (((p : ℕ) : O) ^ e) ∈ (f.base y).asIdeal →
    U.ι.base y ∈ Set.range (𝔛.compInf κ ≫ bc).base

  orient_zero : ∀ y : ↥(U : Scheme.{0}), CrossingQuotient.U (((p : ℕ) : O) ^ e) ∈ (f.base y).asIdeal →
    U.ι.base y ∈ Set.range (𝔛.compZero κ ≫ bc).base

  orient_inf_conv : ∀ y : ↥(U : Scheme.{0}), U.ι.base y ∈ Set.range (𝔛.compInf κ ≫ bc).base →
    CrossingQuotient.V (((p : ℕ) : O) ^ e) ∈ (f.base y).asIdeal
  orient_zero_conv : ∀ y : ↥(U : Scheme.{0}), U.ι.base y ∈ Set.range (𝔛.compZero κ ≫ bc).base →
    CrossingQuotient.U (((p : ℕ) : O) ^ e) ∈ (f.base y).asIdeal

def chartData (hC : HasOrientedCrossingCharts p 𝔛 O κ bc) (n : Node p 𝔛 κ) : ChartData p 𝔛 O κ bc n :=
  let h₁ := hC n
  let h₂ := h₁.choose_spec
  let h₃ := h₂.choose_spec
  let h₄ := h₃.choose_spec
  let h₅ := h₄.choose_spec
  let h := h₅.choose_spec
  { e := h₁.choose
    one_le_e := h₂.choose
    U := h₃.choose
    x_mem_U := h₄.choose
    f := h₅.choose
    f_over := h.1
    f_fibre := h.2.1
    f_node := h.2.2.1
    orient_inf := h.2.2.2.1
    orient_zero := h.2.2.2.2.1
    orient_inf_conv := h.2.2.2.2.2.1
    orient_zero_conv := h.2.2.2.2.2.2 }

def rawChartInputOfDR (hϖ : IsLocalRing.maximalIdeal O = Ideal.span {((p : ℕ) : O)}) (M : ModelHyps p O)
    (hC : HasOrientedCrossingCharts p 𝔛 O κ bc)
    (hxinj : Function.Injective (fun n : Node p 𝔛 κ => xpt 𝔛 bc n))
    (hxcl : ∀ n : Node p 𝔛 κ, IsClosed ({xpt 𝔛 bc n} : Set (XO p O))) :
    RawChartInput (XO p O) (Node p 𝔛 κ) := by

  haveI : IsProper (DRModel.toBase p) := 𝔛.isProper
  haveI : LocallyOfFiniteType (pullback.snd (DRModel.toBase p) (Spec.map (CommRingCat.ofHom (algebraMap ℤ O)))) :=
    MorphismProperty.pullback_snd _ _ inferInstance
  have hlfp : ∀ n, LocallyOfFinitePresentation (chartData p 𝔛 O κ bc hC n).f := fun n => by
    have : LocallyOfFiniteType ((chartData p 𝔛 O κ bc hC n).f ≫
        Spec.map (CommRingCat.ofHom (algebraMap O (CrossingQuotient O (((p : ℕ) : O) ^ (chartData p 𝔛 O κ bc hC n).e))))) := by
      rw [(chartData p 𝔛 O κ bc hC n).f_over]; infer_instance
    haveI := locallyOfFiniteType_of_comp (chartData p 𝔛 O κ bc hC n).f
      (Spec.map (CommRingCat.ofHom (algebraMap O (CrossingQuotient O (((p : ℕ) : O) ^ (chartData p 𝔛 O κ bc hC n).e)))))
    exact V3Glue.SiteAux.locallyOfFinitePresentation_of_isLocallyNoetherian (chartData p 𝔛 O κ bc hC n).f
  exact
  { x := fun n => xpt 𝔛 bc n
    x_injective := hxinj
    isClosed_x := hxcl
    S := fun n => crossingScheme (((p : ℕ) : O) ^ (chartData p 𝔛 O κ bc hC n).e)
    Vc := fun n => PrimeSpectrum.basicOpen (CrossingQuotient.U (((p : ℕ) : O) ^ (chartData p 𝔛 O κ bc hC n).e)) ⊔
      PrimeSpectrum.basicOpen (CrossingQuotient.V (((p : ℕ) : O) ^ (chartData p 𝔛 O κ bc hC n).e))
    Res := fun n => Resolution ((p : ℕ) : O) (chartData p 𝔛 O κ bc hC n).e
    ρ := fun n => Resolution.toCrossing ((p : ℕ) : O) (chartData p 𝔛 O κ bc hC n).e

    isIso_ρ_restrict := fun n => M.L6 _ (chartData p 𝔛 O κ bc hC n).one_le_e

    isProper_ρ := fun n => M.P6 (chartData p 𝔛 O κ bc hC n).e
    thick := fun n => (chartData p 𝔛 O κ bc hC n).e
    one_le_thick := fun n => (chartData p 𝔛 O κ bc hC n).one_le_e
    U₀ := fun n => (chartData p 𝔛 O κ bc hC n).U
    x_mem_U₀ := fun n => (chartData p 𝔛 O κ bc hC n).x_mem_U
    f₀ := fun n => (chartData p 𝔛 O κ bc hC n).f
    f₀_mem_Vc_iff := fun n y => by
      have h := (chartData p 𝔛 O κ bc hC n).f_fibre y
      have hy : ((chartData p 𝔛 O κ bc hC n).U).ι.base y = (y : XO p O) := by simp
      rw [hy] at h
      have key : (chartData p 𝔛 O κ bc hC n).f.base y ∈
          (PrimeSpectrum.basicOpen (CrossingQuotient.U (((p : ℕ) : O) ^ (chartData p 𝔛 O κ bc hC n).e)) ⊔
            PrimeSpectrum.basicOpen (CrossingQuotient.V (((p : ℕ) : O) ^ (chartData p 𝔛 O κ bc hC n).e)) :
              TopologicalSpace.Opens (PrimeSpectrum (CrossingQuotient O (((p : ℕ) : O) ^ (chartData p 𝔛 O κ bc hC n).e)))) ↔
          (chartData p 𝔛 O κ bc hC n).f.base y ∈
              PrimeSpectrum.basicOpen (CrossingQuotient.U (((p : ℕ) : O) ^ (chartData p 𝔛 O κ bc hC n).e)) ∨
            (chartData p 𝔛 O κ bc hC n).f.base y ∈
              PrimeSpectrum.basicOpen (CrossingQuotient.V (((p : ℕ) : O) ^ (chartData p 𝔛 O κ bc hC n).e)) :=
        TopologicalSpace.Opens.mem_sup
      have kU : (chartData p 𝔛 O κ bc hC n).f.base y ∈
            PrimeSpectrum.basicOpen (CrossingQuotient.U (((p : ℕ) : O) ^ (chartData p 𝔛 O κ bc hC n).e)) ↔
          CrossingQuotient.U (((p : ℕ) : O) ^ (chartData p 𝔛 O κ bc hC n).e) ∉ ((chartData p 𝔛 O κ bc hC n).f.base y).asIdeal :=
        PrimeSpectrum.mem_basicOpen _ _
      have kV : (chartData p 𝔛 O κ bc hC n).f.base y ∈
            PrimeSpectrum.basicOpen (CrossingQuotient.V (((p : ℕ) : O) ^ (chartData p 𝔛 O κ bc hC n).e)) ↔
          CrossingQuotient.V (((p : ℕ) : O) ^ (chartData p 𝔛 O κ bc hC n).e) ∉ ((chartData p 𝔛 O κ bc hC n).f.base y).asIdeal :=
        PrimeSpectrum.mem_basicOpen _ _
      refine key.trans ((kU.or kV).trans ?_)
      rw [← not_and_or]
      exact not_congr h

    f₀_node := fun n y hy => by
      have hy' : ((chartData p 𝔛 O κ bc hC n).U).ι.base y = xpt 𝔛 bc n := by rw [← hy]; simp
      exact (chartData p 𝔛 O κ bc hC n).f_node y hy'
    f₀_lfp := hlfp
    B := Spec (CommRingCat.of O)
    πX := pullback.snd _ _
    σ := fun n => Spec.map (CommRingCat.ofHom (algebraMap O (CrossingQuotient O (((p : ℕ) : O) ^ (chartData p 𝔛 O κ bc hC n).e))))
    f₀_over := fun n => (chartData p 𝔛 O κ bc hC n).f_over

    flat_ρ_σ := fun n => M.flat (chartData p 𝔛 O κ bc hC n).e
    isLocallyNoetherian_Res := fun n => M.noeth (chartData p 𝔛 O κ bc hC n).e
    interior_preimage_vertex := fun n => M.interior (chartData p 𝔛 O κ bc hC n).e }

@[simp] theorem rawChartInputOfDR_U₀ (hϖ : IsLocalRing.maximalIdeal O = Ideal.span {((p : ℕ) : O)}) (M : ModelHyps p O)
    (hC : HasOrientedCrossingCharts p 𝔛 O κ bc) (hxinj hxcl) (n : Node p 𝔛 κ) :
    (rawChartInputOfDR p 𝔛 O κ bc hϖ M hC hxinj hxcl).U₀ n = (chartData p 𝔛 O κ bc hC n).U := rfl

@[simp] theorem rawChartInputOfDR_f₀ (hϖ : IsLocalRing.maximalIdeal O = Ideal.span {((p : ℕ) : O)}) (M : ModelHyps p O)
    (hC : HasOrientedCrossingCharts p 𝔛 O κ bc) (hxinj hxcl) (n : Node p 𝔛 κ) :
    (rawChartInputOfDR p 𝔛 O κ bc hϖ M hC hxinj hxcl).f₀ n = (chartData p 𝔛 O κ bc hC n).f := rfl

@[simp] theorem rawChartInputOfDR_thick (hϖ : IsLocalRing.maximalIdeal O = Ideal.span {((p : ℕ) : O)}) (M : ModelHyps p O)
    (hC : HasOrientedCrossingCharts p 𝔛 O κ bc) (hxinj hxcl) (n : Node p 𝔛 κ) :
    (rawChartInputOfDR p 𝔛 O κ bc hϖ M hC hxinj hxcl).thick n = (chartData p 𝔛 O κ bc hC n).e := rfl

def chartInputOfDR [Finite (Node p 𝔛 κ)] (hϖ : IsLocalRing.maximalIdeal O = Ideal.span {((p : ℕ) : O)}) (M : ModelHyps p O)
    (hC : HasOrientedCrossingCharts p 𝔛 O κ bc) (ET : EtNbhd)
    (hxinj : Function.Injective (fun n : Node p 𝔛 κ => xpt 𝔛 bc n))
    (hxcl : ∀ n : Node p 𝔛 κ, IsClosed ({xpt 𝔛 bc n} : Set (XO p O))) :
    ChartInput (XO p O) (Node p 𝔛 κ) :=
  (rawChartInputOfDR p 𝔛 O κ bc hϖ M hC hxinj hxcl).toChartInput
    ((rawChartInputOfDR p 𝔛 O κ bc hϖ M hC hxinj hxcl).hnbhd_of ET)

end V3Glue.Site

end

noncomputable section

namespace V3Asm

open ModularCurve MvPolynomial MvPolynomial.CrossingQuotient

variable (p : ℕ) [Fact p.Prime] (𝔛 : DRModelPackage p) (O : Type) [CommRing O] [IsDomain O]
  [IsDiscreteValuationRing O] (κ : Type) [Field κ] [CharP κ p] [IsAlgClosed κ] (toκ : O →+* κ)

abbrev πX : V3Glue.Site.XO p O ⟶ Spec (CommRingCat.of O) := pullback.snd _ _

abbrev bc : pullback (DRModel.toBase p) (Spec.map (CommRingCat.ofHom (algebraMap ℤ κ))) ⟶ V3Glue.Site.XO p O :=
  DRModel.baseChangeMap toκ

theorem bc_fst : bc p O κ toκ ≫ pullback.fst _ _ = pullback.fst _ _ := by
  rw [bc, DRModel.baseChangeMap, pullback.lift_fst, Category.comp_id]

theorem bc_snd : bc p O κ toκ ≫ pullback.snd _ _ = pullback.snd _ _ ≫ Spec.map (CommRingCat.ofHom toκ) := by
  rw [bc, DRModel.baseChangeMap, pullback.lift_snd]

structure SiteHyps : Prop where
  nodeFinite : Finite (V3Glue.Site.Node p 𝔛 κ)
  hC : V3Glue.Site.HasOrientedCrossingCharts p 𝔛 O κ (bc p O κ toκ)
  ET : V3Glue.Site.EtNbhd
  hxinj : Function.Injective (fun n : V3Glue.Site.Node p 𝔛 κ => V3Glue.Site.xpt 𝔛 (bc p O κ toκ) n)
  hxcl : ∀ n : V3Glue.Site.Node p 𝔛 κ, IsClosed ({V3Glue.Site.xpt 𝔛 (bc p O κ toκ) n} : Set (V3Glue.Site.XO p O))
  model : V3Glue.Site.ModelHyps p O

variable (hϖ : IsLocalRing.maximalIdeal O = Ideal.span {((p : ℕ) : O)}) (H : SiteHyps p 𝔛 O κ toκ)

def R : V3Glue.RawChartInput (V3Glue.Site.XO p O) (V3Glue.Site.Node p 𝔛 κ) :=
  V3Glue.Site.rawChartInputOfDR p 𝔛 O κ (bc p O κ toκ) hϖ H.model H.hC H.hxinj H.hxcl

def C : V3Glue.ChartInput (V3Glue.Site.XO p O) (V3Glue.Site.Node p 𝔛 κ) :=
  haveI := H.nodeFinite
  V3Glue.Site.chartInputOfDR p 𝔛 O κ (bc p O κ toκ) hϖ H.model H.hC H.ET H.hxinj H.hxcl

def D : V3Glue.GlueInput (V3Glue.Site.XO p O) (V3Glue.Site.Node p 𝔛 κ) := (C p 𝔛 O κ toκ hϖ H).toGlueInput
def Y : Scheme.{0} := (D p 𝔛 O κ toκ hϖ H).glued
def toDR : Y p 𝔛 O κ toκ hϖ H ⟶ V3Glue.Site.XO p O := (D p 𝔛 O κ toκ hϖ H).toDR
def toBase : Y p 𝔛 O κ toκ hϖ H ⟶ Spec (CommRingCat.of O) := toDR p 𝔛 O κ toκ hϖ H ≫ πX p O

theorem toDR_over : toDR p 𝔛 O κ toκ hϖ H ≫ pullback.snd _ _ = toBase p 𝔛 O κ toκ hϖ H := rfl

theorem hq : ∀ n (y : (D p 𝔛 O κ toκ hϖ H).Y n), (((D p 𝔛 O κ toκ hϖ H).q n).base y).1 ∈ (D p 𝔛 O κ toκ hϖ H).X0 →
    y ∈ Set.range ((D p 𝔛 O κ toκ hϖ H).j n).base :=
  (C p 𝔛 O κ toκ hϖ H).hq

theorem mem_X0_iff (x : V3Glue.Site.XO p O) :
    x ∈ (D p 𝔛 O κ toκ hϖ H).X0 ↔ ∀ n, x ≠ V3Glue.Site.xpt 𝔛 (bc p O κ toκ) n := by
  haveI := H.nodeFinite
  exact V3Glue.RawChartInput.mem_X0 _ x

def width : V3Glue.Site.Node p 𝔛 κ → ℕ := (C p 𝔛 O κ toκ hϖ H).thick

theorem one_le_width : ∀ n, 1 ≤ width p 𝔛 O κ toκ hϖ H n := (C p 𝔛 O κ toκ hϖ H).one_le_thick

theorem hRF : ∀ n, IsIso (((C p 𝔛 O κ toκ hϖ H).f n).residueFieldMap ((C p 𝔛 O κ toκ hϖ H).xU n)) :=
  fun n => (C p 𝔛 O κ toκ hϖ H).f_res n

include hϖ in

theorem p_mem_maximalIdeal : ((p : ℕ) : O) ∈ IsLocalRing.maximalIdeal O :=
  hϖ ▸ Ideal.mem_span_singleton_self _

def chartIso (n : V3Glue.Site.Node p 𝔛 κ) : (C p 𝔛 O κ toκ hϖ H).Y n ≅ ↑(toDR p 𝔛 O κ toκ hϖ H ⁻¹ᵁ (C p 𝔛 O κ toκ hϖ H).U n) :=
  IsPullback.isoIsPullback _ _ ((D p 𝔛 O κ toκ hϖ H).isPullback_ιY (hq p 𝔛 O κ toκ hϖ H) n)
    (isPullback_morphismRestrict (toDR p 𝔛 O κ toκ hϖ H) ((C p 𝔛 O κ toκ hϖ H).U n))

theorem chartIso_hom_fst (n : V3Glue.Site.Node p 𝔛 κ) :
    (chartIso p 𝔛 O κ toκ hϖ H n).hom ≫ (toDR p 𝔛 O κ toκ hϖ H ∣_ (C p 𝔛 O κ toκ hϖ H).U n) = (C p 𝔛 O κ toκ hϖ H).q n :=
  IsPullback.isoIsPullback_hom_fst _ _ _ _

def ξ : Fin 2 → V3Glue.Site.XO p O :=
  Fin.cases ((𝔛.compInf κ ≫ DRModel.baseChangeMap toκ).base (genericPoint (𝔛.ratModel κ).C))
    (fun _ => (𝔛.compZero κ ≫ DRModel.baseChangeMap toκ).base (genericPoint (𝔛.ratModel κ).C))

@[simp] theorem ξ_zero :
    ξ p 𝔛 O κ toκ 0 = (𝔛.compInf κ ≫ DRModel.baseChangeMap toκ).base (genericPoint (𝔛.ratModel κ).C) := rfl
@[simp] theorem ξ_one :
    ξ p 𝔛 O κ toκ 1 = (𝔛.compZero κ ≫ DRModel.baseChangeMap toκ).base (genericPoint (𝔛.ratModel κ).C) := rfl

theorem vertex_eq (n : V3Glue.Site.Node p 𝔛 κ) :
    (C p 𝔛 O κ toκ hϖ H).vertex n = MvPolynomial.CrossingQuotient.Resolution.vertexPt ((p : ℕ) : O) ((C p 𝔛 O κ toκ hϖ H).thick n) (IsLocalRing.maximalIdeal O)
      (p_mem_maximalIdeal p O hϖ) ((C p 𝔛 O κ toκ hϖ H).one_le_thick n) := by
  have hUV : ((C p 𝔛 O κ toκ hϖ H).f n).base ((C p 𝔛 O κ toκ hϖ H).xU n) ∉ (C p 𝔛 O κ toκ hϖ H).Vc n := by
    rw [(C p 𝔛 O κ toκ hϖ H).f_mem_Vc_iff]; exact fun h => h rfl
  have hUV' : ¬ (((C p 𝔛 O κ toκ hϖ H).f n).base ((C p 𝔛 O κ toκ hϖ H).xU n) ∈
        PrimeSpectrum.basicOpen (MvPolynomial.CrossingQuotient.U (((p : ℕ) : O) ^ ((C p 𝔛 O κ toκ hϖ H).thick n))) ∨
      ((C p 𝔛 O κ toκ hϖ H).f n).base ((C p 𝔛 O κ toκ hϖ H).xU n) ∈
        PrimeSpectrum.basicOpen (MvPolynomial.CrossingQuotient.V (((p : ℕ) : O) ^ ((C p 𝔛 O κ toκ hϖ H).thick n)))) :=
    fun hh => hUV (TopologicalSpace.Opens.mem_sup.mpr hh)
  have kU : ((C p 𝔛 O κ toκ hϖ H).f n).base ((C p 𝔛 O κ toκ hϖ H).xU n) ∈
        PrimeSpectrum.basicOpen (MvPolynomial.CrossingQuotient.U (((p : ℕ) : O) ^ ((C p 𝔛 O κ toκ hϖ H).thick n))) ↔
      MvPolynomial.CrossingQuotient.U (((p : ℕ) : O) ^ ((C p 𝔛 O κ toκ hϖ H).thick n)) ∉
        (((C p 𝔛 O κ toκ hϖ H).f n).base ((C p 𝔛 O κ toκ hϖ H).xU n)).asIdeal :=
    PrimeSpectrum.mem_basicOpen _ _
  have kV : ((C p 𝔛 O κ toκ hϖ H).f n).base ((C p 𝔛 O κ toκ hϖ H).xU n) ∈
        PrimeSpectrum.basicOpen (MvPolynomial.CrossingQuotient.V (((p : ℕ) : O) ^ ((C p 𝔛 O κ toκ hϖ H).thick n))) ↔
      MvPolynomial.CrossingQuotient.V (((p : ℕ) : O) ^ ((C p 𝔛 O κ toκ hϖ H).thick n)) ∉
        (((C p 𝔛 O κ toκ hϖ H).f n).base ((C p 𝔛 O κ toκ hϖ H).xU n)).asIdeal :=
    PrimeSpectrum.mem_basicOpen _ _
  have hU1 : MvPolynomial.CrossingQuotient.U (((p : ℕ) : O) ^ ((C p 𝔛 O κ toκ hϖ H).thick n)) ∈
      (((C p 𝔛 O κ toκ hϖ H).f n).base ((C p 𝔛 O κ toκ hϖ H).xU n)).asIdeal :=
    not_not.mp fun hn => hUV' (Or.inl (kU.mpr hn))
  have hV1 : MvPolynomial.CrossingQuotient.V (((p : ℕ) : O) ^ ((C p 𝔛 O κ toκ hϖ H).thick n)) ∈
      (((C p 𝔛 O κ toκ hϖ H).f n).base ((C p 𝔛 O κ toκ hϖ H).xU n)).asIdeal :=
    not_not.mp fun hn => hUV' (Or.inr (kV.mpr hn))
  refine MvPolynomial.CrossingQuotient.Resolution.eq_vertexPt_of_mem ((p : ℕ) : O) ((C p 𝔛 O κ toκ hϖ H).thick n) (IsLocalRing.maximalIdeal O) (p_mem_maximalIdeal p O hϖ)
    ((C p 𝔛 O κ toκ hϖ H).one_le_thick n) hU1 hV1 ?_
  intro w hw
  have hw0 : toκ w = 0 := by
    rw [hϖ, Ideal.mem_span_singleton] at hw
    obtain ⟨c, rfl⟩ := hw
    rw [map_mul, map_natCast, CharP.cast_eq_zero, zero_mul]
  have hover : ((C p 𝔛 O κ toκ hϖ H).σ n).base (((C p 𝔛 O κ toκ hϖ H).f n).base ((C p 𝔛 O κ toκ hϖ H).xU n)) = (πX p O).base ((C p 𝔛 O κ toκ hϖ H).x n) := by
    have h := congr($((C p 𝔛 O κ toκ hϖ H).f_over n).base ((C p 𝔛 O κ toκ hϖ H).xU n))
    simp only [Scheme.Hom.comp_base, TopCat.comp_app] at h
    exact h
  have hx : (πX p O).base ((C p 𝔛 O κ toκ hϖ H).x n) =
      (Spec.map (CommRingCat.ofHom toκ)).base
        ((pullback.snd (DRModel.toBase p) (Spec.map (CommRingCat.ofHom (algebraMap ℤ κ)))).base
          ((pullback.fst (𝔛.compInf κ) (𝔛.compZero κ) ≫ 𝔛.compInf κ).base n)) := by
    have h := congr($(bc_snd p O κ toκ).base ((pullback.fst (𝔛.compInf κ) (𝔛.compZero κ) ≫ 𝔛.compInf κ).base n))
    simp only [Scheme.Hom.comp_base, TopCat.comp_app] at h
    exact h
  change w ∈ (PrimeSpectrum.comap (algebraMap O (MvPolynomial.CrossingQuotient O (((p : ℕ) : O) ^ ((C p 𝔛 O κ toκ hϖ H).thick n))))
    (((C p 𝔛 O κ toκ hϖ H).f n).base ((C p 𝔛 O κ toκ hϖ H).xU n))).asIdeal
  have hσ : PrimeSpectrum.comap (algebraMap O (MvPolynomial.CrossingQuotient O (((p : ℕ) : O) ^ ((C p 𝔛 O κ toκ hϖ H).thick n)))) (((C p 𝔛 O κ toκ hϖ H).f n).base ((C p 𝔛 O κ toκ hϖ H).xU n)) =
      ((C p 𝔛 O κ toκ hϖ H).σ n).base (((C p 𝔛 O κ toκ hϖ H).f n).base ((C p 𝔛 O κ toκ hϖ H).xU n)) := rfl
  rw [hσ, hover, hx]
  change w ∈ Ideal.comap toκ _
  rw [Ideal.mem_comap, hw0]
  exact Ideal.zero_mem _

def oRes (n : V3Glue.Site.Node p 𝔛 κ) (d : Fin (width p 𝔛 O κ toκ hϖ H n)) : (C p 𝔛 O κ toκ hϖ H).Res n :=
  MvPolynomial.CrossingQuotient.Resolution.origin ((p : ℕ) : O) ((C p 𝔛 O κ toκ hϖ H).thick n) (IsLocalRing.maximalIdeal O) (p_mem_maximalIdeal p O hϖ) d

theorem hoRes : ∀ (n : V3Glue.Site.Node p 𝔛 κ) (d : Fin (width p 𝔛 O κ toκ hϖ H n)), (C p 𝔛 O κ toκ hϖ H).ρ n (oRes p 𝔛 O κ toκ hϖ H n d) = (C p 𝔛 O κ toκ hϖ H).vertex n := by
  intro n d
  show ((C p 𝔛 O κ toκ hϖ H).ρ n).base _ = _
  rw [vertex_eq p 𝔛 O κ toκ hϖ H n]
  exact MvPolynomial.CrossingQuotient.Resolution.toCrossing_origin ((p : ℕ) : O) ((C p 𝔛 O κ toκ hϖ H).thick n) (IsLocalRing.maximalIdeal O) (p_mem_maximalIdeal p O hϖ) d

def gRes (n : V3Glue.Site.Node p 𝔛 κ) (k : Fin (width p 𝔛 O κ toκ hϖ H n - 1)) : (C p 𝔛 O κ toκ hϖ H).Res n :=
  MvPolynomial.CrossingQuotient.Resolution.lineUGen ((p : ℕ) : O) ((C p 𝔛 O κ toκ hϖ H).thick n) (IsLocalRing.maximalIdeal O) (p_mem_maximalIdeal p O hϖ)
    ⟨(k : ℕ), by have hk := k.2; dsimp only [width] at hk; omega⟩

theorem hgRes : ∀ (n : V3Glue.Site.Node p 𝔛 κ) (k : Fin (width p 𝔛 O κ toκ hϖ H n - 1)), (C p 𝔛 O κ toκ hϖ H).ρ n (gRes p 𝔛 O κ toκ hϖ H n k) = (C p 𝔛 O κ toκ hϖ H).vertex n := by
  intro n k
  show ((C p 𝔛 O κ toκ hϖ H).ρ n).base _ = _
  rw [vertex_eq p 𝔛 O κ toκ hϖ H n]
  exact MvPolynomial.CrossingQuotient.Resolution.toCrossing_lineUGen_of_lt ((p : ℕ) : O) ((C p 𝔛 O κ toκ hϖ H).thick n) (IsLocalRing.maximalIdeal O) (p_mem_maximalIdeal p O hϖ) _
    (by have hk := k.2; dsimp only [width] at hk; simp only; omega)

variable (hξ : ∀ j, ξ p 𝔛 O κ toκ j ∈ (C p 𝔛 O κ toκ hϖ H).X0)

def comp : X0MqComponents (width p 𝔛 O κ toκ hϖ H) → (Y p 𝔛 O κ toκ hϖ H).IdealSheafData :=
  (C p 𝔛 O κ toκ hϖ H).compG (hRF p 𝔛 O κ toκ hϖ H) (gRes p 𝔛 O κ toκ hϖ H) (hgRes p 𝔛 O κ toκ hϖ H) (ξ p 𝔛 O κ toκ) hξ

def η : X0MqComponents (width p 𝔛 O κ toκ hϖ H) → Y p 𝔛 O κ toκ hϖ H :=
  (C p 𝔛 O κ toκ hϖ H).ηG (hRF p 𝔛 O κ toκ hϖ H) (gRes p 𝔛 O κ toκ hϖ H) (hgRes p 𝔛 O κ toκ hϖ H) (ξ p 𝔛 O κ toκ) hξ

def edgePt : (n : V3Glue.Site.Node p 𝔛 κ) → Fin (width p 𝔛 O κ toκ hϖ H n) → Y p 𝔛 O κ toκ hϖ H :=
  (C p 𝔛 O κ toκ hϖ H).edgePt' (hRF p 𝔛 O κ toκ hϖ H) (oRes p 𝔛 O κ toκ hϖ H) (hoRes p 𝔛 O κ toκ hϖ H)

theorem comp_def (v) : comp p 𝔛 O κ toκ hϖ H hξ v =
    (C p 𝔛 O κ toκ hϖ H).compG (hRF p 𝔛 O κ toκ hϖ H) (gRes p 𝔛 O κ toκ hϖ H) (hgRes p 𝔛 O κ toκ hϖ H) (ξ p 𝔛 O κ toκ) hξ v := rfl
theorem η_def (v) : η p 𝔛 O κ toκ hϖ H hξ v =
    (C p 𝔛 O κ toκ hϖ H).ηG (hRF p 𝔛 O κ toκ hϖ H) (gRes p 𝔛 O κ toκ hϖ H) (hgRes p 𝔛 O κ toκ hϖ H) (ξ p 𝔛 O κ toκ) hξ v := rfl
theorem edgePt_def (n) (d) : edgePt p 𝔛 O κ toκ hϖ H n d =
    (C p 𝔛 O κ toκ hϖ H).edgePt' (hRF p 𝔛 O κ toκ hϖ H) (oRes p 𝔛 O κ toκ hϖ H) (hoRes p 𝔛 O κ toκ hϖ H) n d := rfl

theorem chainPos'_eq (n : V3Glue.Site.Node p 𝔛 κ) (d : ℕ) :
    (C p 𝔛 O κ toκ hϖ H).chainPos' n d = DRResolvedModelPackage.chainPos (width p 𝔛 O κ toκ hϖ H) n d := rfl

end V3Asm

end