Lean4
/-- (Implementation detail)
The glue data associated to a locally directed diagram.
One usually does not want to use this directly, and instead use the generic `colimit` API.
-/
def glueData : Scheme.GlueData where
J := Shrink.{u} J
U j := F.obj ↓j
V ij := V F (↓ij.1) ↓ij.2
f i j := Scheme.Opens.ι _
f_id i := V_self F ↓i ▸ (Scheme.topIso _).isIso_hom
f_hasPullback := inferInstance
f_open := inferInstance
t i j := t F (↓i) ↓j
t_id i := t_id F ↓i
t' i j
k :=
pullback.lift
(IsOpenImmersion.lift (V F (↓j) ↓k).ι (pullback.fst _ _ ≫ tAux F (↓i) ↓j)
(by
rintro _ ⟨x, rfl⟩
obtain ⟨l, fi, fj, fk, α, z, hα, hα₁, hα₂, rfl⟩ := exists_of_pullback_V_V F x
rw [← Scheme.comp_base_apply, reassoc_of% hα₁, homOfLE_tAux F (↓i) (↓j) fi fj, Iso.hom_inv_id_assoc,
Scheme.Opens.range_ι, SetLike.mem_coe]
exact TopologicalSpace.Opens.mem_iSup.mpr ⟨⟨l, fj, fk⟩, ⟨z, rfl⟩⟩))
(pullback.fst _ _ ≫ t F _ _) (by simp [t])
t_fac i j k := pullback.lift_snd _ _ _
cocycle i j
k := by
refine Scheme.hom_ext_of_forall _ _ fun x ↦ ?_
have := exists_of_pullback_V_V F x
obtain ⟨l, fi, fj, fk, α, z, hα, hα₁, hα₂, e⟩ := this
refine ⟨α.opensRange, ⟨_, e⟩, ?_⟩
rw [← cancel_mono (pullback.snd _ _), ← cancel_mono (Scheme.Opens.ι _)]
simp only [t, Category.assoc, limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app, limit.lift_π_assoc,
cospan_left, IsOpenImmersion.lift_fac, Category.id_comp]
rw [IsOpenImmersion.comp_lift_assoc]
simp only [limit.lift_π_assoc, PullbackCone.mk_pt, cospan_left, PullbackCone.mk_π_app]
rw [← cancel_epi α.isoOpensRange.hom]
simp_rw [Scheme.Hom.isoOpensRange_hom_ι_assoc, IsOpenImmersion.comp_lift_assoc]
simp only [reassoc_of% hα₁, homOfLE_tAux F _ _ fi fj, Iso.hom_inv_id_assoc, reassoc_of% hα₂]
generalize_proofs _ h₁
have :
IsOpenImmersion.lift (V F (↓j) ↓k).ι (F.map fj) h₁ =
(F.map fj).isoOpensRange.hom ≫ (F.obj ↓j).homOfLE (le_iSup_of_le ⟨l, fj, fk⟩ le_rfl) :=
by
rw [← cancel_mono (Scheme.Opens.ι _), Category.assoc, IsOpenImmersion.lift_fac, ← Iso.inv_comp_eq,
Scheme.Hom.isoOpensRange_inv_comp]
exact (Scheme.homOfLE_ι _ _).symm
simp_rw [this, Category.assoc, homOfLE_tAux F _ _ fj fk, Iso.hom_inv_id_assoc]
generalize_proofs h₂
have :
IsOpenImmersion.lift (V F (↓k) ↓i).ι (F.map fk) h₂ =
(F.map fk).isoOpensRange.hom ≫ (F.obj ↓k).homOfLE (le_iSup_of_le ⟨l, fk, fi⟩ le_rfl) :=
by
rw [← cancel_mono (Scheme.Opens.ι _), Category.assoc, IsOpenImmersion.lift_fac, ← Iso.inv_comp_eq,
Scheme.Hom.isoOpensRange_inv_comp]
exact (Scheme.homOfLE_ι _ _).symm
simp_rw [this, Category.assoc, homOfLE_tAux F _ _ fk fi, Iso.hom_inv_id_assoc, ← Iso.inv_comp_eq,
Scheme.Hom.isoOpensRange_inv_comp]
exact (Scheme.homOfLE_ι _ _).symm
