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.

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

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

Equations
Instances For
instance CategoryTheory.End.one {C : Type u} (X : C) :
Equations
• = { one := }
instance CategoryTheory.End.inhabited {C : Type u} (X : C) :
Equations
• = { default := }
instance CategoryTheory.End.mul {C : Type u} (X : C) :

Multiplication of endomorphisms agrees with Function.comp, not with CategoryTheory.CategoryStruct.comp.

Equations
• = { mul := fun (x y : ) => }
def CategoryTheory.End.of {C : Type u} {X : C} (f : X X) :

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

Equations
Instances For
def CategoryTheory.End.asHom {C : Type u} {X : C} (f : ) :
X X

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

Equations
• f.asHom = f
Instances For
@[simp]
theorem CategoryTheory.End.one_def {C : Type u} {X : C} :
@[simp]
theorem CategoryTheory.End.mul_def {C : Type u} {X : C} (xs : ) (ys : ) :
xs * ys =
instance CategoryTheory.End.monoid {C : Type u} {X : C} :

Endomorphisms of an object form a monoid

Equations
• CategoryTheory.End.monoid = Monoid.mk npowRec
instance CategoryTheory.End.mulActionRight {C : Type u} {X : C} {Y : C} :
Equations
• CategoryTheory.End.mulActionRight =
instance CategoryTheory.End.mulActionLeft {C : Type u} {X : Cᵒᵖ} {Y : C} :
MulAction (X.unop Y)
Equations
• CategoryTheory.End.mulActionLeft =
theorem CategoryTheory.End.smul_right {C : Type u} {X : C} {Y : C} {r : } {f : X Y} :
theorem CategoryTheory.End.smul_left {C : Type u} {X : Cᵒᵖ} {Y : C} {r : } {f : X.unop Y} :
instance CategoryTheory.End.group {C : Type u} (X : C) :

In a groupoid, endomorphisms form a group

Equations
theorem CategoryTheory.isUnit_iff_isIso {C : Type u} {X : C} (f : ) :
def CategoryTheory.Aut {C : Type u} (X : C) :

Automorphisms of an object in a category.

The order of arguments in multiplication agrees with Function.comp, not with CategoryTheory.CategoryStruct.comp.

Equations
Instances For
theorem CategoryTheory.Aut.ext {C : Type u} {X : C} {φ₁ : } {φ₂ : } (h : φ₁.hom = φ₂.hom) :
φ₁ = φ₂
instance CategoryTheory.Aut.inhabited {C : Type u} (X : C) :
Equations
• = { default := }
instance CategoryTheory.Aut.instGroup {C : Type u} (X : C) :
Equations
theorem CategoryTheory.Aut.Aut_mul_def {C : Type u} (X : C) (f : ) (g : ) :
f * g = g ≪≫ f
theorem CategoryTheory.Aut.Aut_inv_def {C : Type u} (X : C) (f : ) :

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
@[simp]
theorem CategoryTheory.Aut.toEnd_apply {C : Type u} (X : C) :
∀ (a : ), = (.symm a)
def CategoryTheory.Aut.toEnd {C : Type u} (X : C) :

The inclusion of Aut X to End X as a monoid homomorphism.

Equations
• = .comp .symm
Instances For
def CategoryTheory.Aut.autMulEquivOfIso {C : Type u} {X : C} {Y : C} (h : X Y) :

Isomorphisms induce isomorphisms of the automorphism group

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.Functor.mapEnd_apply {C : Type u} (X : C) {D : Type u'} [] (f : ) :
∀ (a : X X), = f.map a
def CategoryTheory.Functor.mapEnd {C : Type u} (X : C) {D : Type u'} [] (f : ) :

f.map as a monoid hom between endomorphism monoids.

Equations
• = { toFun := f.map, map_one' := , map_mul' := }
Instances For
def CategoryTheory.Functor.mapAut {C : Type u} (X : C) {D : Type u'} [] (f : ) :

f.mapIso as a group hom between automorphism groups.

Equations
• = { toFun := f.mapIso, map_one' := , map_mul' := }
Instances For
@[simp]
theorem CategoryTheory.Functor.FullyFaithful.mulEquivEnd_symm_apply {C : Type u} {D : Type u'} [] {f : } (hf : f✝.FullyFaithful) (X : C) (f : f✝.obj X f✝.obj X) :
(hf.mulEquivEnd X).symm f = hf.preimage f
@[simp]
theorem CategoryTheory.Functor.FullyFaithful.mulEquivEnd_apply {C : Type u} {D : Type u'} [] {f : } (hf : f.FullyFaithful) (X : C) :
∀ (a : X X), (hf.mulEquivEnd X) a = f.map a
noncomputable def CategoryTheory.Functor.FullyFaithful.mulEquivEnd {C : Type u} {D : Type u'} [] {f : } (hf : f.FullyFaithful) (X : C) :

mulEquivEnd as an isomorphism between endomorphism monoids.

Equations
• hf.mulEquivEnd X = let __spread.0 := ; { toEquiv := hf.homEquiv, map_mul' := }
Instances For
@[simp]
theorem CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_apply_inv {C : Type u} {D : Type u'} [] {f : } (hf : f.FullyFaithful) (X : C) (i : X X) :
((hf.autMulEquivOfFullyFaithful X) i).inv = f.map i.inv
@[simp]
theorem CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_symm_apply_inv {C : Type u} {D : Type u'} [] {f : } (hf : f.FullyFaithful) (X : C) (e : f.obj X f.obj X) :
((hf.autMulEquivOfFullyFaithful X).symm e).inv = hf.preimage e.inv
@[simp]
theorem CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_symm_apply_hom {C : Type u} {D : Type u'} [] {f : } (hf : f.FullyFaithful) (X : C) (e : f.obj X f.obj X) :
((hf.autMulEquivOfFullyFaithful X).symm e).hom = hf.preimage e.hom
@[simp]
theorem CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_apply_hom {C : Type u} {D : Type u'} [] {f : } (hf : f.FullyFaithful) (X : C) (i : X X) :
((hf.autMulEquivOfFullyFaithful X) i).hom = f.map i.hom
noncomputable def CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful {C : Type u} {D : Type u'} [] {f : } (hf : f.FullyFaithful) (X : C) :

mulEquivAut as an isomorphism between automorphism groups.

Equations
• hf.autMulEquivOfFullyFaithful X = let __spread.0 := ; { toEquiv := hf.isoEquiv, map_mul' := }
Instances For