English
Conjugation-then-mate and mate-then-conjugate commute in the two-square setting.
Русский
Сопряжение- затем отношение мейт и наоборот совместимы в двухквадратной конфигурации.
LaTeX
$$$\\text{conjugateEquiv } adj_1 adj_2(α) \\circ (\\text{mateEquiv } adj_1 adj_3)(β) = (\\text{mateEquiv } adj_2 adj_3)(β) \\circ (\\text{conjugateEquiv } adj_1 adj_2)(α)$$$
Lean4
/-- The mates equivalence commutes with this composition, essentially by `mateEquiv_vcomp`. -/
theorem conjugateEquiv_mateEquiv_vcomp {L₁ : A ⥤ B} {R₁ : B ⥤ A} {L₂ : A ⥤ B} {R₂ : B ⥤ A} {L₃ : C ⥤ D} {R₃ : D ⥤ C}
(adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (adj₃ : L₃ ⊣ R₃) (α : L₂ ⟶ L₁) (β : TwoSquare G L₂ L₃ H) :
(mateEquiv adj₁ adj₃) (β.whiskerLeft α) = (mateEquiv adj₂ adj₃ β).whiskerTop (conjugateEquiv adj₁ adj₂ α) :=
by
ext b
have vcomp := mateEquiv_vcomp adj₁ adj₂ adj₃ (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv) β
unfold vComp hComp at vcomp
unfold TwoSquare.whiskerLeft TwoSquare.whiskerTop conjugateEquiv
have vcompb := congr_app vcomp b
simp only [comp_obj, id_obj, whiskerRight_comp, assoc, mateEquiv_apply, whiskerLeft_comp, whiskerLeft_twice, comp_app,
Functor.whiskerLeft_app, Functor.whiskerRight_app, associator_hom_app, map_id, associator_inv_app,
leftUnitor_hom_app, rightUnitor_inv_app, Functor.comp_map, Functor.id_map, id_comp, whiskerRight_twice,
Iso.inv_hom_id_assoc, comp_id] at vcompb
simpa [mateEquiv]
