map'_comp — Mathlib

English

If C has colimits, the skyscraper presheaf functor p0 ↦ skyscraperPresheafFunctor p0 is a right adjoint.

Русский

Если в категории C существуют колимиты, то функция skyscraperPresheafFunctor p0 является правой адъюнкцией.

LaTeX

$$$(skyscraperPresheafFunctor p_0).IsRightAdjoint$$$

Lean4

theorem map'_comp {a b c : C} (f : a ⟶ b) (g : b ⟶ c) :
    SkyscraperPresheafFunctor.map' p₀ (f ≫ g) =
      SkyscraperPresheafFunctor.map' p₀ f ≫ SkyscraperPresheafFunctor.map' p₀ g :=
  by
  ext U
  simp only [SkyscraperPresheafFunctor.map'_app]
  split_ifs with h <;> cat_disch

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