Documentation

Mathlib.CategoryTheory.Endomorphism

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.

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

Equations

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

Equations

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

Equations
  • f.asHom = f

Endomorphisms of an object form a monoid

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

In a groupoid, endomorphisms form a group

Equations

Automorphisms of an object in a category.

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

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

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.

Isomorphisms induce isomorphisms of the automorphism group

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

f.map as a monoid hom between endomorphism monoids.

Equations

f.mapIso as a group hom between automorphism groups.

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

mulEquivEnd as an isomorphism between endomorphism monoids.

Equations
  • hf.mulEquivEnd X = { toEquiv := hf.homEquiv, map_mul' := }
@[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
@[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_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_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

mulEquivAut as an isomorphism between automorphism groups.

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