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.
Endomorphisms of an object in a category. Arguments order in multiplication agrees with
Function.comp
, not with CategoryTheory.CategoryStruct.comp
.
Instances For
Multiplication of endomorphisms agrees with Function.comp
, not with
CategoryTheory.CategoryStruct.comp
.
Assist the typechecker by expressing a morphism X ⟶ X
as a term of CategoryTheory.End X
.
Instances For
Assist the typechecker by expressing an endomorphism f : CategoryTheory.End X
as a term of
X ⟶ X
.
Instances For
Endomorphisms of an object form a monoid
Equations
Equations
Equations
In a groupoid, endomorphisms form a group
Automorphisms of an object in a category.
The order of arguments in multiplication agrees with
Function.comp
, not with CategoryTheory.CategoryStruct.comp
.
Instances For
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.
Instances For
Isomorphisms induce isomorphisms of the automorphism group
Equations
- One or more equations did not get rendered due to their size.
Instances For
f.map
as a monoid hom between endomorphism monoids.
Equations
- CategoryTheory.Functor.mapEnd X f = { toFun := f.map, map_one' := ⋯, map_mul' := ⋯ }
Instances For
f.mapIso
as a group hom between automorphism groups.
Equations
- CategoryTheory.Functor.mapAut X f = { toFun := f.mapIso, map_one' := ⋯, map_mul' := ⋯ }
Instances For
mulEquivEnd
as an isomorphism between endomorphism monoids.
Equations
- hf.mulEquivEnd X = { toEquiv := hf.homEquiv, map_mul' := ⋯ }
Instances For
mulEquivAut
as an isomorphism between automorphism groups.