English
Naturality of glueData ι in Shrink setting (variant).
Русский
Естественная совместимость glueData ι в настройке Shrink (вариант).
LaTeX
$$$$ {i j : Shrink.{u} J} (f : ↓i ⟶ ↓j) : F.map f \circ (glueData F).ι j = (glueData F).ι i $$$$
Lean4
theorem ι_eq_ι_iff {i j : J} {xi : F.obj i} {xj : F.obj j} :
(colimit.ι F i).base xi = (colimit.ι F j).base xj ↔
∃ k fi fj, ∃ (x : F.obj k), (F.map fi).base x = xi ∧ (F.map fj).base x = xj :=
by
constructor; swap
· rintro ⟨k, fi, fj, x, rfl, rfl⟩; simp only [← Scheme.comp_base_apply, colimit.w]
obtain ⟨i, rfl⟩ := (equivShrink J).symm.surjective i
obtain ⟨j, rfl⟩ := (equivShrink J).symm.surjective j
rw [← ((isColimit F).coconePointUniqueUpToIso (colimit.isColimit F)).inv.isOpenEmbedding.injective.eq_iff]
simp only [Limits.colimit, ← Scheme.comp_base_apply, colimit.comp_coconePointUniqueUpToIso_inv, cocone,
glueDataι_naturality]
refine ?_ ∘ ((glueData F).ι_eq_iff _ _ _ _).mp
dsimp only [GlueData.Rel]
rintro ⟨x, rfl, rfl⟩
obtain ⟨⟨k, ki, kj⟩, y, hy : (F.map ki).base y = ((glueData F).f i j).base x⟩ := mem_iSup.mp x.2
refine ⟨k, ki, kj, y, hy, ?_⟩
obtain ⟨k, rfl⟩ := (equivShrink J).symm.surjective k
apply ((glueData F).ι _).isOpenEmbedding.injective
simp only [← Scheme.comp_base_apply, Category.assoc, GlueData.glue_condition]
trans ((glueData F).ι k).base y
· simp [← glueDataι_naturality F kj]; rfl
· simp [← glueDataι_naturality F ki, ← hy]; rfl
