AlgebraicGeometry.Scheme.Modules.exists_nonempty_iso_pullback_of_nonempty_iso_pullback_of_isDirectLimit
Lean source · full declarationtheorem exists_nonempty_iso_pullback_of_nonempty_iso_pullback_of_isDirectLimit
{ι : Type u} [Preorder ι] [Nonempty ι] [IsDirected ι (· ≤ ·)]
{G : ι → Type u} [∀ i, CommRing (G i)] (φ : ∀ i j : ι, i ≤ j → G i →+* G j)
[DirectedSystem G fun i j h => ⇑(φ i j h)]
{R : Type u} [CommRing R] (g : ∀ i, G i →+* R)
(hR : IsDirectLimit (fun i j h => ⇑(φ i j h)) fun i => ⇑(g i))
(i : ι) {X : Scheme.{u}} (fX : X ⟶ Spec (CommRingCat.of (G i))) [QuasiCompact fX]
[QuasiSeparated fX]
(𝓛₁ 𝓛₂ : X.Modules) (h₁ : Scheme.Modules.IsInvertible 𝓛₁) (h₂ : Scheme.Modules.IsInvertible 𝓛₂)
(hiso : Nonempty
((Scheme.Modules.pullback (Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (g i))))).obj
𝓛₁ ≅
(Scheme.Modules.pullback (Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (g i))))).obj
𝓛₂)) :
∃ (j : ι) (hij : i ≤ j), Nonempty
((Scheme.Modules.pullback (Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (φ i j
hij))))).obj 𝓛₁ ≅
(Scheme.Modules.pullback (Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (φ i j
hij))))).obj 𝓛₂) := by
classical
have : CompactSpace ↥(Spec (CommRingCat.of (G i))) := (inferInstance : CompactSpace
(PrimeSpectrum (G i)))
have : CompactSpace ↥X := QuasiCompact.compactSpace_of_compactSpace fX
have : QuasiSeparatedSpace ↥X := (quasiSeparated_iff_quasiSeparatedSpace fX).mp inferInstance
let J : Type u := {j : ι // i ≤ j}
have : Nonempty J := ⟨⟨i, le_rfl⟩⟩
have : IsDirected J (· ≤ ·) := ⟨fun a b => by
obtain ⟨c, hac, hbc⟩ := directed_of (· ≤ ·) a.1 b.1
exact ⟨⟨c, a.2.trans hac⟩, hac, hbc⟩⟩
let algK : ∀ j : J, Algebra (G i) (G j.1) := fun j => (φ i j.1 j.2).toAlgebra
let algR : Algebra (G i) R := (g i).toAlgebra
let algGR : ∀ j : J, Algebra (G j.1) R := fun j => (g j.1).toAlgebra
have hST : ∀ j : J, IsScalarTower (G i) (G j.1) R := fun j =>
IsScalarTower.of_algebraMap_eq (fun r => (IsDirectLimit.compatibility (f := fun i j h => ⇑(φ i
j h))
(g := fun i => ⇑(g i)) i j.1 j.2 r).symm)
let f' : ∀ j k : J, j ≤ k → G j.1 →ₐ[G i] G k.1 := fun j k h =>
{ toRingHom := φ j.1 k.1 h
commutes' := fun r => DirectedSystem.map_map (f := fun i j h => ⇑(φ i j h)) j.2 h r }
have hDS : DirectedSystem (fun j : J => G j.1) (fun j k h => ⇑(f' j k h)) :=
⟨fun j x => DirectedSystem.map_self (f := fun i j h => ⇑(φ i j h)) x,
fun k j l hlj hjk x => DirectedSystem.map_map (f := fun i j h => ⇑(φ i j h)) hlj hjk x⟩
have hR' : IsDirectLimit (fun j k h => ⇑(f' j k h)) (fun j : J => ⇑(algebraMap (G j.1) R)) := by
refine ⟨fun x => ?_, fun j k x y hxy => ?_, fun j k h x => ?_⟩
· obtain ⟨i', y, hy⟩ := hR.surj x
obtain ⟨k, hik, hi'k⟩ := directed_of (· ≤ ·) i i'
exact ⟨⟨k, hik⟩, φ i' k hi'k y, by rw [← hy]; exact hR.compatibility i' k hi'k y⟩
· obtain ⟨l, hjl, hkl, e⟩ := hR.inj j.1 k.1 x y hxy
exact ⟨⟨l, j.2.trans hjl⟩, hjl, hkl, e⟩
· exact hR.compatibility j.1 k.1 h x
let instK : ∀ V : X.Opens, Algebra (G i) Γ(X, V) := fun V =>
Scheme.TwoAffineOpenCover.algebraOfHom fX V
let instKR : ∀ W : (Limits.pullback fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) R)))).Opens,
Algebra (G i) Γ(Limits.pullback fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) R))), W) :=
fun W =>
Scheme.TwoAffineOpenCover.algebraOfHom
(Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) R))) ≫ fX) W
obtain ⟨εR, hεaff, hε1, -, hε2⟩ :=
AlgebraicGeometry.exists_algEquiv_sections_pullback_fst_preimage_tensor_of_isAffineOpen (G i)
fX R
have hDL : ∀ V : X.Opens, ∃ _ : DirectedSystem (fun j : J => G j.1 ⊗[G i] Γ(X, V))
(fun j k h => ⇑(Algebra.TensorProduct.map (f' j k h) (AlgHom.id (G i) Γ(X, V)))),
IsDirectLimit (fun j k h => ⇑(Algebra.TensorProduct.map (f' j k h) (AlgHom.id (G i) Γ(X, V))))
(fun j : J => ⇑(Algebra.TensorProduct.map (IsScalarTower.toAlgHom (G i) (G j.1) R)
(AlgHom.id (G i) Γ(X, V)))) := fun V =>
Algebra.TensorProduct.isDirectLimit_map_of_isDirectLimit (G i) (fun j : J => G j.1) f' R hR'
Γ(X, V)
choose hDSv hDLv using hDL
let γR : ∀ (V : X.Opens) (hV : IsAffineOpen V),
Γ(Limits.pullback fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) R))),
(Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) R)))) ⁻¹ᵁ V) ≃ₐ[G i]
R ⊗[G i] Γ(X, V) := fun V hV => (εR V hV).trans (Algebra.TensorProduct.comm (G i) Γ(X, V) R)
have γR1 : ∀ (V : X.Opens) (hV : IsAffineOpen V) (s : Γ(X, V)),
γR V hV ((Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) R)))).app V
s) =
(1 : R) ⊗ₜ[G i] s := by
intro V hV s
change Algebra.TensorProduct.comm (G i) _ R (εR V hV _) = _
erw [hε1 V hV s]
exact Algebra.TensorProduct.comm_tmul _ _ _
have γR2 : ∀ (V V' : X.Opens) (hV : IsAffineOpen V) (hV' : IsAffineOpen V') (hle : V' ≤ V)
(s : Γ(Limits.pullback fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) R))),
(Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) R)))) ⁻¹ᵁ V)),
Algebra.TensorProduct.map (AlgHom.id (G i) R) (Scheme.TwoAffineOpenCover.restrictAlgHom fX
hle) (γR V hV s) =
γR V' hV' ((Limits.pullback fX (Spec.map (CommRingCat.ofHom (algebraMap (G i)
R)))).presheaf.map
(homOfLE ((Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (algebraMap (G i)
R)))).preimage_mono
hle)).op s) := by
intro V V' hV hV' hle s
change Algebra.TensorProduct.map _ _ (Algebra.TensorProduct.comm (G i) _ R (εR V hV s)) =
Algebra.TensorProduct.comm (G i) _ R (εR V' hV' _)
rw [← hε2 V V' hV hV' hle s]
exact (Algebra.TensorProduct.comm_comp_map_apply _ _ _).symm
obtain ⟨n, U, hUaff, hUcov, fa, fb, ha, hb⟩ := h₁.exists_fin_affine_cover_isFrameOn₂ h₂
have hiso' : Nonempty
((Scheme.Modules.pullback (Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (algebraMap (G
i) R))))).obj 𝓛₁ ≅
(Scheme.Modules.pullback (Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (algebraMap (G
i) R))))).obj 𝓛₂) :=
hiso
obtain ⟨u, hu, hcoc⟩ := exists_units_of_iso
(Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) R)))) ha hb hiso'.some
have hWc : ∀ k l : Fin n, IsCompact ((U k ⊓ U l : X.Opens) : Set X) := fun k l =>
QuasiSeparatedSpace.inter_isCompact _ _ (U k).isOpen (hUaff k).isCompact (U l).isOpen (hUaff
l).isCompact
have hP := fun k l : Fin n => (isCompact_iff_finite_and_eq_biUnion_affineOpens (U := U k ⊓ U
l)).1 (hWc k l)
choose S hSfin hSeq using hP
have hSle : ∀ (k l : Fin n) (W : ↥(S k l)), ((W : X.affineOpens) : X.Opens) ≤ U k ⊓ U l := fun k
l W => by
rw [hSeq k l]; exact le_iSup₂ (f := fun (i : X.affineOpens) (_ : i ∈ S k l) => (i : X.Opens))
W.1 W.2
have : ∀ k l : Fin n, Finite ↥(S k l) := fun k l => (hSfin k l).to_subtype
have s1 := fun k => (hDLv (U k)).surj (γR (U k) (hUaff k) (u k))
choose j₁ uT huT using s1
have s2 := fun k => (hDLv (U k)).surj (γR (U k) (hUaff k) ↑(hu k).unit⁻¹)
choose j₂ wT hwT using s2
obtain ⟨j₀, hj₁, hj₂⟩ := exists_ge₂ j₁ j₂
obtain ⟨uT0, huT0⟩ : ∃ uT0 : ∀ k, G j₀.1 ⊗[G i] Γ(X, U k), ∀ k,
Algebra.TensorProduct.map (IsScalarTower.toAlgHom (G i) (G j₀.1) R) (AlgHom.id (G i) Γ(X, U
k)) (uT0 k) =
γR (U k) (hUaff k) (u k) :=
⟨fun k => Algebra.TensorProduct.map (f' (j₁ k) j₀ (hj₁ k)) (AlgHom.id (G i) Γ(X, U k)) (uT k),
fun k => by
rw [← huT k]; exact (hDLv (U k)).compatibility (j₁ k) j₀ (hj₁ k) (uT k)⟩
obtain ⟨wT0, hwT0⟩ : ∃ wT0 : ∀ k, G j₀.1 ⊗[G i] Γ(X, U k), ∀ k,
Algebra.TensorProduct.map (IsScalarTower.toAlgHom (G i) (G j₀.1) R) (AlgHom.id (G i) Γ(X, U
k)) (wT0 k) =
γR (U k) (hUaff k) ↑(hu k).unit⁻¹ :=
⟨fun k => Algebra.TensorProduct.map (f' (j₂ k) j₀ (hj₂ k)) (AlgHom.id (G i) Γ(X, U k)) (wT k),
fun k => by
rw [← hwT k]; exact (hDLv (U k)).compatibility (j₂ k) j₀ (hj₂ k) (wT k)⟩
have s3 : ∀ k, ∃ (l : J) (h h' : j₀ ≤ l),
Algebra.TensorProduct.map (f' j₀ l h) (AlgHom.id (G i) Γ(X, U k)) (uT0 k * wT0 k) =
Algebra.TensorProduct.map (f' j₀ l h') (AlgHom.id (G i) Γ(X, U k)) 1 := fun k =>
(hDLv (U k)).inj j₀ j₀ (uT0 k * wT0 k) 1 (by
rw [map_mul, huT0, hwT0, map_one, ← map_mul, IsUnit.mul_val_inv, map_one])
choose j₃ hj₃ hj₃' huw using s3
have s4 : ∀ (k l : Fin n) (W : ↥(S k l)), ∃ (m : J) (h h' : j₀ ≤ m),
Algebra.TensorProduct.map (f' j₀ m h) (AlgHom.id (G i) Γ(X, W))
(((1 : G j₀.1) ⊗ₜ[G i] X.presheaf.map (homOfLE (hSle k l W)).op (IsFrameOn.trans ha k l)) *
Algebra.TensorProduct.map (AlgHom.id (G i) (G j₀.1))
(Scheme.TwoAffineOpenCover.restrictAlgHom fX ((hSle k l W).trans inf_le_left)) (uT0 k))
=
Algebra.TensorProduct.map (f' j₀ m h') (AlgHom.id (G i) Γ(X, W))
(Algebra.TensorProduct.map (AlgHom.id (G i) (G j₀.1))
(Scheme.TwoAffineOpenCover.restrictAlgHom fX ((hSle k l W).trans inf_le_right)) (uT0 l)
*
((1 : G j₀.1) ⊗ₜ[G i] X.presheaf.map (homOfLE (hSle k l W)).op (IsFrameOn.trans hb k l)))
:= by
intro k l W
apply (hDLv W).inj j₀ j₀
have hWaff : IsAffineOpen ((W : X.affineOpens) : X.Opens) := W.1.2
have hγa := γR1 ((W : X.affineOpens) : X.Opens) hWaff
(X.presheaf.map (homOfLE (hSle k l W)).op (IsFrameOn.trans ha k l))
have hγb := γR1 ((W : X.affineOpens) : X.Opens) hWaff
(X.presheaf.map (homOfLE (hSle k l W)).op (IsFrameOn.trans hb k l))
have hγk := γR2 (U k) ((W : X.affineOpens) : X.Opens) (hUaff k) hWaff
((hSle k l W).trans inf_le_left) (u k)
have hγl := γR2 (U l) ((W : X.affineOpens) : X.Opens) (hUaff l) hWaff
((hSle k l W).trans inf_le_right) (u l)
have hc := cocycle_res _ (hSle k l W) (IsFrameOn.trans ha k l) (IsFrameOn.trans hb k l) (u k)
(u l) (hcoc k l)
have hc' := congrArg (γR ((W : X.affineOpens) : X.Opens) hWaff) hc
rw [map_mul, map_mul, hγa, hγb, ← hγk, ← hγl, ← huT0, ← huT0,
← map_swap, ← map_swap] at hc'
rw [map_mul, map_mul, map_one_tmul, map_one_tmul]
exact hc'
choose j₄ hj₄ hj₄' hz using s4
obtain ⟨m₁, hm₃, hm₄⟩ := exists_ge₂ j₃ (fun p : Σ k : Fin n, Σ l : Fin n, ↥(S k l) => j₄ p.1
p.2.1 p.2.2)
obtain ⟨js, h0s, h1s⟩ := directed_of (· ≤ ·) j₀ m₁
let instKs : ∀ W : (Limits.pullback fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) (G
js.1))))).Opens,
Algebra (G i) Γ(Limits.pullback fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) (G
js.1)))), W) := fun W =>
Scheme.TwoAffineOpenCover.algebraOfHom
(Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) (G js.1)))) ≫ fX) W
obtain ⟨εs, hεsaff, hεs1, -, hεs2⟩ :=
AlgebraicGeometry.exists_algEquiv_sections_pullback_fst_preimage_tensor_of_isAffineOpen (G i)
fX (G js.1)
let γs : ∀ (V : X.Opens) (hV : IsAffineOpen V),
Γ(Limits.pullback fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) (G js.1)))),
(Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) (G js.1))))) ⁻¹ᵁ V)
≃ₐ[G i]
G js.1 ⊗[G i] Γ(X, V) := fun V hV => (εs V hV).trans (Algebra.TensorProduct.comm (G i) Γ(X,
V) (G js.1))
have γs1 : ∀ (V : X.Opens) (hV : IsAffineOpen V) (s : Γ(X, V)),
γs V hV ((Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) (G
js.1))))).app V s) =
(1 : G js.1) ⊗ₜ[G i] s := by
intro V hV s
change Algebra.TensorProduct.comm (G i) _ (G js.1) (εs V hV _) = _
erw [hεs1 V hV s]
exact Algebra.TensorProduct.comm_tmul _ _ _
have γs2 : ∀ (V V' : X.Opens) (hV : IsAffineOpen V) (hV' : IsAffineOpen V') (hle : V' ≤ V)
(s : Γ(Limits.pullback fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) (G js.1)))),
(Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) (G js.1))))) ⁻¹ᵁ V)),
Algebra.TensorProduct.map (AlgHom.id (G i) (G js.1))
(Scheme.TwoAffineOpenCover.restrictAlgHom fX hle)
(γs V hV s) =
γs V' hV' ((Limits.pullback fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) (G
js.1))))).presheaf.map
(homOfLE ((Limits.pullback.fst fX
(Spec.map (CommRingCat.ofHom (algebraMap (G i) (G js.1))))).preimage_mono hle)).op s)
:= by
intro V V' hV hV' hle s
change Algebra.TensorProduct.map _ _ (Algebra.TensorProduct.comm (G i) _ (G js.1) (εs V hV s)) =
Algebra.TensorProduct.comm (G i) _ (G js.1) (εs V' hV' _)
rw [← hεs2 V V' hV hV' hle s]
exact (Algebra.TensorProduct.comm_comp_map_apply _ _ _).symm
let v : ∀ k, Γ(Limits.pullback fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) (G js.1)))),
(Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) (G js.1))))) ⁻¹ᵁ U k)
:= fun k =>
(γs (U k) (hUaff k)).symm
(Algebra.TensorProduct.map (f' j₀ js h0s) (AlgHom.id (G i) Γ(X, U k)) (uT0 k))
have hγv : ∀ k, γs (U k) (hUaff k) (v k) =
Algebra.TensorProduct.map (f' j₀ js h0s) (AlgHom.id (G i) Γ(X, U k)) (uT0 k) := fun k =>
(γs (U k) (hUaff k)).apply_symm_apply _
have hPuw : ∀ k, Algebra.TensorProduct.map (f' j₀ js h0s) (AlgHom.id (G i) Γ(X, U k)) (uT0 k) *
Algebra.TensorProduct.map (f' j₀ js h0s) (AlgHom.id (G i) Γ(X, U k)) (wT0 k) = 1 := fun k =>
by
have e := congrArg (Algebra.TensorProduct.map (f' (j₃ k) js ((hm₃ k).trans h1s)) (AlgHom.id (G
i) Γ(X, U k)))
(huw k)
rw [(hDSv (U k)).map_map, (hDSv (U k)).map_map, map_one] at e
rw [← map_mul]
exact e
have hv : ∀ k, IsUnit (v k) := fun k => by
have e : v k * (γs (U k) (hUaff k)).symm
(Algebra.TensorProduct.map (f' j₀ js h0s) (AlgHom.id (G i) Γ(X, U k)) (wT0 k)) = 1 := by
apply (γs (U k) (hUaff k)).injective
rw [map_mul, hγv, AlgEquiv.apply_symm_apply, map_one]
exact hPuw k
exact IsUnit.of_mul_eq_one _ e
have hcocs : ∀ k l,
(Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) (G js.1))))).appInf (U
k) (U l)
(IsFrameOn.trans ha k l) *
(Limits.pullback fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) (G js.1))))).presheaf.map
(homOfLE (inf_le_left :
(Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) (G js.1))))) ⁻¹ᵁ
U k ⊓
(Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) (G js.1))))) ⁻¹ᵁ
U l ≤ _)).op
(v k) =
(Limits.pullback fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) (G js.1))))).presheaf.map
(homOfLE (inf_le_right :
(Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) (G js.1))))) ⁻¹ᵁ
U k ⊓
(Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) (G js.1))))) ⁻¹ᵁ
U l ≤ _)).op
(v l) *
(Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) (G js.1))))).appInf
(U k) (U l)
(IsFrameOn.trans hb k l) := by
intro k l
apply TopCat.Sheaf.eq_of_locally_eq'
(Limits.pullback fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) (G js.1))))).sheaf
(fun W : ↥(S k l) => (Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (algebraMap (G i)
(G js.1))))) ⁻¹ᵁ
((W : X.affineOpens) : X.Opens))
_ (fun W => homOfLE ((Limits.pullback.fst fX
(Spec.map (CommRingCat.ofHom (algebraMap (G i) (G js.1))))).preimage_mono_inf (hSle k l W)))
· intro x hx
have hx' : (Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) (G
js.1))))) x ∈
(⨆ W ∈ S k l, (W : X.Opens)) := by rw [← hSeq k l]; exact hx
obtain ⟨W, hW⟩ := Opens.mem_iSup.1 hx'
obtain ⟨hWS, hxW⟩ := Opens.mem_iSup.1 hW
exact Opens.mem_iSup.2 ⟨⟨W, hWS⟩, hxW⟩
· intro W
change (Limits.pullback fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) (G
js.1))))).presheaf.map
(homOfLE ((Limits.pullback.fst fX
(Spec.map (CommRingCat.ofHom (algebraMap (G i) (G js.1))))).preimage_mono_inf (hSle k l
W))).op (_ * _) =
(Limits.pullback fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) (G js.1))))).presheaf.map
(homOfLE ((Limits.pullback.fst fX
(Spec.map (CommRingCat.ofHom (algebraMap (G i) (G js.1))))).preimage_mono_inf (hSle k l
W))).op (_ * _)
rw [map_mul, map_mul, appInf_res _ _ _ _ (hSle k l W), appInf_res _ _ _ _ (hSle k l W),
res_res, res_res]
have hWaff : IsAffineOpen ((W : X.affineOpens) : X.Opens) := W.1.2
have hγa := γs1 ((W : X.affineOpens) : X.Opens) hWaff
(X.presheaf.map (homOfLE (hSle k l W)).op (IsFrameOn.trans ha k l))
have hγb := γs1 ((W : X.affineOpens) : X.Opens) hWaff
(X.presheaf.map (homOfLE (hSle k l W)).op (IsFrameOn.trans hb k l))
have hγk := γs2 (U k) ((W : X.affineOpens) : X.Opens) (hUaff k) hWaff
((hSle k l W).trans inf_le_left) (v k)
have hγl := γs2 (U l) ((W : X.affineOpens) : X.Opens) (hUaff l) hWaff
((hSle k l W).trans inf_le_right) (v l)
apply (γs ((W : X.affineOpens) : X.Opens) hWaff).injective
rw [map_mul, map_mul, hγa, hγb, ← hγk, ← hγl, hγv, hγv, ← map_swap, ← map_swap,
← map_one_tmul (f' j₀ js h0s) (X.presheaf.map (homOfLE (hSle k l W)).op (IsFrameOn.trans ha
k l)),
← map_one_tmul (f' j₀ js h0s) (X.presheaf.map (homOfLE (hSle k l W)).op (IsFrameOn.trans hb
k l)),
← map_mul, ← map_mul]
have e := congrArg (Algebra.TensorProduct.map (f' (j₄ k l W) js ((hm₄ ⟨k, l, W⟩).trans h1s))
(AlgHom.id (G i) Γ(X, ((W : X.affineOpens) : X.Opens)))) (hz k l W)
rw [(hDSv _).map_map, (hDSv _).map_map] at e
exact e
have key := nonempty_iso_of_units
(Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (algebraMap (G i) (G js.1))))) (ι :=
ULift.{u} (Fin n))
(U := fun k => U k.down)
(by rw [← hUcov, iSup_ulift]) (a := fun k => fa k.down) (b := fun k => fb k.down)
(fun k => ha k.down) (fun k => hb k.down) (fun k => v k.down) (fun k => hv k.down)
(fun k l => hcocs k.down l.down)
exact ⟨js.1, js.2, key⟩