English
Opens and images commute under gluing data: the opens functor interacts compatibly with pullbacks and pushes forward across glue maps.
Русский
Открытые множества и их образы корректно склеиваются в данных склейки: функтор opens совместим с вытаскиванием по обратной проекции и переносами через glue-маршруты.
LaTeX
$$$ opensImagePreimageMap \\text{ commutes with glue-data }$$
Lean4
theorem opensImagePreimageMap_app' (i j k : D.J) (U : Opens (D.U i).carrier) :
∃ eq,
D.opensImagePreimageMap i j U ≫ (D.f j k).c.app _ =
((π₁ j, i, k) ≫ D.t j i ≫ D.f i j).c.app (op U) ≫
(π₂⁻¹ j, i, k) (unop _) ≫ (D.V (j, k)).presheaf.map (eqToHom eq) :=
by
constructor
· delta opensImagePreimageMap
simp_rw [Category.assoc]
rw [(D.f j k).c.naturality, f_invApp_f_app_assoc]
· erw [← (D.V (j, k)).presheaf.map_comp]
· simp_rw [← Category.assoc]
erw [← comp_c_app, ← comp_c_app]
· simp_rw [Category.assoc]
dsimp only [Functor.op, unop_op, Quiver.Hom.unop_op]
rw [eqToHom_map (Opens.map _), eqToHom_op, eqToHom_trans]
congr
