Scheme_TwoAffineOpenCover_exists_sectionsOf_overlap_linearEquiv_baseChange_of_isInvertible.lean

theorem op_hom_eq {U V : Y.Opens} (i j : op U ⟶ op V) : i = j

theorem map_map (M : Y.Modules) {U V W : Y.Opens} (i : op U ⟶ op V) (j : op V ⟶ op W) (x : Γ(M,
    U)) :
    M.presheaf.map j (M.presheaf.map i x) = M.presheaf.map (i ≫ j) x

theorem map_irrel (M : Y.Modules) {U V : Y.Opens} (i j : op U ⟶ op V) (x : Γ(M, U)) :
    M.presheaf.map i x = M.presheaf.map j x

theorem ring_map_map {U V W : Y.Opens} (i : op U ⟶ op V) (j : op V ⟶ op W) (x : Y.presheaf.obj
    (op U)) :
    Y.presheaf.map j (Y.presheaf.map i x) = Y.presheaf.map (i ≫ j) x

theorem ring_map_irrel {U V : Y.Opens} (i j : op U ⟶ op V) (x : Y.presheaf.obj (op U)) :
    Y.presheaf.map i x = Y.presheaf.map j x

theorem P2mWs11Span.span_res_eq_top
    {X : Scheme.{u}} (M : X.Modules)
    (htriv : ∀ x : X, ∃ (W : X.Opens), x ∈ W ∧
      Nonempty ((Scheme.Modules.pullback W.ι).obj M ≅ SheafOfModules.unit W.toScheme.ringCatSheaf))
    {U V : X.Opens} (hU : IsAffineOpen U) (hV : IsAffineOpen V) (hVU : V ≤ U) :
    Submodule.span Γ(X, V) (Set.range (fun y : Γ(M, U) => M.presheaf.map (homOfLE hVU).op y)) =
      ⊤ := by
  classical
  set S : Submodule Γ(X, V) Γ(M, V) :=
    Submodule.span Γ(X, V) (Set.range (fun y : Γ(M, U) => M.presheaf.map (homOfLE hVU).op y))
      with hS
  rw [Submodule.eq_top_iff']
  intro s
  have key : ∀ f : Γ(X, U), X.basicOpen f ≤ V →
      ∃ N : ℕ, (X.presheaf.map (homOfLE hVU).op f) ^ N • s ∈ S := by
    intro f hfV
    set g : Γ(X, V) := X.presheaf.map (homOfLE hVU).op f with hg
    obtain ⟨n, y, hy⟩ :=
      (Scheme.Modules.isLocalization_basicOpen_of_locallyTrivial M htriv ⟨U, hU⟩ f).1
        (M.presheaf.map (homOfLE hfV).op s)
    have hgf : X.basicOpen g ≤ X.basicOpen f := by
      rw [hg, Scheme.basicOpen_res]; exact inf_le_right
    set t : Γ(M, V) := g ^ n • s - M.presheaf.map (homOfLE hVU).op y with ht
    have htf : M.presheaf.map (homOfLE hfV).op t = 0 := by
      rw [ht, map_sub, Scheme.Modules.map_smul, map_pow, map_map, hg, ring_map_map, sub_eq_zero,
        ring_map_irrel ((homOfLE hVU).op ≫ (homOfLE hfV).op) (homOfLE (X.basicOpen_le f)).op,
        map_irrel M ((homOfLE hVU).op ≫ (homOfLE hfV).op) (homOfLE (X.basicOpen_le f)).op, hy,
          map_pow]
    have htg : M.presheaf.map (homOfLE (X.basicOpen_le g)).op t = 0 := by
      rw [map_irrel M (homOfLE (X.basicOpen_le g)).op ((homOfLE hfV).op ≫ (homOfLE hgf).op),
        ← map_map, htf, map_zero]
    obtain ⟨m, hm⟩ :=
      (Scheme.Modules.isLocalization_basicOpen_of_locallyTrivial M htriv ⟨V, hV⟩ g).2 t htg
    refine ⟨m + n, ?_⟩
    have : g ^ (m + n) • s = g ^ m • M.presheaf.map (homOfLE hVU).op y := by
      rw [pow_add, mul_smul, ← sub_eq_zero, ← smul_sub, ← ht]; exact hm
    rw [this]
    exact S.smul_mem _ (Submodule.subset_span ⟨y, rfl⟩)
  suffices h1 : (1 : Γ(X, V)) ∈ S.colon {s} by
    simpa using Submodule.mem_colon_singleton.mp h1
  by_contra h1
  have hI : S.colon {s} ≠ ⊤ := fun h => h1 (h ▸ Submodule.mem_top)
  obtain ⟨𝔪, h𝔪, hI𝔪⟩ := Ideal.exists_le_maximal _ hI
  let p : PrimeSpectrum Γ(X, V) := ⟨𝔪, h𝔪.isPrime⟩
  have hxV : hV.fromSpec p ∈ V := by
    have h : hV.fromSpec p ∈ Set.range (hV.fromSpec : _ → X) := ⟨p, rfl⟩
    rw [hV.range_fromSpec] at h
    exact h
  obtain ⟨f, hfV, hxf⟩ := hU.exists_basicOpen_le ⟨_, hxV⟩ (hVU hxV)
  obtain ⟨N, hN⟩ := key f hfV
  set g : Γ(X, V) := X.presheaf.map (homOfLE hVU).op f with hg
  have hgI : g ^ N ∈ S.colon {s} := Submodule.mem_colon_singleton.mpr hN
  have hg𝔪 : g ∈ 𝔪 := h𝔪.isPrime.mem_of_pow_mem N (hI𝔪 hgI)
  have hxg : hV.fromSpec p ∈ X.basicOpen g := by
    rw [hg, Scheme.basicOpen_res]; exact ⟨hxV, hxf⟩
  have : p ∈ hV.fromSpec ⁻¹ᵁ X.basicOpen g := hxg
  rw [hV.fromSpec_preimage_basicOpen] at this
  exact (PrimeSpectrum.mem_basicOpen g p).mp this hg𝔪

theorem algebraMap_basicOpen_apply {U : X.Opens} (f : Γ(X, U)) (x : Γ(X, U)) :
    algebraMap Γ(X, U) Γ(X, X.basicOpen f) x = X.presheaf.map (homOfLE (X.basicOpen_le f)).op x

theorem exists_pow_mul_eq_algebraMap {U V : X.Opens} (hU : IsAffineOpen U) (hV : IsAffineOpen V)
    (hVU : V ≤ U) [Algebra Γ(X, U) Γ(X, V)]
    (halg : ∀ a, algebraMap Γ(X, U) Γ(X, V) a = X.presheaf.map (homOfLE hVU).op a)
    (h : Γ(X, U)) (hDV : X.basicOpen h ≤ V) (b : Γ(X, V)) :
    ∃ (n : ℕ) (a : Γ(X, U)), algebraMap Γ(X, U) Γ(X, V) h ^ n * b = algebraMap Γ(X, U) Γ(X, V) a

theorem algebraMap_tmul_eq_one_tmul_smul {A B P : Type*} [CommRing A] [CommRing B] [Algebra A B]
    [AddCommGroup P] [Module A P] (a : A) (p : P) :
    (algebraMap A B a) ⊗ₜ[A] p = (1 : B) ⊗ₜ[A] (a • p)

theorem algebraMap_pow_smul_one_tmul {A B P : Type*} [CommRing A] [CommRing B] [Algebra A B]
    [AddCommGroup P] [Module A P] (a : A) (n : ℕ) (p : P) :
    (algebraMap A B a) ^ n • ((1 : B) ⊗ₜ[A] p) = (1 : B) ⊗ₜ[A] (a ^ n • p)

theorem exists_baseChange_equiv (M : X.Modules)
    (htriv : ∀ x : X, ∃ (W : X.Opens), x ∈ W ∧
      Nonempty ((Scheme.Modules.pullback W.ι).obj M ≅ SheafOfModules.unit W.toScheme.ringCatSheaf))
    {U V : X.Opens} (hU : IsAffineOpen U) (hV : IsAffineOpen V) (hVU : V ≤ U)
    [alg : Algebra Γ(X, U) Γ(X, V)]
    (halg : ∀ a, algebraMap Γ(X, U) Γ(X, V) a = X.presheaf.map (homOfLE hVU).op a) :
    ∃ e : Γ(X, V) ⊗[Γ(X, U)] Γ(M, U) ≃ₗ[Γ(X, V)] Γ(M, V),
      ∀ m : Γ(M, U), e ((1 : Γ(X, V)) ⊗ₜ[Γ(X, U)] m) = M.presheaf.map (homOfLE hVU).op m

theorem exists_sectionsOf_overlap_linearEquiv_baseChange_of_isInvertible
    {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
    (M : X.Modules) (hM : Scheme.Modules.IsInvertible M) :
    letI : Algebra (𝒱.cover c).A0 (𝒱.cover c).A01 := (𝒱.cover c).ρ0.toRingHom.toAlgebra
    letI : Algebra (𝒱.cover c).A1 (𝒱.cover c).A01 := (𝒱.cover c).ρ1.toRingHom.toAlgebra
    ∃ (rbc0 : (𝒱.cover c).A01 ⊗[(𝒱.cover c).A0] (𝒱.sectionsOf c M).M0 ≃ₗ[(𝒱.cover c).A01]
                (𝒱.sectionsOf c M).M01)
      (rbc1 : (𝒱.cover c).A01 ⊗[(𝒱.cover c).A1] (𝒱.sectionsOf c M).M1 ≃ₗ[(𝒱.cover c).A01]
                (𝒱.sectionsOf c M).M01),
      (∀ m, rbc0 ((1 : (𝒱.cover c).A01) ⊗ₜ[(𝒱.cover c).A0] m) = (𝒱.sectionsOf c M).r0 m) ∧
      (∀ m, rbc1 ((1 : (𝒱.cover c).A01) ⊗ₜ[(𝒱.cover c).A1] m) = (𝒱.sectionsOf c M).r1 m) := by
  let alg0 : Algebra (𝒱.cover c).A0 (𝒱.cover c).A01 := (𝒱.cover c).ρ0.toRingHom.toAlgebra
  let alg1 : Algebra (𝒱.cover c).A1 (𝒱.cover c).A01 := (𝒱.cover c).ρ1.toRingHom.toAlgebra
  obtain ⟨e0, he0⟩ := P2mWs11Span.exists_baseChange_equiv (alg := alg0) M hM.exists_trivialization
    𝒱.isAffineOpen_U0 𝒱.isAffineOpen_inf inf_le_left (fun _ => rfl)
  obtain ⟨e1, he1⟩ := P2mWs11Span.exists_baseChange_equiv (alg := alg1) M hM.exists_trivialization
    𝒱.isAffineOpen_U1 𝒱.isAffineOpen_inf inf_le_right (fun _ => rfl)
  exact ⟨e0, e1, he0, he1⟩