partialLeftAdjointHomEquiv_map — Mathlib

English

In the left adjoint framework, applying the hom-equivalence to F.partialLeftAdjointMap f yields the same as composing with f on the left inside the domain, i.e., F.partialLeftAdjointHomEquiv (F.partialLeftAdjointMap f) = f ≫ F.partialLeftAdjointHomEquiv (𝟙 _).

Русский

Для частичного левого сопряжённого отображения применение гом-эквиварианта к F.partialLeftAdjointMap f даёт тот же результат, что и композиция с f слева внутри области определения.

LaTeX

$$$F.partialLeftAdjointHomEquiv (F.partialLeftAdjointMap f) = f \;\circ\; F.partialLeftAdjointHomEquiv (\mathbf{1})$$$

Lean4

@[simp]
theorem partialLeftAdjointHomEquiv_map {X Y : F.PartialLeftAdjointSource} (f : X ⟶ Y) :
    F.partialLeftAdjointHomEquiv (F.partialLeftAdjointMap f) = by exact f ≫ F.partialLeftAdjointHomEquiv (𝟙 _) := by
  simp [partialLeftAdjointMap]

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