English
For an adjunction η, ε between f and g, the left zigzag associated to adjointifyCounit η ε matches the composition λ_f ≫ ρ_f^{-1}.
Русский
Для пары сущностей f ⊣ g с η и ε, левая зигзагообразная конструкция, задаваемая adjointifyCounit η ε, эквивалентна композиции λ_f ≫ ρ_f^{-1}.
LaTeX
$$$\\mathrm{leftZigzagIso}(\\eta,\\mathrm{adjointifyCounit}(\\eta,\\varepsilon)) = \\lambda_{f} \\;≪≫\\; (\\rho_{f}).{\\mathrm{symm}}$$$
Lean4
theorem adjointifyCounit_left_triangle (η : 𝟙 a ≅ f ≫ g) (ε : g ≫ f ≅ 𝟙 b) :
leftZigzagIso η (adjointifyCounit η ε) = λ_ f ≪≫ (ρ_ f).symm :=
by
apply Iso.ext
dsimp [adjointifyCounit, bicategoricalIsoComp]
calc
_ = 𝟙 _ ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom := by bicategory
_ = 𝟙 _ ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom := by
rw [← whisker_exchange η.hom (f ◁ ε.inv)]; bicategory
_ = 𝟙 _ ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom := by rw [← whisker_exchange η.hom η.inv]; bicategory
_ = 𝟙 _ ⊗≫ f ◁ (ε.inv ≫ ε.hom) := by rw [Iso.inv_hom_id]; bicategory
_ = _ := by rw [Iso.inv_hom_id]; bicategory
