mathlib documentation

category_theory.endomorphism

def category_theory.End {C : Type u} [category_theory.category_struct C] :
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
@[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] :
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

f.map_iso as a group hom between automorphism groups.

Equations