GeneratedAlgebraLocalization.lean

theorem isLocalizationAway_restrict_of_eq
    {B B' : Type u} [CommRing B] [CommRing B'] (q : B →+* B')
    (C C' : Subring B) (D D' : Subring B') (hC : C = C') (hD : D = D')
    (hq : ∀ x ∈ C, q x ∈ D) (hq' : ∀ x ∈ C', q x ∈ D')
    (a : B) (ha : a ∈ C) (ha' : a ∈ C')
    (hlocal : let : Algebra C' D' := (q.restrict C' D' hq').toAlgebra
      IsLocalization.Away (⟨a, ha'⟩ : C') D') :
    let : Algebra C D := (q.restrict C D hq).toAlgebra
    IsLocalization.Away (⟨a, ha⟩ : C) D := by
  subst C'
  subst D'
  exact hlocal

theorem isLocalization_basicOpen (U : X.AffineZariskiSite) (r : Γ(X, U.1)) :
    let q := (presheaf α N.toSubmodule).map (homOfLE (X.basicOpen_le r)).op
    let : Algebra
        ((presheaf α N.toSubmodule).obj (op U.1))
        ((presheaf α N.toSubmodule).obj (op (X.basicOpen r))) := q.hom.toAlgebra
    IsLocalization.Away ((structureMap α N.toSubmodule).app (op U.1) r)
      ((presheaf α N.toSubmodule).obj (op (X.basicOpen r))) := by
  let R : CommRingCat.{u} := Γ(X, U.1)
  let R' : CommRingCat.{u} := Γ(X, X.basicOpen r)
  let B : CommRingCat.{u} := A.obj.obj (op U.1)
  let B' : CommRingCat.{u} := A.obj.obj (op (X.basicOpen r))
  let i : op U.1 ⟶ op (X.basicOpen r) := (homOfLE (X.basicOpen_le r)).op
  let σ : R →+* R' := (X.presheaf.map i).hom
  let ι : R →+* B := (α.hom.app (op U.1)).hom
  let ι' : R' →+* B' := (α.hom.app (op (X.basicOpen r))).hom
  let q : B →+* B' := (A.obj.map i).hom
  let : Algebra R R' := σ.toAlgebra
  let : Algebra R B := ι.toAlgebra
  let : Algebra R' B' := ι'.toAlgebra
  let : Algebra R B' := (ι'.comp σ).toAlgebra
  have : IsScalarTower R R' B' := IsScalarTower.of_algebraMap_eq (fun x => rfl)
  have hcomm (x : R) : q (ι x) = ι' (σ x) :=
    (congrArg (fun k : R ⟶ B' => k x) (α.hom.naturality i)).symm
  let f : B →ₐ[R] B' := { q with commutes' := hcomm }
  let P : Submodule R B := N.toSubmodule.obj (op U.1)
  let P' : Submodule R' B' := N.toSubmodule.obj (op (X.basicOpen r))
  have hf : ∀ x ∈ P, f x ∈ P' := by
    intro x hx
    exact N.toSubmodule.map_mem i hx
  have : IsLocalization.Away r R' := U.2.isLocalization_basicOpen r
  have : IsLocalizedModule.Away r f.toLinearMap :=
    Modules.isLocalizedModule_basicOpen_of_isQuasicoherent_of_qcqs
      (RelativeSpec.underlyingModule α) U.2.isCompact U.2.isQuasiSeparated r
  have : IsLocalizedModule.Away r
      (f.toLinearMap.restrict (p := P) (q := P'.restrictScalars R) hf) :=
    Modules.isLocalizedModule_basicOpen_of_isQuasicoherent_of_qcqs
      (show X.Modules from N.toSheafOfModules) U.2.isCompact U.2.isQuasiSeparated r
  have hC : sectionSubring α N.toSubmodule (op U.1) =
      (Algebra.adjoin R (P : Set B)).toSubring :=
    sectionSubring_eq_adjoin α N.toSubmodule (op U.1)
  have hD : sectionSubring α N.toSubmodule (op (X.basicOpen r)) =
      (Algebra.adjoin R' (P' : Set B')).toSubring :=
    sectionSubring_eq_adjoin α N.toSubmodule (op (X.basicOpen r))
  let g : Algebra.adjoin R (P : Set B) →ₐ[R] Algebra.adjoin R' (P' : Set B') :=
    Submodule.adjoinRestrictionTo R' f P P' hf
  have hg : ∀ x ∈ (Algebra.adjoin R (P : Set B)).toSubring,
      q x ∈ (Algebra.adjoin R' (P' : Set B')).toSubring := by
    intro x hx
    exact (g ⟨x, hx⟩).property
  change
    let : Algebra
        (sectionSubring α N.toSubmodule (op U.1))
        (sectionSubring α N.toSubmodule (op (X.basicOpen r))) :=
      (q.restrict (sectionSubring α N.toSubmodule (op U.1))
        (sectionSubring α N.toSubmodule (op (X.basicOpen r)))
        (restriction_mem α N.toSubmodule i)).toAlgebra
    IsLocalization.Away
      ((ι.codRestrict (sectionSubring α N.toSubmodule (op U.1))
        (fun x => Subring.subset_closure (Or.inl ⟨x, rfl⟩))) r)
      (sectionSubring α N.toSubmodule (op (X.basicOpen r)))
  exact isLocalizationAway_restrict_of_eq q
    (sectionSubring α N.toSubmodule (op U.1))
    (Algebra.adjoin R (P : Set B)).toSubring
    (sectionSubring α N.toSubmodule (op (X.basicOpen r)))
    (Algebra.adjoin R' (P' : Set B')).toSubring hC hD
    (restriction_mem α N.toSubmodule i) hg (ι r)
    (Subring.subset_closure (Or.inl ⟨r, rfl⟩))
    ((Algebra.adjoin R (P : Set B)).algebraMap_mem r)
    (Submodule.isLocalizationAway_adjoinRestrictionTo R' f P P' hf r)

theorem coequifibered : (affineStructureMap α N.toSubmodule).Coequifibered

def gluingData : (AffineZariskiSite.directedCover X).RelativeGluingData

instance gluingData_isLocallyDirected :
    ((gluingData α N).functor ⋙ Scheme.forget).IsLocallyDirected

def scheme : Scheme.{u}

def toBase : scheme α N ⟶ X