English
Mating after conjugation equals conjugation after mating in a compatible way.
Русский
После сопряжения через сопряжение мейт соответствует сопряжению после мейтового преобразования.
LaTeX
$$$\\text{conjugateEquiv } adj_1 adj_2(α) = α' \\Rightarrow (\\text{mateEquiv } adj_1 adj_3)(α) = (\\text{mateEquiv } adj_1 adj_2 α) \\circ (\\text{conjugateEquiv } adj_2 adj_3)(β)$$$
Lean4
/-- The mates equivalence commutes with this composition, essentially by `mateEquiv_vcomp`. -/
theorem mateEquiv_conjugateEquiv_vcomp {L₁ : A ⥤ B} {R₁ : B ⥤ A} {L₂ : C ⥤ D} {R₂ : D ⥤ C} {L₃ : C ⥤ D} {R₃ : D ⥤ C}
(adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (adj₃ : L₃ ⊣ R₃) (α : TwoSquare G L₁ L₂ H) (β : L₃ ⟶ L₂) :
(mateEquiv adj₁ adj₃) (α.whiskerRight β) = (mateEquiv adj₁ adj₂ α).whiskerBottom (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.whiskerRight TwoSquare.whiskerBottom conjugateEquiv
have vcompb := congr_app vcomp b
simp only [comp_obj, id_obj, whiskerLeft_comp, assoc, mateEquiv_apply, whiskerLeft_twice, Iso.hom_inv_id_assoc,
whiskerRight_comp, comp_app, Functor.whiskerLeft_app, Functor.whiskerRight_app, associator_hom_app, map_id,
associator_inv_app, leftUnitor_hom_app, rightUnitor_inv_app, Functor.id_map, Functor.comp_map, id_comp,
whiskerRight_twice, comp_id] at vcompb
simpa [mateEquiv]
