English
Compatibility of map composition with pullback components: the c-apps intertwine with pushforwards and pullbacks along f and g.
Русский
Совместимость композиции отображений с компонентами $c$ при вытягивании по $f$ и $g$.
LaTeX
$$$(F.map (f \\to g)).c.app U = (F.map g).c.app U \\;\\cdot\\; (\\text{pushforward}).map (F.map f).c \\cdot (\\text{pushforwardEq}).hom.app U$$$
Lean4
/-- The red and the blue arrows in  commute. -/
theorem opensImagePreimageMap_app (i j k : D.J) (U : Opens (D.U i).carrier) :
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 (opensImagePreimageMap_app' D i j k U).choose) :=
(opensImagePreimageMap_app' D i j k U).choose_spec