partialRightAdjointHomEquiv_comp — Mathlib

English

For f: X' ⟶ F.partialRightAdjointObj Y and g: X ⟶ X', the bijection respects composition: F.partialRightAdjointHomEquiv (g ≫ f) = F.map g ≫ F.partialRightAdjointHomEquiv f.

Русский

Для f: X' ⟶ F.partialRightAdjointObj Y и g: X ⟶ X' биекция сохраняет композицию: F.partialRightAdjointHomEquiv (g ≫ f) = F.map g ≫ F.partialRightAdjointHomEquiv f.

LaTeX

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

Lean4

theorem partialRightAdjointHomEquiv_comp {X X' : C} {Y : F.PartialRightAdjointSource}
    (f : X' ⟶ F.partialRightAdjointObj Y) (g : X ⟶ X') :
    F.partialRightAdjointHomEquiv (g ≫ f) = F.map g ≫ F.partialRightAdjointHomEquiv f :=
  RepresentableBy.homEquiv_comp ..

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