map_comp_c_app — Mathlib

English

The naturality of desc with respect to the left index j is preserved, i.e., the diagram commutes when applying maps along i.

Русский

Натуральность desc относительно левого индекса j сохраняется: диаграмма коммутирует при применении отображений по i.

LaTeX

$$$(colimitCocone F).ι.app j ≫ desc F s = s.ι.app j$$$

Lean4

@[simp]
theorem map_comp_c_app (F : J ⥤ PresheafedSpace.{_, _, v} C) {j₁ j₂ j₃} (f : j₁ ⟶ j₂) (g : j₂ ⟶ j₃) (U) :
    (F.map (f ≫ g)).c.app U =
      (F.map g).c.app U ≫
        ((pushforward C (F.map g).base).map (F.map f).c).app U ≫
          (pushforwardEq (congr_arg Hom.base (F.map_comp f g).symm) _).hom.app U :=
  by simp [PresheafedSpace.congr_app (F.map_comp f g)]

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