Documentation

Mathlib.CategoryTheory.Conj

Conjugate morphisms by isomorphisms #

An isomorphism α : X ≅ Y defines

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

Equations
  • α.conj = { toEquiv := α.homCongr α, map_mul' := }
Instances For
    @[simp]
    @[simp]
    theorem CategoryTheory.Iso.trans_conj {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X Y) {Z : C} (β : Y Z) (f : CategoryTheory.End X) :
    (α ≪≫ β).conj f = β.conj (α.conj f)
    @[simp]
    theorem CategoryTheory.Iso.symm_self_conj {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X Y) (f : CategoryTheory.End X) :
    α.symm.conj (α.conj f) = f
    @[simp]
    theorem CategoryTheory.Iso.self_symm_conj {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X Y) (f : CategoryTheory.End Y) :
    α.conj (α.symm.conj f) = f
    @[simp]
    theorem CategoryTheory.Iso.conj_pow {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X Y) (f : CategoryTheory.End X) (n : ) :
    α.conj (f ^ n) = α.conj f ^ n

    conj defines a group isomorphisms between groups of automorphisms

    Equations
    Instances For
      theorem CategoryTheory.Iso.conjAut_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X Y) (f : CategoryTheory.Aut X) :
      α.conjAut f = α.symm ≪≫ f ≪≫ α
      @[simp]
      theorem CategoryTheory.Iso.conjAut_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X Y) (f : CategoryTheory.Aut X) :
      (α.conjAut f).hom = α.conj f.hom
      @[simp]
      theorem CategoryTheory.Iso.trans_conjAut {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X Y) {Z : C} (β : Y Z) (f : CategoryTheory.Aut X) :
      (α ≪≫ β).conjAut f = β.conjAut (α.conjAut f)
      @[simp]
      theorem CategoryTheory.Iso.conjAut_mul {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X Y) (f : CategoryTheory.Aut X) (g : CategoryTheory.Aut X) :
      α.conjAut (f * g) = α.conjAut f * α.conjAut g
      @[simp]
      theorem CategoryTheory.Iso.conjAut_trans {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X Y) (f : CategoryTheory.Aut X) (g : CategoryTheory.Aut X) :
      α.conjAut (f ≪≫ g) = α.conjAut f ≪≫ α.conjAut g
      @[simp]
      theorem CategoryTheory.Iso.conjAut_pow {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X Y) (f : CategoryTheory.Aut X) (n : ) :
      α.conjAut (f ^ n) = α.conjAut f ^ n
      @[simp]
      theorem CategoryTheory.Iso.conjAut_zpow {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (α : X Y) (f : CategoryTheory.Aut X) (n : ) :
      α.conjAut (f ^ n) = α.conjAut f ^ n
      theorem CategoryTheory.Functor.map_conj {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} (α : X Y) (f : CategoryTheory.End X) :
      F.map (α.conj f) = (F.mapIso α).conj (F.map f)
      theorem CategoryTheory.Functor.map_conjAut {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} (α : X Y) (f : CategoryTheory.Aut X) :
      F.mapIso (α.conjAut f) = (F.mapIso α).conjAut (F.mapIso f)