# Documentation

Mathlib.CategoryTheory.Endomorphism

# Endomorphisms #

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

For each X : C, we provide CategoryTheory.End X := X ⟶ X with a monoid structure, and CategoryTheory.Aut X := X ≅ X  with a group structure.

def CategoryTheory.End {C : Type u} (X : C) :

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

Instances For
instance CategoryTheory.End.one {C : Type u} (X : C) :
instance CategoryTheory.End.inhabited {C : Type u} (X : C) :
instance CategoryTheory.End.mul {C : Type u} (X : C) :

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

def CategoryTheory.End.of {C : Type u} {X : C} (f : X X) :

Assist the typechecker by expressing a morphism X ⟶ X as a term of CategoryTheory.End X.

Instances For
def CategoryTheory.End.asHom {C : Type u} {X : C} (f : ) :
X X

Assist the typechecker by expressing an endomorphism f : CategoryTheory.End X as a term of X ⟶ X.

Instances For
@[simp]
theorem CategoryTheory.End.one_def {C : Type u} {X : C} :
@[simp]
theorem CategoryTheory.End.mul_def {C : Type u} {X : C} (xs : ) (ys : ) :
xs * ys =
instance CategoryTheory.End.monoid {C : Type u} {X : C} :

Endomorphisms of an object form a monoid

instance CategoryTheory.End.mulActionRight {C : Type u} {X : C} {Y : C} :
MulAction () (X Y)
instance CategoryTheory.End.mulActionLeft {C : Type u} {X : Cᵒᵖ} {Y : C} :
MulAction () (X.unop Y)
theorem CategoryTheory.End.smul_right {C : Type u} {X : C} {Y : C} {r : } {f : X Y} :
theorem CategoryTheory.End.smul_left {C : Type u} {X : Cᵒᵖ} {Y : C} {r : } {f : X.unop Y} :
r f =
instance CategoryTheory.End.group {C : Type u} (X : C) :

In a groupoid, endomorphisms form a group

theorem CategoryTheory.isUnit_iff_isIso {C : Type u} {X : C} (f : ) :
def CategoryTheory.Aut {C : Type u} (X : C) :

Automorphisms of an object in a category.

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

Instances For
theorem CategoryTheory.Aut.ext {C : Type u} {X : C} {φ₁ : } {φ₂ : } (h : φ₁.hom = φ₂.hom) :
φ₁ = φ₂
instance CategoryTheory.Aut.inhabited {C : Type u} (X : C) :
instance CategoryTheory.Aut.instGroupAut {C : Type u} (X : C) :
theorem CategoryTheory.Aut.Aut_mul_def {C : Type u} (X : C) (f : ) (g : ) :
f * g = g ≪≫ f
theorem CategoryTheory.Aut.Aut_inv_def {C : Type u} (X : C) (f : ) :
f⁻¹ = f.symm

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

Instances For
def CategoryTheory.Aut.autMulEquivOfIso {C : Type u} {X : C} {Y : C} (h : X Y) :

Isomorphisms induce isomorphisms of the automorphism group

Instances For
@[simp]
theorem CategoryTheory.Functor.mapEnd_apply {C : Type u} (X : C) {D : Type u'} [] (f : ) :
∀ (a : X X), ↑() a = f.map a
def CategoryTheory.Functor.mapEnd {C : Type u} (X : C) {D : Type u'} [] (f : ) :

f.map as a monoid hom between endomorphism monoids.

Instances For
def CategoryTheory.Functor.mapAut {C : Type u} (X : C) {D : Type u'} [] (f : ) :

f.mapIso as a group hom between automorphism groups.

Instances For