partialLeftAdjointHomEquiv_comp — Mathlib

English

If R is a diagram and hc, hc' are IsColimit cocones, then F ⋙ coyoneda.obj (op c.pt) corepresentable by c'.pt via the cocones; i.e., there is a corepresentability structure compatible with the colimit cocones.

Русский

Пусть R — диаграмма, a hc, hc' — IsColimit коконы; тогда F ⋙ coyoneda.obj (op c.pt) является ядром презентируемым через c'.pt совместимо с коконами колимита.

LaTeX

$$$\text{CorepresentableBy}(F \circ \mathrm{coyoneda.obj}(\mathrm{op} c.pt)) \; c'$$$

Lean4

theorem partialLeftAdjointHomEquiv_comp {X : F.PartialLeftAdjointSource} {Y Y' : D} (f : F.partialLeftAdjointObj X ⟶ Y)
    (g : Y ⟶ Y') : F.partialLeftAdjointHomEquiv (f ≫ g) = F.partialLeftAdjointHomEquiv f ≫ F.map g := by
  apply CorepresentableBy.homEquiv_comp

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