conjugateEquiv_id_comp_right_apply

English

The conjugate with a composition of right adjunction and id yields a simple relation: conjugateEquiv adj ((Adjunction.id).comp adj') ((λ_ _).hom ≫ φ) = conjugateEquiv adj adj' φ ≫ (λ_ _).inv.

Русский

При сопряжении с (id ∘ adj') получается relation: conjugateEquiv adj ((id c).comp adj') ((λ_ _).hom ≫ φ) = conjugateEquiv adj adj' φ ≫ (λ_ _).inv.

LaTeX

$$$$ \\text{conjugateEquiv } adj ((Adjunction.id\\ _).comp adj') ((\\lambda_\\_).hom \\gg \\phi) = \\text{conjugateEquiv } adj adj' \\phi \\gg (\\lambda_\\_).inv. $$$$

Lean4

theorem conjugateEquiv_id_comp_right_apply :
    conjugateEquiv adj ((Adjunction.id _).comp adj') ((λ_ _).hom ≫ φ) = conjugateEquiv adj adj' φ ≫ (ρ_ _).inv :=
  by
  simp only [conjugateEquiv_apply, mateEquiv_id_comp_right, id_whiskerLeft, Category.assoc, Iso.inv_hom_id_assoc]
  bicategory

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