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

• CategoryTheory.End.asHom f = 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

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

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

Equations

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

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

Equations

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

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 r.unop 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 (_ : ∀ (f : X ⟶ X), CategoryTheory.CategoryStruct.comp f (CategoryTheory.Groupoid.inv f) = CategoryTheory.CategoryStruct.id X)

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

Equations

• CategoryTheory.Aut.instGroupAut X = Group.mk (_ : ∀ (α : X ≅ X), α ≪≫ α.symm = CategoryTheory.Iso.refl X)

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⁻¹ = f.symm

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 = ↑((MulEquiv.symm (CategoryTheory.Aut.unitsEndEquivAut X)) 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 = MonoidHom.comp (Units.coeHom (CategoryTheory.End X)) ↑(MulEquiv.symm (CategoryTheory.Aut.unitsEndEquivAut X))

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.toPrefunctor.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.toPrefunctor.obj X)

f.map as a monoid hom between endomorphism monoids.

Equations

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

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.toPrefunctor.obj X)

f.mapIso as a group hom between automorphism groups.

Equations

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

@[simp]

theorem CategoryTheory.Functor.mulEquivOfFullyFaithful_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) {D : Type u'} [CategoryTheory.Category.{v', u'} D] (f : CategoryTheory.Functor C D) [CategoryTheory.Full f✝] [CategoryTheory.Faithful f✝] (f : f✝.toPrefunctor.obj X ⟶ f✝.toPrefunctor.obj X) : (MulEquiv.symm (CategoryTheory.Functor.mulEquivOfFullyFaithful X f✝)) f = f✝.preimage f

@[simp]

theorem CategoryTheory.Functor.mulEquivOfFullyFaithful_apply {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) {D : Type u'} [CategoryTheory.Category.{v', u'} D] (f : CategoryTheory.Functor C D) [CategoryTheory.Full f✝] [CategoryTheory.Faithful f✝] (f : X ⟶ X) : (CategoryTheory.Functor.mulEquivOfFullyFaithful X f✝) f = f✝.toPrefunctor.map f

def CategoryTheory.Functor.mulEquivOfFullyFaithful {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) {D : Type u'} [CategoryTheory.Category.{v', u'} D] (f : CategoryTheory.Functor C D) [CategoryTheory.Full f] [CategoryTheory.Faithful f] : CategoryTheory.End X ≃* CategoryTheory.End (f.toPrefunctor.obj X)

equivOfFullyFaithful f as an isomorphism between endomorphism monoids.

Equations

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

@[simp]

theorem CategoryTheory.Functor.autMulEquivOfFullyFaithful_symm_apply_inv {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) {D : Type u'} [CategoryTheory.Category.{v', u'} D] (f : CategoryTheory.Functor C D) [CategoryTheory.Full f✝] [CategoryTheory.Faithful f✝] (f : f✝.toPrefunctor.obj X ≅ f✝.toPrefunctor.obj X) : ((MulEquiv.symm (CategoryTheory.Functor.autMulEquivOfFullyFaithful X f✝)) f).inv = f✝.preimage f.inv

@[simp]

theorem CategoryTheory.Functor.autMulEquivOfFullyFaithful_apply_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) {D : Type u'} [CategoryTheory.Category.{v', u'} D] (f : CategoryTheory.Functor C D) [CategoryTheory.Full f✝] [CategoryTheory.Faithful f✝] (f : X ≅ X) : ((CategoryTheory.Functor.autMulEquivOfFullyFaithful X f✝) f).hom = f✝.toPrefunctor.map f.hom

@[simp]

theorem CategoryTheory.Functor.autMulEquivOfFullyFaithful_symm_apply_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) {D : Type u'} [CategoryTheory.Category.{v', u'} D] (f : CategoryTheory.Functor C D) [CategoryTheory.Full f✝] [CategoryTheory.Faithful f✝] (f : f✝.toPrefunctor.obj X ≅ f✝.toPrefunctor.obj X) : ((MulEquiv.symm (CategoryTheory.Functor.autMulEquivOfFullyFaithful X f✝)) f).hom = f✝.preimage f.hom

@[simp]

theorem CategoryTheory.Functor.autMulEquivOfFullyFaithful_apply_inv {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) {D : Type u'} [CategoryTheory.Category.{v', u'} D] (f : CategoryTheory.Functor C D) [CategoryTheory.Full f✝] [CategoryTheory.Faithful f✝] (f : X ≅ X) : ((CategoryTheory.Functor.autMulEquivOfFullyFaithful X f✝) f).inv = f✝.toPrefunctor.map f.inv

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

isoEquivOfFullyFaithful f as an isomorphism between automorphism groups.

Equations

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