partialRightAdjointHomEquiv_map — Mathlib

English

For morphisms f and f’s mapping under the left leg, the HomEquiv behaves as expected: F.partialRightAdjointHomEquiv (F.partialRightAdjointMap f) equals F.partialRightAdjointHomEquiv (id) ≫ f.

Русский

Для отображения f и его отображения через F.partialRightAdjointMap гомэквивариант ведёт себя естественно: F.partialRightAdjointHomEquiv (F.partialRightAdjointMap f) = F.partialRightAdjointHomEquiv (id) ≫ f.

LaTeX

$$$F.partialRightAdjointHomEquiv (F.partialRightAdjointMap f) = F.partialRightAdjointHomEquiv (\mathbf{1}) \;\circ\; f$$$

Lean4

@[simp]
theorem partialRightAdjointHomEquiv_map {X Y : F.PartialRightAdjointSource} (f : X ⟶ Y) :
    F.partialRightAdjointHomEquiv (F.partialRightAdjointMap f) = F.partialRightAdjointHomEquiv (𝟙 _) ≫ f := by
  simp [partialRightAdjointMap]

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