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.

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

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

@[reducible, inline]

abbrev 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.

@[reducible, inline]

abbrev 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.

@[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

theorem CategoryTheory.End.ext {C : Type u} [CategoryStruct.{v, u} C] {X : C} {x y : End X} (h : x.asHom = y.asHom) : x = y

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

Endomorphisms of an object form a monoid

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

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

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 Y : C} {r : (End X)ᵐᵒᵖ} {f : X ⟶ Y} : r • f = CategoryStruct.comp (MulOpposite.unop r) f

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

In a groupoid, endomorphisms form a group

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.

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

theorem CategoryTheory.Aut.ext_iff {C : Type u} [Category.{v, u} C] {X : C} {φ₁ φ₂ : Aut X} : φ₁ = φ₂ ↔ φ₁.hom = φ₂.hom

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

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

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.

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.

@[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

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.

@[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.

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.

@[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✝

@[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✝

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.

@[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

@[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_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_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

def CategoryTheory.InducedCategory.endEquiv {C : Type u} [Category.{v, u} C] {D : Type u_1} {F : D → C} {X : InducedCategory C F} : End X ≃* End (F X)

The multiplicative bijection End X ≃* End (F X) when X : InducedCategory C F.

@[simp]

theorem CategoryTheory.InducedCategory.endEquiv_symm_apply_hom {C : Type u} [Category.{v, u} C] {D : Type u_1} {F : D → C} {X : InducedCategory C F} (f : F X ⟶ F X) : (endEquiv.symm f).hom = f

@[simp]

theorem CategoryTheory.InducedCategory.endEquiv_apply {C : Type u} [Category.{v, u} C] {D : Type u_1} {F : D → C} {X : InducedCategory C F} (f : X ⟶ X) : endEquiv f = f.hom