opensImagePreimageMap_app — Mathlib

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 ![this diagram](https://i.imgur.com/mBzV1Rx.png) 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

Похожие утверждения