AlgebraicGeometry.Scheme.Modules.exists_isInvertible_nonempty_pullback_iso_of_isInvertible_of_isDirectLimit
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicGeometry.Scheme.Modules
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleDirectLimit
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.TopologicalSpace
open _root_.Opposite
universe u
open
_root_.AlgebraicCurves.Geometry.Sheaves.Proofs.InvertibleDirectLimit.AlgebraicGeometry.LimitPic
_root_.AlgebraicGeometry.Scheme.Modules in
Lean source · full declarationtheorem exists_isInvertible_nonempty_pullback_iso_of_isInvertible_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]
(𝓛 : (Limits.pullback fX (Spec.map (CommRingCat.ofHom (g i)))).Modules) (h𝓛 :
Scheme.Modules.IsInvertible 𝓛) :
∃ (j : ι) (hij : i ≤ j) (𝓛j : (Limits.pullback fX (Spec.map (CommRingCat.ofHom (φ i j
hij)))).Modules),
Scheme.Modules.IsInvertible 𝓛j ∧
∀ cX : Limits.pullback fX (Spec.map (CommRingCat.ofHom (g i))) ⟶
Limits.pullback fX (Spec.map (CommRingCat.ofHom (φ i j hij))),
cX ≫ Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (φ i j hij))) =
Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (g i))) →
cX ≫ Limits.pullback.snd fX (Spec.map (CommRingCat.ofHom (φ i j hij))) =
Limits.pullback.snd fX (Spec.map (CommRingCat.ofHom (g i))) ≫ Spec.map (CommRingCat.ofHom
(g j)) →
Nonempty ((Scheme.Modules.pullback cX).obj 𝓛j ≅ 𝓛) := by
classical
have hcompat : ∀ (a b : ι) (h : a ≤ b), (g b).comp (φ a b h) = g a := fun a b h =>
RingHom.ext fun x => hR.compatibility a b h x
have hφφ : ∀ (a b c : ι) (hab : a ≤ b) (hbc : b ≤ c), (φ b c hbc).comp (φ a b hab) = φ a c
(hab.trans hbc) :=
fun a b c hab hbc => RingHom.ext fun x => DirectedSystem.map_map' (f := φ) hab hbc x
have hSpec : ∀ (a b : ι) (h : a ≤ b),
Spec.map (CommRingCat.ofHom (g b)) ≫ Spec.map (CommRingCat.ofHom (φ a b h)) = Spec.map
(CommRingCat.ofHom (g a)) :=
fun a b h => by rw [← Spec.map_comp, ← CommRingCat.ofHom_comp, hcompat]
have hSpecφ : ∀ (a b c : ι) (hab : a ≤ b) (hbc : b ≤ c),
Spec.map (CommRingCat.ofHom (φ b c hbc)) ≫ Spec.map (CommRingCat.ofHom (φ a b hab)) =
Spec.map (CommRingCat.ofHom (φ a c (hab.trans hbc))) :=
fun a b c hab hbc => by rw [← Spec.map_comp, ← CommRingCat.ofHom_comp, hφφ]
obtain ⟨j₀, hij₀, n, W, hW, HW⟩ :=
IsInvertible.exists_isAffineOpen_isFrameOn_preimage_of_isDirectLimit
φ g hR i fX 𝓛 h𝓛
let XR := Limits.pullback fX (Spec.map (CommRingCat.ofHom (g i)))
let prR := Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (g i)))
let sndR := Limits.pullback.snd fX (Spec.map (CommRingCat.ofHom (g i)))
let X₀ := Limits.pullback fX (Spec.map (CommRingCat.ofHom (φ i j₀ hij₀)))
let pr₀ := Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (φ i j₀ hij₀)))
let f₀ : X₀ ⟶ Spec (CommRingCat.of (G j₀)) := Limits.pullback.snd fX (Spec.map (CommRingCat.ofHom
(φ i j₀ hij₀)))
let c₀ : XR ⟶ X₀ := Limits.pullback.lift prR (sndR ≫ Spec.map (CommRingCat.ofHom (g j₀)))
(by rw [Category.assoc, hSpec, Limits.pullback.condition])
have hc₀₁ : c₀ ≫ pr₀ = prR := Limits.pullback.lift_fst _ _ _
have hc₀₂ : c₀ ≫ f₀ = sndR ≫ Spec.map (CommRingCat.ofHom (g j₀)) := Limits.pullback.lift_snd _ _ _
obtain ⟨hcov₀, s, hs⟩ := HW c₀ hc₀₁ hc₀₂
have : QuasiCompact f₀ := inferInstance
have : QuasiSeparated f₀ := inferInstance
let X'R := Limits.pullback f₀ (Spec.map (CommRingCat.ofHom (g j₀)))
let pr'R := Limits.pullback.fst f₀ (Spec.map (CommRingCat.ofHom (g j₀)))
let snd'R := Limits.pullback.snd f₀ (Spec.map (CommRingCat.ofHom (g j₀)))
let eh : X'R ⟶ XR := Limits.pullback.lift (pr'R ≫ pr₀) snd'R (by
rw [Category.assoc, Limits.pullback.condition, ← Category.assoc, Limits.pullback.condition,
Category.assoc, hSpec])
let ei : XR ⟶ X'R := Limits.pullback.lift c₀ sndR hc₀₂
have eh₁ : eh ≫ prR = pr'R ≫ pr₀ := Limits.pullback.lift_fst _ _ _
have eh₂ : eh ≫ sndR = snd'R := Limits.pullback.lift_snd _ _ _
have ei₁ : ei ≫ pr'R = c₀ := Limits.pullback.lift_fst _ _ _
have ei₂ : ei ≫ snd'R = sndR := Limits.pullback.lift_snd _ _ _
have heh_c₀ : eh ≫ c₀ = pr'R := by
apply Limits.pullback.hom_ext
· rw [Category.assoc, hc₀₁, eh₁]
· rw [Category.assoc, hc₀₂, ← Category.assoc, eh₂, Limits.pullback.condition]
let e : X'R ≅ XR :=
{ hom := eh, inv := ei
hom_inv_id := by
apply Limits.pullback.hom_ext
· rw [Category.assoc, ei₁, heh_c₀, Category.id_comp]
· rw [Category.assoc, ei₂, eh₂, Category.id_comp]
inv_hom_id := by
apply Limits.pullback.hom_ext
· rw [Category.assoc, eh₁, ← Category.assoc, ei₁, hc₀₁, Category.id_comp]
· rw [Category.assoc, eh₂, ei₂, Category.id_comp] }
let 𝓛' : X'R.Modules := (Scheme.Modules.pullback e.hom).obj 𝓛
have h𝓛' : IsInvertible 𝓛' := h𝓛.pullback e.hom
have hO : ∀ k, pr'R ⁻¹ᵁ W k = e.hom ⁻¹ᵁ (c₀ ⁻¹ᵁ W k) := fun k => by
rw [← Scheme.Hom.comp_preimage]; exact congrArg (· ⁻¹ᵁ W k) heh_c₀.symm
let s' : ∀ k, Γ(𝓛', pr'R ⁻¹ᵁ W k) := fun k =>
𝓛'.presheaf.map (eqToHom (hO k)).op (pullbackLocalSection e.hom (s k))
have hs' : ∀ k, IsFrameOn (s' k) (pr'R ⁻¹ᵁ W k) := fun k =>
isFrameOn_cast (hO k) _ ((hs k).pullbackLocalSection e.hom)
obtain ⟨gc, hgc⟩ := exists_unitCocycle_of_frames' (fun k => pr'R ⁻¹ᵁ W k) 𝓛' s' hs'
have hW' : ∀ k, IsCompact ((W k : X₀.Opens) : Set X₀) := fun k => (hW k).isCompact
have hcov' : (⨆ k, pr'R ⁻¹ᵁ W k) = ⊤ := by
rw [show (fun k => pr'R ⁻¹ᵁ W k) = fun k => e.hom ⁻¹ᵁ (c₀ ⁻¹ᵁ W k) from funext hO,
← Scheme.Hom.preimage_iSup, hcov₀, Scheme.Hom.preimage_top]
obtain ⟨j, hj₀j, c, hcovj, Hc⟩ :=
AlgebraicGeometry.Scheme.Modules.UnitCocycle.exists_comap_eq_of_isDirectLimit φ g hR j₀ f₀ W
hW' hcov' gc
let X'j := Limits.pullback f₀ (Spec.map (CommRingCat.ofHom (φ j₀ j hj₀j)))
let pr'j := Limits.pullback.fst f₀ (Spec.map (CommRingCat.ofHom (φ j₀ j hj₀j)))
let snd'j := Limits.pullback.snd f₀ (Spec.map (CommRingCat.ofHom (φ j₀ j hj₀j)))
let cX' : X'R ⟶ X'j := Limits.pullback.lift pr'R (snd'R ≫ Spec.map (CommRingCat.ofHom (g j)))
(by rw [Category.assoc, hSpec, Limits.pullback.condition])
have hcX'₁ : cX' ≫ pr'j = pr'R := Limits.pullback.lift_fst _ _ _
have hcX'₂ : cX' ≫ snd'j = snd'R ≫ Spec.map (CommRingCat.ofHom (g j)) := Limits.pullback.lift_snd
_ _ _
have hV : ∀ k, cX' ⁻¹ᵁ (pr'j ⁻¹ᵁ W k) = pr'R ⁻¹ᵁ W k := fun k => by
rw [← Scheme.Hom.comp_preimage]; exact congrArg (· ⁻¹ᵁ W k) hcX'₁
let 𝓛'j : X'j.Modules := glueOfCocycle c
have h𝓛'j : IsInvertible 𝓛'j := AlgebraicGeometry.Scheme.Modules.isInvertible_glueOfCocycle hcovj
c
obtain ⟨iso₁⟩ : Nonempty ((Scheme.Modules.pullback cX').obj 𝓛'j ≅ 𝓛') := by
refine nonempty_pullback_glueOfCocycle_iso' cX' hcovj c (fun k => pr'R ⁻¹ᵁ W k) hV 𝓛' s' hs' ?_
intro a b hab
rw [← hgc a b]
congr 1
exact Hc cX' hcX'₁ hcX'₂ a b _
let Xj := Limits.pullback fX (Spec.map (CommRingCat.ofHom (φ i j (hij₀.trans hj₀j))))
let prj := Limits.pullback.fst fX (Spec.map (CommRingCat.ofHom (φ i j (hij₀.trans hj₀j))))
let sndj := Limits.pullback.snd fX (Spec.map (CommRingCat.ofHom (φ i j (hij₀.trans hj₀j))))
let d : Xj ⟶ X₀ := Limits.pullback.lift prj (sndj ≫ Spec.map (CommRingCat.ofHom (φ j₀ j hj₀j)))
(by rw [Category.assoc, hSpecφ, Limits.pullback.condition])
have hd₁ : d ≫ pr₀ = prj := Limits.pullback.lift_fst _ _ _
have hd₂ : d ≫ f₀ = sndj ≫ Spec.map (CommRingCat.ofHom (φ j₀ j hj₀j)) := Limits.pullback.lift_snd
_ _ _
let ejh : X'j ⟶ Xj := Limits.pullback.lift (pr'j ≫ pr₀) snd'j (by
rw [Category.assoc, Limits.pullback.condition, ← Category.assoc, Limits.pullback.condition,
Category.assoc, hSpecφ])
let eji : Xj ⟶ X'j := Limits.pullback.lift d sndj hd₂
have ejh₁ : ejh ≫ prj = pr'j ≫ pr₀ := Limits.pullback.lift_fst _ _ _
have ejh₂ : ejh ≫ sndj = snd'j := Limits.pullback.lift_snd _ _ _
have eji₁ : eji ≫ pr'j = d := Limits.pullback.lift_fst _ _ _
have eji₂ : eji ≫ snd'j = sndj := Limits.pullback.lift_snd _ _ _
have hejh_d : ejh ≫ d = pr'j := by
apply Limits.pullback.hom_ext
· rw [Category.assoc, hd₁, ejh₁]
· rw [Category.assoc, hd₂, ← Category.assoc, ejh₂, Limits.pullback.condition]
let ej : X'j ≅ Xj :=
{ hom := ejh, inv := eji
hom_inv_id := by
apply Limits.pullback.hom_ext
· rw [Category.assoc, eji₁, hejh_d, Category.id_comp]
· rw [Category.assoc, eji₂, ejh₂, Category.id_comp]
inv_hom_id := by
apply Limits.pullback.hom_ext
· rw [Category.assoc, ejh₁, ← Category.assoc, eji₁, hd₁, Category.id_comp]
· rw [Category.assoc, ejh₂, eji₂, Category.id_comp] }
let 𝓛j : Xj.Modules := (Scheme.Modules.pullback ej.inv).obj 𝓛'j
refine ⟨j, hij₀.trans hj₀j, 𝓛j, h𝓛'j.pullback ej.inv, fun cX h1 h2 => ?_⟩
have : Mono ej.hom := (Iso.isIso_hom ej).mono_of_iso
have hkey : cX ≫ ej.inv = e.inv ≫ cX' := by
rw [← cancel_mono ej.hom, Category.assoc, ej.inv_hom_id, Category.comp_id, Category.assoc]
apply Limits.pullback.hom_ext
· rw [h1, Category.assoc, Category.assoc, ejh₁, ← Category.assoc cX', hcX'₁]
change prR = e.inv ≫ pr'R ≫ pr₀
rw [← eh₁, ← Category.assoc, e.inv_hom_id, Category.id_comp]
· rw [h2, Category.assoc, Category.assoc, ejh₂, hcX'₂]
change sndR ≫ _ = e.inv ≫ snd'R ≫ _
rw [← eh₂, ← Category.assoc, ← Category.assoc, e.inv_hom_id, Category.id_comp]
refine ⟨(Scheme.Modules.pullbackComp cX ej.inv).app 𝓛'j ≪≫ (Scheme.Modules.pullbackCongr
hkey).app 𝓛'j ≪≫
((Scheme.Modules.pullbackComp e.inv cX').app 𝓛'j).symm ≪≫ (Scheme.Modules.pullback
e.inv).mapIso iso₁ ≪≫
(Scheme.Modules.pullbackComp e.inv e.hom).app 𝓛 ≪≫ (Scheme.Modules.pullbackCongr
e.inv_hom_id).app 𝓛 ≪≫
(Scheme.Modules.pullbackId XR).app 𝓛⟩