English
For f and g as specified, the functoriality of the partialLeftAdjointHomEquiv is compatible with composition: F.partialLeftAdjointHomEquiv (F.partialLeftAdjointMap f ≫ g) equals F.partialLeftAdjointHomEquiv f ≫ F.map g, which is the standard functoriality property.
Русский
Для указанных f и g отображение частичного левого сопряжения совместимо с композициями: F.partialLeftAdjointHomEquiv (F.partialLeftAdjointMap f ≫ g) = F.partialLeftAdjointHomEquiv f ≫ F.map g.
LaTeX
$$$F.partialLeftAdjointHomEquiv (F.partialLeftAdjointMap f \;\circ\; g) = F.partialLeftAdjointHomEquiv f \;\circ\; F.map g$$$
Lean4
theorem partialLeftAdjointHomEquiv_map_comp {X X' : F.PartialLeftAdjointSource} {Y : D} (f : X ⟶ X')
(g : F.partialLeftAdjointObj X' ⟶ Y) :
F.partialLeftAdjointHomEquiv (F.partialLeftAdjointMap f ≫ g) = by exact f ≫ F.partialLeftAdjointHomEquiv g := by
rw [partialLeftAdjointHomEquiv_comp, partialLeftAdjointHomEquiv_map, assoc, ← partialLeftAdjointHomEquiv_comp,
id_comp]
