partialRightAdjointHomEquiv_map_comp

English

For f and g, the following holds: F.partialRightAdjointHomEquiv (F.partialRightAdjointMap f ≫ g) = F.partialRightAdjointHomEquiv f ≫ g, up to rearrangement with associativity.

Русский

Для f и g выполняется: F.partialRightAdjointHomEquiv (F.partialRightAdjointMap f ≫ g) = F.partialRightAdjointHomEquiv f ≫ g.

LaTeX

$$$F.partialRightAdjointHomEquiv (F.partialRightAdjointMap f \;\circ\; g) = F.partialRightAdjointHomEquiv f \;\circ\; g$$$

Lean4

theorem partialRightAdjointHomEquiv_map_comp {X : C} {Y Y' : F.PartialRightAdjointSource}
    (f : X ⟶ F.partialRightAdjointObj Y) (g : Y ⟶ Y') :
    F.partialRightAdjointHomEquiv (f ≫ F.partialRightAdjointMap g) = F.partialRightAdjointHomEquiv f ≫ g := by
  rw [partialRightAdjointHomEquiv_comp, partialRightAdjointHomEquiv_map, ← assoc, ← partialRightAdjointHomEquiv_comp,
    comp_id]

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