ProjectivePresentation.lean

structure ProjPresentation (M : X.Modules) (f : X ⟶ Spec (.of R)) (N : ℕ) where
  /-- The chosen global sections whose restrictions give the coordinate frames. -/
  σ : Fin (N + 1) → Γ(M, ⊤)
  /-- The morphism to projective space presented by the sections `σ`. -/
  toProj : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)
  /-- The projective-space morphism lies over the specified map `f`. -/
  toProj_π : toProj ≫ ProjSpace.π R N = f
  /-- Each `σ i` restricts to a frame on every open contained in the preimage of the `i`th
      standard chart. -/
  frame : ∀ (i : Fin (N + 1)) (V : X.Opens),
    V ≤ toProj ⁻¹ᵁ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)
        (MvPolynomial.X i) →
    Function.Bijective fun g : Γ(X, V) => g • (M.presheaf.map (homOfLE (le_top : V ≤ ⊤)).op (σ
        i) : Γ(M, V))
  /-- Pulling back a coordinate ratio on the `i`th chart expresses `σ j` as that ratio times `σ
      i`. -/
  app_ratio_smul : ∀ i j : Fin (N + 1),
    (toProj.app (Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R)
        (MvPolynomial.X i))
        (Proj.awayToSection _ (MvPolynomial.X i) (ProjSpace.ratio R N i j))) •
        M.presheaf.map (homOfLE (le_top : toProj ⁻¹ᵁ
          Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R) (MvPolynomial.X i)
              ≤ ⊤)).op (σ i)
      = M.presheaf.map (homOfLE (le_top : toProj ⁻¹ᵁ
          Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) R) (MvPolynomial.X i)
              ≤ ⊤)).op (σ j)

def FiniteBySections (M : X.Modules) (f : X ⟶ Spec (.of R)) : Prop

def ClosedImmersionBySections (M : X.Modules) (f : X ⟶ Spec (.of R)) : Prop

def awayZeroEval :
    HomogeneousLocalization.Away (MvPolynomial.homogeneousSubmodule (Fin 1) R) (X 0 :
        MvPolynomial (Fin 1) R) →+* R

def pointOfProjZero : Spec (.of R) ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin 1) R)

theorem pointOfProjZero_π : pointOfProjZero R ≫ π R 0 = 𝟙 _

theorem pointOfProjZero_preimage_basicOpen :
    pointOfProjZero R ⁻¹ᵁ Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin 1) R) (X 0) = ⊤

def Scheme.Modules.unitOne (X : Scheme.{u}) :
    Γ((SheafOfModules.unit X.ringCatSheaf : X.Modules), (⊤ : X.Opens))

def Scheme.Modules.ProjPresentation.unitSpec :
    Scheme.Modules.ProjPresentation (SheafOfModules.unit (Spec (.of R)).ringCatSheaf : (Spec
        (.of R)).Modules)
      (𝟙 (Spec (.of R))) 0 where
  σ := fun _ => Scheme.Modules.unitOne (Spec (.of R))
  toProj := ProjSpace.pointOfProjZero R
  toProj_π := ProjSpace.pointOfProjZero_π R
  frame := fun i V _ => by
    have h : (Scheme.Modules.presheaf (SheafOfModules.unit (Spec (.of R)).ringCatSheaf : (Spec
        (.of R)).Modules)).map
        (homOfLE (le_top : V ≤ ⊤)).op (Scheme.Modules.unitOne (Spec (.of R)))
        = (show Γ(Spec (.of R), V) from 1) := by
      change ((Spec (.of R)).ringCatSheaf.obj.map (homOfLE (le_top : V ≤ ⊤)).op).hom 1 = 1
      exact map_one _
    rw [h]
    change Function.Bijective fun g : Γ(Spec (.of R), V) => g * 1
    simp only [mul_one]
    exact Function.bijective_id
  app_ratio_smul := fun i j => by
    have hi : i = 0 := Fin.eq_zero i
    have hj : j = 0 := Fin.eq_zero j
    subst hi hj
    rw [ProjSpace.ratio_self, map_one, map_one, one_smul]