presheafHom_naturality — Mathlib

English

Let f: P → Q be a morphism; then presheafHom φ is natural in P, Q with respect to f, matching f with the action on φ.

Русский

Пусть f: P → Q — морфизм; тогда presheafHom φ естественным образом зависит от P, Q по отношению к f и согласуется с действием φ.

LaTeX

$$$$ presheafHom.{w} φ P ≡ f ≡ presheafHom φ Q $$$$

Lean4

@[reassoc (attr := simp)]
theorem presheafHom_naturality {P Q : Cᵒᵖ ⥤ Type max w v₁ v₂} (f : P ⟶ Q) :
    presheafHom.{w} φ P ≫ Functor.whiskerLeft F.op (G.map f) = f ≫ presheafHom φ Q :=
  hom_ext_uliftYoneda.{max w v₂}
    (fun X p ↦
      uliftYonedaEquiv.injective
        (by
          rw [← assoc p f, uliftYonedaEquiv_ι_presheafHom, ← assoc, uliftYonedaEquiv_comp,
            uliftYonedaEquiv_ι_presheafHom, Functor.map_comp, FunctorToTypes.comp]
          dsimp))

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