Conjugate morphisms by isomorphisms

An isomorphism α : X ≅ Y defines

a monoid isomorphism conj : End X ≃* End Y by α.conj f = α.inv ≫ f ≫ α.hom;
a group isomorphism conj_Aut : Aut X ≃* Aut Y by α.conj_Aut f = α.symm ≪≫ f ≪≫ α.

For completeness, we also define hom_congr : (X ≅ X₁) → (Y ≅ Y₁) → (X ⟶ Y) ≃ (X₁ ⟶ Y₁), cf. equiv.arrow_congr.

An isomorphism between two objects defines a monoid isomorphism between their monoid of endomorphisms.

conj defines a group isomorphisms between groups of automorphisms