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

Equations

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

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

Equations

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

instance CategoryTheory.End.mul {C : Type u} [CategoryTheory.CategoryStruct.{v, u} C] (X : C) : Mul (CategoryTheory.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} [CategoryTheory.CategoryStruct.{v, u} C] {X : C} (f : X ⟶ X) : CategoryTheory.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} [CategoryTheory.CategoryStruct.{v, u} C] {X : C} (f : CategoryTheory.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} [CategoryTheory.CategoryStruct.{v, u} C] {X : C} : 1 = CategoryTheory.CategoryStruct.id X

@[simp]

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

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

Endomorphisms of an object form a monoid

Equations

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

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

Equations

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

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

Equations

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

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

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

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

In a groupoid, endomorphisms form a group

Equations

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

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

def CategoryTheory.Aut {C : Type u} [CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {X : C} {φ₁ : CategoryTheory.Aut X} {φ₂ : CategoryTheory.Aut X} (h : φ₁.hom = φ₂.hom) : φ₁ = φ₂

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

Equations

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

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

Equations

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

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

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

def CategoryTheory.Aut.unitsEndEquivAut {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : (CategoryTheory.End X)ˣ ≃* CategoryTheory.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.

@[simp]

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

def CategoryTheory.Aut.toEnd {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : CategoryTheory.Aut X →* CategoryTheory.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

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

Isomorphisms induce isomorphisms of the automorphism group

Equations

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

@[simp]

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

def CategoryTheory.Functor.mapEnd {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) {D : Type u'} [CategoryTheory.Category.{v', u'} D] (f : CategoryTheory.Functor C D) : CategoryTheory.End X →* CategoryTheory.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' := ⋯ }

def CategoryTheory.Functor.mapAut {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) {D : Type u'} [CategoryTheory.Category.{v', u'} D] (f : CategoryTheory.Functor C D) : CategoryTheory.Aut X →* CategoryTheory.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' := ⋯ }

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.mulEquivEnd_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {f : CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {f : CategoryTheory.Functor C D} (hf : f.FullyFaithful) (X : C) : ∀ (a : X ⟶ X), (hf.mulEquivEnd X) a = f.map a

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

mulEquivEnd as an isomorphism between endomorphism monoids.

Equations

• hf.mulEquivEnd X = let __spread.0 := CategoryTheory.Functor.mapEnd X f; { toEquiv := hf.homEquiv, map_mul' := ⋯ }

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_apply_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {f : CategoryTheory.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_symm_apply_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {f : CategoryTheory.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_symm_apply_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {f : CategoryTheory.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_apply_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {f : CategoryTheory.Functor C D} (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} [CategoryTheory.Category.{v, u} C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] {f : CategoryTheory.Functor C D} (hf : f.FullyFaithful) (X : C) : CategoryTheory.Aut X ≃* CategoryTheory.Aut (f.obj X)

mulEquivAut as an isomorphism between automorphism groups.

Equations

• hf.autMulEquivOfFullyFaithful X = let __spread.0 := CategoryTheory.Functor.mapAut X f; { toEquiv := hf.isoEquiv, map_mul' := ⋯ }