Endomorphisms of an object in a category. Arguments order in multiplication agrees with
function.comp, not with category.comp.
Equations
- category_theory.End X = (X ⟶ X)
@[instance]
Equations
- category_theory.End.has_one X = {one := 𝟙 X}
@[instance]
Multiplication of endomorphisms agrees with function.comp, not category_struct.comp.
Equations
- category_theory.End.has_mul X = {mul := λ (x y : category_theory.End X), y ≫ x}
@[simp]
@[simp]
theorem
category_theory.End.mul_def
{C : Type u}
[category_theory.category_struct C]
{X : C}
(xs ys : category_theory.End X) :
@[instance]
Endomorphisms of an object form a monoid
Equations
- category_theory.End.monoid = {mul := has_mul.mul (category_theory.End.has_mul X), mul_assoc := _, one := 1, one_mul := _, mul_one := _}
@[instance]
In a groupoid, endomorphisms form a group
Equations
- category_theory.End.group X = {mul := monoid.mul category_theory.End.monoid, mul_assoc := _, one := monoid.one category_theory.End.monoid, one_mul := _, mul_one := _, inv := category_theory.groupoid.inv X, mul_left_inv := _}
Equations
- category_theory.Aut X = (X ≅ X)
@[instance]
Equations
- category_theory.Aut.group X = {mul := flip category_theory.iso.trans, mul_assoc := _, one := category_theory.iso.refl X, one_mul := _, mul_one := _, inv := category_theory.iso.symm X, mul_left_inv := _}
Units in the monoid of endomorphisms of an object are (multiplicatively) equivalent to automorphisms of that object.
Equations
- category_theory.Aut.units_End_equiv_Aut X = {to_fun := λ (f : units (category_theory.End X)), {hom := f.val, inv := f.inv, hom_inv_id' := _, inv_hom_id' := _}, inv_fun := λ (f : category_theory.Aut X), {val := f.hom, inv := f.inv, val_inv := _, inv_val := _}, left_inv := _, right_inv := _, map_mul' := _}
def
category_theory.functor.map_End
{C : Type u}
[category_theory.category C]
(X : C)
{D : Type u'}
[category_theory.category D]
(f : C ⥤ D) :
category_theory.End X →* category_theory.End (f.obj X)
f.map as a monoid hom between endomorphism monoids.
def
category_theory.functor.map_Aut
{C : Type u}
[category_theory.category C]
(X : C)
{D : Type u'}
[category_theory.category D]
(f : C ⥤ D) :
category_theory.Aut X →* category_theory.Aut (f.obj X)
f.map_iso as a group hom between automorphism groups.