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} [CategoryStruct.{v, u} C] (X : C) : Type v

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

Equations

• CategoryTheory.End X = (X ⟶ X)

instance CategoryTheory.End.one {C : Type u} [CategoryStruct.{v, u} C] (X : C) : One (End X)

Equations

• CategoryTheory.End.one X = { one := CategoryTheory.CategoryStruct.id X }

instance CategoryTheory.End.inhabited {C : Type u} [CategoryStruct.{v, u} C] (X : C) : Inhabited (End X)

Equations

• CategoryTheory.End.inhabited X = { default := CategoryTheory.CategoryStruct.id X }

instance CategoryTheory.End.mul {C : Type u} [CategoryStruct.{v, u} C] (X : C) : Mul (End X)

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

Equations

• CategoryTheory.End.mul X = { mul := fun (x y : CategoryTheory.End X) => CategoryTheory.CategoryStruct.comp y x }

def CategoryTheory.End.of {C : Type u} [CategoryStruct.{v, u} C] {X : C} (f : X ⟶ X) : End X

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

Equations

• CategoryTheory.End.of f = f

def CategoryTheory.End.asHom {C : Type u} [CategoryStruct.{v, u} C] {X : C} (f : End X) : X ⟶ X

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

Equations

• f.asHom = f

@[simp]

theorem CategoryTheory.End.one_def {C : Type u} [CategoryStruct.{v, u} C] {X : C} : 1 = CategoryStruct.id X

@[simp]

theorem CategoryTheory.End.mul_def {C : Type u} [CategoryStruct.{v, u} C] {X : C} (xs ys : End X) : xs * ys = CategoryStruct.comp ys xs

instance CategoryTheory.End.monoid {C : Type u} [Category.{v, u} C] {X : C} : Monoid (End X)

Endomorphisms of an object form a monoid

Equations

• CategoryTheory.End.monoid = Monoid.mk ⋯ ⋯ npowRecAuto ⋯ ⋯

instance CategoryTheory.End.mulActionRight {C : Type u} [Category.{v, u} C] {X Y : C} : MulAction (End Y) (X ⟶ Y)

Equations

• CategoryTheory.End.mulActionRight = MulAction.mk ⋯ ⋯

instance CategoryTheory.End.mulActionLeft {C : Type u} [Category.{v, u} C] {X : Cᵒᵖ} {Y : C} : MulAction (End X) (Opposite.unop X ⟶ Y)

Equations

• CategoryTheory.End.mulActionLeft = MulAction.mk ⋯ ⋯

theorem CategoryTheory.End.smul_right {C : Type u} [Category.{v, u} C] {X Y : C} {r : End Y} {f : X ⟶ Y} : r • f = CategoryStruct.comp f r

theorem CategoryTheory.End.smul_left {C : Type u} [Category.{v, u} C] {X : Cᵒᵖ} {Y : C} {r : End X} {f : Opposite.unop X ⟶ Y} : r • f = CategoryStruct.comp (Quiver.Hom.unop r) f

instance CategoryTheory.End.group {C : Type u} [Groupoid C] (X : C) : Group (End X)

In a groupoid, endomorphisms form a group

Equations

• CategoryTheory.End.group X = Group.mk ⋯

theorem CategoryTheory.isUnit_iff_isIso {C : Type u} [Category.{v, u} C] {X : C} (f : End X) : IsUnit f ↔ IsIso f

def CategoryTheory.Aut {C : Type u} [Category.{v, u} C] (X : C) : Type v

Automorphisms of an object in a category.

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

Equations

• CategoryTheory.Aut X = (X ≅ X)

theorem CategoryTheory.Aut.ext {C : Type u} [Category.{v, u} C] {X : C} {φ₁ φ₂ : Aut X} (h : φ₁.hom = φ₂.hom) : φ₁ = φ₂

instance CategoryTheory.Aut.inhabited {C : Type u} [Category.{v, u} C] (X : C) : Inhabited (Aut X)

Equations

• CategoryTheory.Aut.inhabited X = { default := CategoryTheory.Iso.refl X }

instance CategoryTheory.Aut.instGroup {C : Type u} [Category.{v, u} C] (X : C) : Group (Aut X)

Equations

• CategoryTheory.Aut.instGroup X = Group.mk ⋯

theorem CategoryTheory.Aut.Aut_mul_def {C : Type u} [Category.{v, u} C] (X : C) (f g : Aut X) : f * g = g ≪≫ f

theorem CategoryTheory.Aut.Aut_inv_def {C : Type u} [Category.{v, u} C] (X : C) (f : Aut X) : f⁻¹ = Iso.symm f

def CategoryTheory.Aut.unitsEndEquivAut {C : Type u} [Category.{v, u} C] (X : C) : (End X)ˣ ≃* Aut X

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.

def CategoryTheory.Aut.toEnd {C : Type u} [Category.{v, u} C] (X : C) : Aut X →* End X

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

Equations

• CategoryTheory.Aut.toEnd X = (Units.coeHom (CategoryTheory.End X)).comp ↑(CategoryTheory.Aut.unitsEndEquivAut X).symm

@[simp]

theorem CategoryTheory.Aut.toEnd_apply {C : Type u} [Category.{v, u} C] (X : C) (a✝ : Aut X) : (toEnd X) a✝ = ↑((unitsEndEquivAut X).symm a✝)

def CategoryTheory.Aut.autMulEquivOfIso {C : Type u} [Category.{v, u} C] {X Y : C} (h : X ≅ Y) : Aut X ≃* Aut Y

Isomorphisms induce isomorphisms of the automorphism group

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Functor.mapEnd {C : Type u} [Category.{v, u} C] (X : C) {D : Type u'} [Category.{v', u'} D] (f : Functor C D) : End X →* End (f.obj X)

f.map as a monoid hom between endomorphism monoids.

Equations

• CategoryTheory.Functor.mapEnd X f = { toFun := f.map, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem CategoryTheory.Functor.mapEnd_apply {C : Type u} [Category.{v, u} C] (X : C) {D : Type u'} [Category.{v', u'} D] (f : Functor C D) (a✝ : X ⟶ X) : (mapEnd X f) a✝ = f.map a✝

def CategoryTheory.Functor.mapAut {C : Type u} [Category.{v, u} C] (X : C) {D : Type u'} [Category.{v', u'} D] (f : Functor C D) : Aut X →* Aut (f.obj X)

f.mapIso as a group hom between automorphism groups.

Equations

• CategoryTheory.Functor.mapAut X f = { toFun := f.mapIso, map_one' := ⋯, map_mul' := ⋯ }

noncomputable def CategoryTheory.Functor.FullyFaithful.mulEquivEnd {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {f : Functor C D} (hf : f.FullyFaithful) (X : C) : End X ≃* End (f.obj X)

mulEquivEnd as an isomorphism between endomorphism monoids.

Equations

• hf.mulEquivEnd X = { toEquiv := hf.homEquiv, map_mul' := ⋯ }

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.mulEquivEnd_apply {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {f : Functor C D} (hf : f.FullyFaithful) (X : C) (a✝ : X ⟶ X) : (hf.mulEquivEnd X) a✝ = f.map a✝

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.mulEquivEnd_symm_apply {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {f : Functor C D} (hf : f.FullyFaithful) (X : C) (f✝ : f.obj X ⟶ f.obj X) : (hf.mulEquivEnd X).symm f✝ = hf.preimage f✝

noncomputable def CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {f : Functor C D} (hf : f.FullyFaithful) (X : C) : Aut X ≃* Aut (f.obj X)

mulEquivAut as an isomorphism between automorphism groups.

Equations

• hf.autMulEquivOfFullyFaithful X = { toEquiv := hf.isoEquiv, map_mul' := ⋯ }

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_symm_apply_inv {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {f : Functor C D} (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_apply_inv {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {f : Functor C D} (hf : f.FullyFaithful) (X : C) (i : X ≅ X) : ((hf.autMulEquivOfFullyFaithful X) i).inv = f.map i.inv

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_apply_hom {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {f : Functor C D} (hf : f.FullyFaithful) (X : C) (i : X ≅ X) : ((hf.autMulEquivOfFullyFaithful X) i).hom = f.map i.hom

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_symm_apply_hom {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {f : Functor C D} (hf : f.FullyFaithful) (X : C) (e : f.obj X ≅ f.obj X) : ((hf.autMulEquivOfFullyFaithful X).symm e).hom = hf.preimage e.hom