Conjugate morphisms by isomorphisms
α : X ≅ Y defines
- a monoid isomorphism
conj : End X ≃* End Yby
α.conj f = α.inv ≫ f ≫ α.hom;
- a group isomorphism
conj_Aut : Aut X ≃* Aut Yby
α.conj_Aut f = α.symm ≪≫ f ≪≫ α.
For completeness, we also define
hom_congr : (X ≅ X₁) → (Y ≅ Y₁) → (X ⟶ Y) ≃ (X₁ ⟶ Y₁), cf.
X is isomorphic to
Y is isomorphic to
there is a natural bijection between
X ⟶ Y and
X₁ ⟶ Y₁. See also
An isomorphism between two objects defines a monoid isomorphism between their monoid of endomorphisms.
conj defines a group isomorphisms between groups of automorphisms