mathlib documentation

category_theory.endomorphism

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

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

Equations
@[instance]

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

Equations

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

Equations

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} [category_theory.category_struct C] {X : C} :
1 = 𝟙 X
@[simp]
theorem category_theory.End.mul_def {C : Type u} [category_theory.category_struct C] {X : C} (xs ys : category_theory.End X) :
xs * ys = ys xs
@[instance]

Endomorphisms of an object form a monoid

Equations
def category_theory.Aut {C : Type u} [category_theory.category C] (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

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

Equations

f.map as a monoid hom between endomorphism monoids.

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

f.map_iso as a group hom between automorphism groups.

Equations