conjugateEquiv_comp_id_right_apply

English

A variant of the previous fact: (conjugateEquiv adj (adj'.comp Id)) of φ equals φ conjugated with the adjunctions, modulo right unitor.

Русский

Альтернатива: (conjugateEquiv adj (adj'.comp Id)) φ равно сопряжению φ через сопряжения, с правыми юниторами.

LaTeX

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

Lean4

theorem conjugateEquiv_comp_id_right_apply :
    conjugateEquiv adj (adj'.comp (Adjunction.id _)) ((ρ_ _).hom ≫ φ) = conjugateEquiv adj adj' φ ≫ (λ_ _).inv :=
  by
  simp only [conjugateEquiv_apply, Category.assoc, mateEquiv_comp_id_right, id_whiskerLeft, Iso.inv_hom_id,
    Category.comp_id, Iso.hom_inv_id, Iso.cancel_iso_inv_left, EmbeddingLike.apply_eq_iff_eq]
  bicategory

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