English
Let adj be an adjunction L ⊣ R on a category C, and let α be a natural transformation R ⇒ Id_C. Then the conjugate of α by the pair (adj, id) satisfies at every object c that the component is the composition of the unit with α evaluated at L(c): ((conjugateEquiv adj Adjunction.id).symm α).app c = adj.unit.app c ∘ α.app (L.obj c).
Русский
Пусть для категории C дано тождественное сопряжение adj: L ⊣ R, и α — натуральное преобразование R ⇒ Id_C. Тогда сопряжённое преобразование α по паре (adj, identity) имеет на каждом объекте c компоненту, равную композиции единицы η_c с α_{L(c)}: ((conjugateEquiv adj Adjunction.id).symm α).app c = adj.unit.app c ∘ α.app (L.obj c).
LaTeX
$$$((\text{conjugateEquiv } adj\, \text{Adjunction.id}).symm\ \alpha).app\ c = (\text{adj}.unit).app\ c \circ \alpha.app(\text{L.obj } c).$$$
Lean4
theorem conjugateEquiv_adjunction_id_symm {L R : C ⥤ C} (adj : L ⊣ R) (α : R ⟶ 𝟭 C) (c : C) :
((conjugateEquiv adj Adjunction.id).symm α).app c = adj.unit.app c ≫ α.app (L.obj c) := by
simp [conjugateEquiv, mateEquiv, Adjunction.id]
