English
Naturality of glueData ι with respect to morphisms in Shrink.
Русский
Единство естественности glueData ι по отношению к отображениям в Shrink.
LaTeX
$$$$ F.map f \circ (glueData F).ι j = (glueData F).ι i $$$$
Lean4
theorem glueDataι_naturality {i j : Shrink.{u} J} (f : ↓i ⟶ ↓j) : F.map f ≫ (glueData F).ι j = (glueData F).ι i :=
by
have : IsIso (V F (↓i) ↓j).ι :=
by
have : V F (↓i) ↓j = ⊤ := top_le_iff.mp (le_iSup_of_le ⟨_, 𝟙 i, f⟩ (by simp [Scheme.Hom.opensRange_of_isIso]))
exact this ▸ (topIso _).isIso_hom
have : t F (↓i) ↓j ≫ (V F (↓j) ↓i).ι ≫ _ = (V F (↓i) ↓j).ι ≫ _ := (glueData F).glue_condition i j
simp only [t, IsOpenImmersion.lift_fac_assoc] at this
rw [← cancel_epi (V F (↓i) ↓j).ι, ← this, ← Category.assoc, ←
(Iso.eq_inv_comp _).mp (homOfLE_tAux F (↓i) (↓j) (𝟙 i) f), ← Category.assoc, ← Category.assoc, Category.assoc]
convert Category.id_comp _
rw [← cancel_mono (Opens.ι _)]
simp [V, InducedCategory.category, Shrink.instCategoryShrink]
