naturality — Mathlib

English

The Coyoneda functor is full: every natural transformation between coyoneda objects arises from a morphism in C.

Русский

Функтор Coyoneda полнообразен: каждая естественная трансформация между объектами Coyoneda получается из морфизма в C.

LaTeX

$$The functor $\mathrm{coyoneda}: C^{op} \to C \to \mathrm{Type}$ is full.$$

Lean4

@[simp]
theorem naturality {X Y : Cᵒᵖ} (α : coyoneda.obj X ⟶ coyoneda.obj Y) {Z Z' : C} (f : Z' ⟶ Z) (h : unop X ⟶ Z') :
    α.app Z' h ≫ f = α.app Z (h ≫ f) :=
  (FunctorToTypes.naturality _ _ α f h).symm

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