Semiconjugacy and intertwining for multiplicative equivalences

An isomorphism ψ : M ≃* M' intertwines two endomorphisms F : M →* M and F' : M' →* M' when (ψ : M →* M').comp F = F'.comp (ψ : M →* M'). This is Function.Semiconj ψ F F' packaged for bundled monoid homomorphisms.

This file provides the inversion and composition laws for such intertwining relations, which show that intertwining by an isomorphism is symmetric and transitive.

Main results

• MulEquiv.symm_comp_eq_comp_symm_of_comp_eq_comp: an intertwining relation inverts along ψ.symm.
• TauCeti.trans_comp_eq_comp_trans_of_comp_eq_comp: intertwining relations compose along ψ.trans χ.

theorem MulEquiv.symm_comp_eq_comp_symm_of_comp_eq_comp {M : Type u_1} {M' : Type u_2} [MulOneClass M] [MulOneClass M'] {F : M →* M} {F' : M' →* M'} (ψ : M ≃* M') (hψ : (↑ψ).comp F = F'.comp ↑ψ) : (↑ψ.symm).comp F' = F.comp ↑ψ.symm

An isomorphism intertwining two endomorphisms has an inverse intertwining them the other way.

The equation is not symmetric in ψ and ψ.symm, so this provides the symmetry direction for intertwining relations.

theorem TauCeti.trans_comp_eq_comp_trans_of_comp_eq_comp {M : Type u_1} {M' : Type u_2} {M'' : Type u_3} [MulOneClass M] [MulOneClass M'] [MulOneClass M''] {F : M →* M} {F' : M' →* M'} {F'' : M'' →* M''} {ψ : M ≃* M'} {χ : M' ≃* M''} (hψ : (↑ψ).comp F = F'.comp ↑ψ) (hχ : (↑χ).comp F' = F''.comp ↑χ) : (↑(ψ.trans χ)).comp F = F''.comp ↑(ψ.trans χ)

Intertwining relations compose.