Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_ModularCurve_ResolvedModelSite.lean

definition module

Crossing charts and glue data for resolved DR models

Fix a prime p, a package \mathfrak X of Deligne–Rapoport model data for level p, a discrete valuation domain O and an algebraically closed field \kappa of characteristic p. Here X_O is the base change pullback (DRModel.toBase p) (Spec.map (algebraMap ℤ O)) of the model to \operatorname{Spec} O, the index type Node is the set of points of the fibre product of the two component maps \mathfrak X.\mathrm{compInf}\,\kappa and \mathfrak X.\mathrm{compZero}\,\kappa, and xpt sends a node to its image in X_O along a given base-change morphism bc. Three predicates record the geometric input, each kept as a hypothesis. HasOrientedCrossingCharts asserts that every node n admits e\ge 1, an open U\ni \mathrm{xpt}(n) and a morphism f\colon U\to crossingScheme ((p:O)^e), the spectrum of O[X_0,X_1]/(X_0X_1-p^e), compatible over \operatorname{Spec} O with the projection of U, such that both distinguished elements U and V lie in the prime f(y) exactly when y\mapsto \mathrm{xpt}(n); at points over \mathrm{xpt}(n) the stalk map is flat, carries the maximal ideal onto the maximal ideal and induces an isomorphism of residue fields; and the chart is oriented, in that V\in f(y) holds precisely for y in the image of the \infty-component and U\in f(y) precisely for y in the image of the 0-component. ModelHyps bundles five properties of the toric resolutions \rho_e: \rho_e restricts to an isomorphism over D(U)\cup D(V) for e>0, is proper, the composite to \operatorname{Spec} O is flat, each resolution is locally Noetherian, and the preimage of the vertex locus has empty interior. EtNbhd asserts the spreading-out statement that a morphism locally of finite presentation which at a point is flat, carries maximal ideal to maximal ideal and induces a residue-field isomorphism is étale on some open neighbourhood of that point.

From these, ChartData packages one chosen chart per node, chartData extracts it, and rawChartInputOfDR, chartInputOfDR assemble a RawChartInput, respectively ChartInput, on X_O indexed by the nodes, with S_n the crossing scheme, V_c the union of the two basic opens, thickness e_n, resolution \rho_{e_n}, and base \operatorname{Spec} O; finite presentation of the charts comes from a lemma proved here, that a morphism locally of finite type into a locally Noetherian scheme is locally of finite presentation. The V3Asm section fixes a ring map \mathrm{to}\kappa\colon O\to\kappa, takes bc to be the induced base-change morphism (with its compatibilities with both projections), and bundles the above into a single hypothesis structure SiteHyps. Under these and the hypothesis that the maximal ideal of O is generated by p, it defines the glued scheme Y with its morphisms to X_O and to \operatorname{Spec} O, the chart isomorphisms onto the preimages of the chart opens, the widths e_n, the two points \xi_0,\xi_1 given by the generic points of the two components of the special fibre, the resolution points oRes (origins) and gRes (generic points of the exceptional lines) together with proofs that both lie over the vertex, the vertex identification vertex_eq with the explicit vertex prime, and finally the ideal-sheaf components comp, their generic points η and the edge points edgePt, plus the identification of the glue's chain position with the chain position used by DRResolvedModelPackage.

Relation to Mathlib

The morphism classes and scheme-theoretic notions used (LocallyOfFiniteType, LocallyOfFinitePresentation, Etale, Flat, IsProper, IsLocallyNoetherian, Scheme.IdealSheafData) are Mathlib's; the crossing scheme, its toric resolutions, the chart and glue inputs, and the model packages are the project's own notions.

Where it is used

These definitions form the site layer producing a regular resolved model over O of the Deligne–Rapoport model of X_0(p), whose special fibre consists of the two components meeting in chains of rational curves at the supersingular points; the resulting DRResolvedModelPackage is the geometric input for the analysis of the Jacobian's Néron model and component group used on the Frey–Serre–Ribet side of the argument.

References

  1. P. Deligne and M. Rapoport, Les schémas de modules de courbes elliptiques, in: Modular Functions of One Variable II, Lecture Notes in Mathematics 349, Springer, 1973, 143–316
  2. B. Mazur, Modular curves and the Eisenstein ideal, Publications Mathématiques de l'IHÉS 47 (1977), 33–186
  3. H. Darmon, F. Diamond and R. Taylor, Fermat's Last Theorem, in: Current Developments in Mathematics 1995, International Press, 1995, 1–154

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

Source file: Definitions/Def_ModularCurve_ResolvedModelSite.lean

Imports

Imported by

  • no other definition module

Declarations

Source

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

Statements phrased using this module (12)