# mathlibdocumentation

category_theory.endomorphism

# Endomorphisms #

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

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

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

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

Equations
Instances for category_theory.End
@[protected, instance]
def category_theory.End.has_one {C : Type u} (X : C) :
Equations
@[protected, instance]
def category_theory.End.inhabited {C : Type u} (X : C) :
Equations
@[protected, instance]
def category_theory.End.has_mul {C : Type u} (X : C) :

Multiplication of endomorphisms agrees with function.comp, not category_struct.comp.

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

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

Equations
def category_theory.End.as_hom {C : Type u} {X : C} (f : category_theory.End X) :
X X

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

Equations
@[simp]
theorem category_theory.End.one_def {C : Type u} {X : C} :
1 = 𝟙 X
@[simp]
theorem category_theory.End.mul_def {C : Type u} {X : C} (xs ys : category_theory.End X) :
xs * ys = ys xs
@[protected, instance]
def category_theory.End.monoid {C : Type u} {X : C} :

Endomorphisms of an object form a monoid

Equations
@[protected, instance]
def category_theory.End.mul_action_right {C : Type u} {X Y : C} :
(X Y)
Equations
@[protected, instance]
def category_theory.End.mul_action_left {C : Type u} {X : Cᵒᵖ} {Y : C} :
Y)
Equations
theorem category_theory.End.smul_right {C : Type u} {X Y : C} {r : category_theory.End Y} {f : X Y} :
r f = f r
theorem category_theory.End.smul_left {C : Type u} {X : Cᵒᵖ} {Y : C} {r : category_theory.End X} {f : Y} :
r f =
@[protected, instance]
def category_theory.End.group {C : Type u} (X : C) :

In a groupoid, endomorphisms form a group

Equations
theorem category_theory.is_unit_iff_is_iso {C : Type u} {X : C} (f : category_theory.End X) :
def category_theory.Aut {C : Type u} (X : C) :
Type v

Automorphisms of an object in a category.

The order of arguments in multiplication agrees with function.comp, not with category.comp.

Equations
Instances for category_theory.Aut
@[protected, instance]
def category_theory.Aut.inhabited {C : Type u} (X : C) :
Equations
@[protected, instance]
def category_theory.Aut.group {C : Type u} (X : C) :
Equations
theorem category_theory.Aut.Aut_mul_def {C : Type u} (X : C) (f g : category_theory.Aut X) :
f * g = g ≪≫ f
def category_theory.Aut.units_End_equiv_Aut {C : Type u} (X : C) :

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

Equations
def category_theory.Aut.Aut_mul_equiv_of_iso {C : Type u} {X Y : C} (h : X Y) :

Isomorphisms induce isomorphisms of the automorphism group

Equations
def category_theory.functor.map_End {C : Type u} (X : C) {D : Type u'} (f : C D) :

f.map as a monoid hom between endomorphism monoids.

Equations
@[simp]
theorem category_theory.functor.map_End_apply {C : Type u} (X : C) {D : Type u'} (f : C D) (ᾰ : X X) :
= f.map
def category_theory.functor.map_Aut {C : Type u} (X : C) {D : Type u'} (f : C D) :

f.map_iso as a group hom between automorphism groups.

Equations