Conjugate morphisms by isomorphisms #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
α : 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₁),
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