Endomorphisms

Definition and basic properties of endomorphisms and automorphisms of an object in a category.

For each X : C, we define a monoid CategoryTheory.End X which is a 1-field structure that is equipped with a bijection with X ⟶ X. Similarly, we define the group CategoryTheory.Aut X, which is equipped with a bijection with X ≅ X.

structure CategoryTheory.End {C : Type u} [CategoryStruct.{v, u} C] (X : C) : Type v

Endomorphisms of an object in a category. Arguments order in multiplication agrees with Function.comp, not with CategoryTheory.CategoryStruct.comp.

• of :: (
• asHom : X ⟶ X

  the underlying morphism of an endomorphism

• )

theorem CategoryTheory.End.ext {C : Type u} {inst✝ : CategoryStruct.{v, u} C} {X : C} {x y : End X} (asHom : x.asHom = y.asHom) : x = y

theorem CategoryTheory.End.ext_iff {C : Type u} {inst✝ : CategoryStruct.{v, u} C} {X : C} {x y : End X} : x = y ↔ x.asHom = y.asHom

@[implicit_reducible]

def CategoryTheory.End.homEquiv {C : Type u} [CategoryStruct.{v, u} C] {X : C} : End X ≃ (X ⟶ X)

The bijection End X ≃ (X ⟶ X).

Equations

• CategoryTheory.End.homEquiv = { toFun := CategoryTheory.End.asHom, invFun := CategoryTheory.End.of, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem CategoryTheory.End.homEquiv_symm_apply_asHom {C : Type u} [CategoryStruct.{v, u} C] {X : C} (asHom : X ⟶ X) : (homEquiv.symm asHom).asHom = asHom

@[simp]

theorem CategoryTheory.End.homEquiv_apply {C : Type u} [CategoryStruct.{v, u} C] {X : C} (self : End X) : homEquiv self = self.asHom

@[instance_reducible]

instance CategoryTheory.End.instOne {C : Type u} [CategoryStruct.{v, u} C] (X : C) : One (End X)

Equations

• CategoryTheory.End.instOne X = { one := { asHom := CategoryTheory.CategoryStruct.id X } }

@[simp]

theorem CategoryTheory.End.one_asHom {C : Type u} [CategoryStruct.{v, u} C] (X : C) : asHom 1 = CategoryStruct.id X

@[instance_reducible]

instance CategoryTheory.End.inhabited {C : Type u} [CategoryStruct.{v, u} C] (X : C) : Inhabited (End X)

Equations

• CategoryTheory.End.inhabited X = { default := { asHom := CategoryTheory.CategoryStruct.id X } }

@[instance_reducible]

instance CategoryTheory.End.instMul {C : Type u} [CategoryStruct.{v, u} C] (X : C) : Mul (End X)

Multiplication of endomorphisms agrees with Function.comp, not with CategoryTheory.CategoryStruct.comp.

Equations

• CategoryTheory.End.instMul X = { mul := fun (f g : CategoryTheory.End X) => { asHom := CategoryTheory.CategoryStruct.comp g.asHom f.asHom } }

@[simp]

theorem CategoryTheory.End.mul_asHom {C : Type u} [CategoryStruct.{v, u} C] (X : C) (f g : End X) : (f * g).asHom = CategoryStruct.comp g.asHom f.asHom

@[deprecated CategoryTheory.End.one_asHom (since := "2026-09-12")]

theorem CategoryTheory.End.one_def {C : Type u} [CategoryStruct.{v, u} C] (X : C) : asHom 1 = CategoryStruct.id X

Alias of CategoryTheory.End.one_asHom.

@[deprecated CategoryTheory.End.mul_asHom (since := "2026-09-12")]

theorem CategoryTheory.End.mul_def {C : Type u} [CategoryStruct.{v, u} C] (X : C) (f g : End X) : (f * g).asHom = CategoryStruct.comp g.asHom f.asHom

Alias of CategoryTheory.End.mul_asHom.

@[instance_reducible]

instance CategoryTheory.End.monoid {C : Type u} [Category.{v, u} C] {X : C} : Monoid (End X)

Endomorphisms of an object form a monoid

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance CategoryTheory.End.instSMulHom {C : Type u} [Category.{v, u} C] {X Y : C} : SMul (End Y) (X ⟶ Y)

Equations

• CategoryTheory.End.instSMulHom = { smul := fun (r : CategoryTheory.End Y) (f : X ⟶ Y) => CategoryTheory.CategoryStruct.comp f r.asHom }

@[instance_reducible]

instance CategoryTheory.End.instSMulMulOppositeHom {C : Type u} [Category.{v, u} C] {X Y : C} : SMul (End X)ᵐᵒᵖ (X ⟶ Y)

Equations

• CategoryTheory.End.instSMulMulOppositeHom = { smul := fun (r : (CategoryTheory.End X)ᵐᵒᵖ) (f : X ⟶ Y) => CategoryTheory.CategoryStruct.comp (MulOpposite.unop r).asHom f }

theorem CategoryTheory.End.smul_right {C : Type u} [Category.{v, u} C] {X Y : C} {r : End Y} {f : X ⟶ Y} : r • f = CategoryStruct.comp f r.asHom

theorem CategoryTheory.End.smul_left {C : Type u} [Category.{v, u} C] {X Y : C} {r : (End X)ᵐᵒᵖ} {f : X ⟶ Y} : r • f = CategoryStruct.comp (MulOpposite.unop r).asHom f

@[instance_reducible]

instance CategoryTheory.End.mulActionRight {C : Type u} [Category.{v, u} C] {X Y : C} : MulAction (End Y) (X ⟶ Y)

Equations

• CategoryTheory.End.mulActionRight = { toSMul := CategoryTheory.End.instSMulHom, mul_smul := ⋯, one_smul := ⋯ }

@[instance_reducible]

instance CategoryTheory.End.mulActionLeft {C : Type u} [Category.{v, u} C] {X Y : C} : MulAction (End X)ᵐᵒᵖ (X ⟶ Y)

Equations

• CategoryTheory.End.mulActionLeft = { toSMul := CategoryTheory.End.instSMulMulOppositeHom, mul_smul := ⋯, one_smul := ⋯ }

@[instance_reducible]

instance CategoryTheory.End.group {C : Type u} [Groupoid C] (X : C) : Group (End X)

In a groupoid, endomorphisms form a group

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.isUnit_iff_isIso {C : Type u} [Category.{v, u} C] {X : C} (f : End X) : IsUnit f ↔ IsIso f.asHom

structure CategoryTheory.Aut {C : Type u} [Category.{v, u} C] (X : C) : Type v

Automorphisms of an object in a category.

The order of arguments in multiplication agrees with Function.comp, not with CategoryTheory.CategoryStruct.comp.

• of :: (
• asIso : X ≅ X

  the underlying isomorphism of an automorphism

• )

theorem CategoryTheory.Aut.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {X : C} {x y : Aut X} : x = y ↔ x.asIso = y.asIso

theorem CategoryTheory.Aut.ext {C : Type u} {inst✝ : Category.{v, u} C} {X : C} {x y : Aut X} (asIso : x.asIso = y.asIso) : x = y

@[implicit_reducible]

def CategoryTheory.Aut.isoEquiv {C : Type u} [Category.{v, u} C] {X : C} : Aut X ≃ (X ≅ X)

The bijection Aut X ≃ (X ≅ X).

Equations

• CategoryTheory.Aut.isoEquiv = { toFun := CategoryTheory.Aut.asIso, invFun := CategoryTheory.Aut.of, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem CategoryTheory.Aut.isoEquiv_symm_apply_asIso {C : Type u} [Category.{v, u} C] {X : C} (asIso : X ≅ X) : (isoEquiv.symm asIso).asIso = asIso

@[simp]

theorem CategoryTheory.Aut.isoEquiv_apply {C : Type u} [Category.{v, u} C] {X : C} (self : Aut X) : isoEquiv self = self.asIso

@[instance_reducible]

instance CategoryTheory.Aut.inhabited {C : Type u} [Category.{v, u} C] (X : C) : Inhabited (Aut X)

Equations

• CategoryTheory.Aut.inhabited X = { default := { asIso := CategoryTheory.Iso.refl X } }

@[instance_reducible]

instance CategoryTheory.Aut.instOne {C : Type u} [Category.{v, u} C] (X : C) : One (Aut X)

Equations

• CategoryTheory.Aut.instOne X = { one := { asIso := CategoryTheory.Iso.refl X } }

@[simp]

theorem CategoryTheory.Aut.one_asIso {C : Type u} [Category.{v, u} C] (X : C) : asIso 1 = Iso.refl X

@[instance_reducible]

instance CategoryTheory.Aut.instInv {C : Type u} [Category.{v, u} C] (X : C) : Inv (Aut X)

Equations

• CategoryTheory.Aut.instInv X = { inv := fun (e : CategoryTheory.Aut X) => { asIso := e.asIso.symm } }

@[simp]

theorem CategoryTheory.Aut.inv_asIso {C : Type u} [Category.{v, u} C] (X : C) (e : Aut X) : e⁻¹.asIso = e.asIso.symm

@[instance_reducible]

instance CategoryTheory.Aut.instMul {C : Type u} [Category.{v, u} C] (X : C) : Mul (Aut X)

Equations

• CategoryTheory.Aut.instMul X = { mul := fun (x y : CategoryTheory.Aut X) => { asIso := y.asIso ≪≫ x.asIso } }

@[simp]

theorem CategoryTheory.Aut.mul_asIso {C : Type u} [Category.{v, u} C] (X : C) (x y : Aut X) : (x * y).asIso = y.asIso ≪≫ x.asIso

@[instance_reducible]

instance CategoryTheory.Aut.instGroup {C : Type u} [Category.{v, u} C] (X : C) : Group (Aut X)

Equations

• One or more equations did not get rendered due to their size.

@[deprecated CategoryTheory.Aut.mul_asIso (since := "2026-09-12")]

theorem CategoryTheory.Aut.Aut_mul_def {C : Type u} [Category.{v, u} C] (X : C) (x y : Aut X) : (x * y).asIso = y.asIso ≪≫ x.asIso

Alias of CategoryTheory.Aut.mul_asIso.

@[deprecated CategoryTheory.Aut.inv_asIso (since := "2026-09-12")]

theorem CategoryTheory.Aut.Aut_inv_def {C : Type u} [Category.{v, u} C] (X : C) (e : Aut X) : e⁻¹.asIso = e.asIso.symm

Alias of CategoryTheory.Aut.inv_asIso.

def CategoryTheory.Aut.toEnd {C : Type u} [Category.{v, u} C] {X : C} : Aut X →* End X

The inclusion of Aut X in End X as a monoid homomorphism.

Equations

• CategoryTheory.Aut.toEnd = { toFun := fun (e : CategoryTheory.Aut X) => { asHom := e.asIso.hom }, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem CategoryTheory.Aut.toEnd_apply_asHom {C : Type u} [Category.{v, u} C] {X : C} (e : Aut X) : (toEnd e).asHom = e.asIso.hom

def CategoryTheory.Aut.unitsEndEquivAut {C : Type u} [Category.{v, u} C] (X : C) : (End X)ˣ ≃* Aut X

Units in the monoid of endomorphisms of an object are (multiplicatively) equivalent to automorphisms of that object.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Aut.unitsEndEquivAut_apply_asIso_hom {C : Type u} [Category.{v, u} C] (X : C) (f : (End X)ˣ) : ((unitsEndEquivAut X) f).asIso.hom = (↑f).asHom

@[simp]

theorem CategoryTheory.Aut.val_unitsEndEquivAut_symm_apply_asHom {C : Type u} [Category.{v, u} C] (X : C) (f : Aut X) : (↑((unitsEndEquivAut X).symm f)).asHom = f.asIso.hom

@[simp]

theorem CategoryTheory.Aut.unitsEndEquivAut_apply_asIso_inv {C : Type u} [Category.{v, u} C] (X : C) (f : (End X)ˣ) : ((unitsEndEquivAut X) f).asIso.inv = f.inv.asHom

@[simp]

theorem CategoryTheory.Aut.val_inv_unitsEndEquivAut_symm_apply_asHom {C : Type u} [Category.{v, u} C] (X : C) (f : Aut X) : (↑((unitsEndEquivAut X).symm f)⁻¹).asHom = f.asIso.inv

def CategoryTheory.Aut.autMulEquivOfIso {C : Type u} [Category.{v, u} C] {X Y : C} (h : X ≅ Y) : Aut X ≃* Aut Y

Isomorphisms induce isomorphisms of the automorphism group

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Aut.autMulEquivOfIso_apply_asIso {C : Type u} [Category.{v, u} C] {X Y : C} (h : X ≅ Y) (e : Aut X) : ((autMulEquivOfIso h) e).asIso = h.symm ≪≫ e.asIso ≪≫ h

@[simp]

theorem CategoryTheory.Aut.autMulEquivOfIso_symm_apply_asIso {C : Type u} [Category.{v, u} C] {X Y : C} (h : X ≅ Y) (e : Aut Y) : ((autMulEquivOfIso h).symm e).asIso = h ≪≫ e.asIso ≪≫ h.symm

@[implicit_reducible]

def CategoryTheory.Functor.mapEnd {C : Type u} [Category.{v, u} C] (X : C) {D : Type u'} [Category.{v', u'} D] (f : Functor C D) : End X →* End (f.obj X)

f.map as a monoid hom between endomorphism monoids.

Equations

• CategoryTheory.Functor.mapEnd X f = { toFun := fun (e : CategoryTheory.End X) => { asHom := f.map e.asHom }, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem CategoryTheory.Functor.mapEnd_apply_asHom {C : Type u} [Category.{v, u} C] (X : C) {D : Type u'} [Category.{v', u'} D] (f : Functor C D) (e : End X) : ((mapEnd X f) e).asHom = f.map e.asHom

@[implicit_reducible]

def CategoryTheory.Functor.mapAut {C : Type u} [Category.{v, u} C] (X : C) {D : Type u'} [Category.{v', u'} D] (f : Functor C D) : Aut X →* Aut (f.obj X)

f.mapIso as a group hom between automorphism groups.

Equations

• CategoryTheory.Functor.mapAut X f = { toFun := fun (e : CategoryTheory.Aut X) => { asIso := f.mapIso e.asIso }, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem CategoryTheory.Functor.mapAut_apply_asIso {C : Type u} [Category.{v, u} C] (X : C) {D : Type u'} [Category.{v', u'} D] (f : Functor C D) (e : Aut X) : ((mapAut X f) e).asIso = f.mapIso e.asIso

noncomputable def CategoryTheory.Functor.FullyFaithful.mulEquivEnd {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {f : Functor C D} (hf : f.FullyFaithful) (X : C) : End X ≃* End (f.obj X)

mulEquivEnd as an isomorphism between endomorphism monoids.

Equations

• hf.mulEquivEnd X = { toEquiv := CategoryTheory.End.homEquiv.trans (hf.homEquiv.trans CategoryTheory.End.homEquiv.symm), map_mul' := ⋯ }

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.mulEquivEnd_symm_apply_asHom {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {f : Functor C D} (hf : f.FullyFaithful) (X : C) (a✝ : End (f.obj X)) : ((hf.mulEquivEnd X).symm a✝).asHom = hf.preimage a✝.asHom

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.mulEquivEnd_apply_asHom {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {f : Functor C D} (hf : f.FullyFaithful) (X : C) (a✝ : End X) : ((hf.mulEquivEnd X) a✝).asHom = f.map a✝.asHom

noncomputable def CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {f : Functor C D} (hf : f.FullyFaithful) (X : C) : Aut X ≃* Aut (f.obj X)

mulEquivAut as an isomorphism between automorphism groups.

Equations

• hf.autMulEquivOfFullyFaithful X = { toEquiv := CategoryTheory.Aut.isoEquiv.trans (hf.isoEquiv.trans CategoryTheory.Aut.isoEquiv.symm), map_mul' := ⋯ }

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_symm_apply_asIso_inv {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {f : Functor C D} (hf : f.FullyFaithful) (X : C) (a✝ : Aut (f.obj X)) : ((hf.autMulEquivOfFullyFaithful X).symm a✝).asIso.inv = hf.preimage a✝.asIso.inv

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_apply_asIso_inv {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {f : Functor C D} (hf : f.FullyFaithful) (X : C) (a✝ : Aut X) : ((hf.autMulEquivOfFullyFaithful X) a✝).asIso.inv = f.map a✝.asIso.inv

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_symm_apply_asIso_hom {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {f : Functor C D} (hf : f.FullyFaithful) (X : C) (a✝ : Aut (f.obj X)) : ((hf.autMulEquivOfFullyFaithful X).symm a✝).asIso.hom = hf.preimage a✝.asIso.hom

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_apply_asIso_hom {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {f : Functor C D} (hf : f.FullyFaithful) (X : C) (a✝ : Aut X) : ((hf.autMulEquivOfFullyFaithful X) a✝).asIso.hom = f.map a✝.asIso.hom

def CategoryTheory.InducedCategory.endEquiv {C : Type u} [Category.{v, u} C] {D : Type u_1} {F : D → C} {X : InducedCategory C F} : End X ≃* End (F X)

The multiplicative bijection End X ≃* End (F X) when X : InducedCategory C F.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.InducedCategory.endEquiv_apply_asHom {C : Type u} [Category.{v, u} C] {D : Type u_1} {F : D → C} {X : InducedCategory C F} (a✝ : End X) : (endEquiv a✝).asHom = a✝.asHom.hom

@[simp]

theorem CategoryTheory.InducedCategory.endEquiv_symm_apply_asHom_hom {C : Type u} [Category.{v, u} C] {D : Type u_1} {F : D → C} {X : InducedCategory C F} (a✝ : End (F X)) : (endEquiv.symm a✝).asHom.hom = a✝.asHom