doc-next-gen

Mathlib.CategoryTheory.Endomorphism

Module docstring

{"# 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. "}

CategoryTheory.End definition
{C : Type u} [CategoryStruct.{v} C] (X : C)
Full source 
/-- Endomorphisms of an object in a category. Arguments order in multiplication agrees with
`Function.comp`, not with `CategoryTheory.CategoryStruct.comp`. -/
def End {C : Type u} [CategoryStruct.{v} C] (X : C) := X ⟶ X
Endomorphisms of an object in a category
Informal description
For an object $X$ in a category $C$, the type $\text{End}(X)$ consists of all endomorphisms of $X$, i.e., all morphisms from $X$ to itself. The multiplication operation on $\text{End}(X)$ is defined by composition of morphisms, with the order agreeing with standard function composition.
CategoryTheory.End.one instance
: One (End X)
Full source 
protected instance one : One (End X) := ⟨𝟙 X⟩
Identity Morphism as the Unit of Endomorphism Monoid
Informal description
For any object $X$ in a category $C$, the endomorphism monoid $\text{End}(X)$ has a distinguished identity element given by the identity morphism of $X$.
CategoryTheory.End.inhabited instance
: Inhabited (End X)
Full source 
protected instance inhabited : Inhabited (End X) := ⟨𝟙 X⟩
Endomorphism Monoid is Inhabited
Informal description
For any object $X$ in a category $C$, the endomorphism monoid $\text{End}(X)$ is inhabited (i.e., nonempty).
CategoryTheory.End.mul instance
: Mul (End X)
Full source 
/-- Multiplication of endomorphisms agrees with `Function.comp`, not with
`CategoryTheory.CategoryStruct.comp`. -/
protected instance mul : Mul (End X) := ⟨fun x y => y ≫ x⟩
Multiplication of Endomorphisms via Function Composition
Informal description
For any object $X$ in a category $C$, the endomorphisms $\text{End}(X)$ form a multiplicative monoid where the multiplication operation is given by composition of morphisms, with the order agreeing with standard function composition (i.e., $(f \cdot g)(x) = f(g(x))$).
CategoryTheory.End.of definition
(f : X ⟶ X) : End X
Full source 
/-- Assist the typechecker by expressing a morphism `X ⟶ X` as a term of `CategoryTheory.End X`. -/
def of (f : X ⟶ X) : End X := f
Endomorphism construction from a morphism
Informal description
The function maps a morphism $f \colon X \to X$ in a category to the corresponding endomorphism in $\text{End}(X)$, which is the type of all endomorphisms of $X$.
CategoryTheory.End.asHom definition
(f : End X) : X ⟶ X
Full source 
/-- Assist the typechecker by expressing an endomorphism `f : CategoryTheory.End X` as a term of
`X ⟶ X`. -/
def asHom (f : End X) : X ⟶ X := f
Endomorphism as morphism
Informal description
The function converts an endomorphism \( f \) of an object \( X \) in a category \( C \) (i.e., an element of \( \text{End}(X) \)) back into a morphism \( X \to X \).
CategoryTheory.End.one_def theorem
: (1 : End X) = 𝟙 X
Full source 
@[simp] -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11215): TODO: use `of`/`asHom`?
theorem one_def : (1 : End X) = 𝟙 X := rfl
Identity Element of Endomorphism Monoid Equals Identity Morphism
Informal description
The identity element of the endomorphism monoid $\text{End}(X)$ is equal to the identity morphism $\text{id}_X$ of the object $X$ in the category.
CategoryTheory.End.mul_def theorem
(xs ys : End X) : xs * ys = ys ≫ xs
Full source 
@[simp] -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11215): TODO: use `of`/`asHom`?
theorem mul_def (xs ys : End X) : xs * ys = ys ≫ xs := rfl
Composition as Multiplication in Endomorphism Monoid: $f \cdot g = g \circ f$
Informal description
For any two endomorphisms $f$ and $g$ of an object $X$ in a category $C$, the product $f \cdot g$ in the endomorphism monoid $\text{End}(X)$ is equal to the composition $g \circ f$ of morphisms in $C$.
CategoryTheory.End.monoid instance
{C : Type u} [Category.{v} C] {X : C} : Monoid (End X)
Full source 
/-- Endomorphisms of an object form a monoid -/
instance monoid {C : Type u} [Category.{v} C] {X : C} : Monoid (End X) where
  mul_one := Category.id_comp
  one_mul := Category.comp_id
  mul_assoc := fun x y z => (Category.assoc z y x).symm
Monoid Structure on Endomorphisms via Composition
Informal description
For any object $X$ in a category $C$, the endomorphisms $\text{End}(X)$ form a monoid under composition of morphisms, with the identity morphism as the unit.
CategoryTheory.End.mulActionRight instance
{X Y : C} : MulAction (End Y) (X ⟶ Y)
Full source 
instance mulActionRight {X Y : C} : MulAction (End Y) (X ⟶ Y) where
  smul r f := f ≫ r
  one_smul := Category.comp_id
  mul_smul _ _ _ := Eq.symm <| Category.assoc _ _ _
Right Action of Endomorphisms on Morphisms via Postcomposition
Informal description
For any objects $X$ and $Y$ in a category $C$, the set of morphisms from $X$ to $Y$ has a right multiplicative action by the endomorphisms of $Y$. This action is defined by postcomposition with endomorphisms of $Y$.
CategoryTheory.End.mulActionLeft instance
{X Y : C} : MulAction (End X)ᵐᵒᵖ (X ⟶ Y)
Full source 
instance mulActionLeft {X Y : C} : MulAction (End X)ᵐᵒᵖ (X ⟶ Y) where
  smul r f := r.unop ≫ f
  one_smul := Category.id_comp
  mul_smul _ _ _ := Category.assoc _ _ _
Left Action of Endomorphisms on Morphisms via Precomposition
Informal description
For any objects $X$ and $Y$ in a category $C$, the set of morphisms from $X$ to $Y$ has a left multiplicative action by the opposite monoid of endomorphisms of $X$. This action is defined by precomposition with endomorphisms of $X$.
CategoryTheory.End.smul_right theorem
{X Y : C} {r : End Y} {f : X ⟶ Y} : r • f = f ≫ r
Full source 
theorem smul_right {X Y : C} {r : End Y} {f : X ⟶ Y} : r • f = f ≫ r :=
  rfl
Right Scalar Multiplication of Endomorphisms via Postcomposition
Informal description
For any objects $X$ and $Y$ in a category $C$, given an endomorphism $r$ of $Y$ and a morphism $f : X \to Y$, the right scalar multiplication $r \bullet f$ is equal to the composition of $f$ with $r$, i.e., $r \bullet f = f \circ r$.
CategoryTheory.End.smul_left theorem
{X Y : C} {r : (End X)ᵐᵒᵖ} {f : X ⟶ Y} : r • f = r.unop ≫ f
Full source 
theorem smul_left {X Y : C} {r : (End X)ᵐᵒᵖ} {f : X ⟶ Y} : r • f = r.unop ≫ f :=
  rfl
Left Scalar Multiplication of Endomorphisms via Precomposition
Informal description
For any objects $X$ and $Y$ in a category $C$, given an endomorphism $r$ of $X$ (considered as an element of the opposite monoid $\text{End}(X)^\text{op}$) and a morphism $f : X \to Y$, the left scalar multiplication $r \bullet f$ is equal to the composition of $r$ with $f$, i.e., $r \bullet f = r \circ f$.
CategoryTheory.End.group instance
{C : Type u} [Groupoid.{v} C] (X : C) : Group (End X)
Full source 
/-- In a groupoid, endomorphisms form a group -/
instance group {C : Type u} [Groupoid.{v} C] (X : C) : Group (End X) where
  inv_mul_cancel := Groupoid.comp_inv
  inv := Groupoid.inv
Group Structure on Endomorphisms in a Groupoid
Informal description
For any object $X$ in a groupoid $C$, the endomorphisms $\text{End}(X)$ form a group under composition of morphisms.
CategoryTheory.isUnit_iff_isIso theorem
{C : Type u} [Category.{v} C] {X : C} (f : End X) : IsUnit (f : End X) ↔ IsIso f
Full source 
theorem isUnit_iff_isIso {C : Type u} [Category.{v} C] {X : C} (f : End X) :
    IsUnitIsUnit (f : End X) ↔ IsIso f :=
  ⟨fun h => { out := ⟨h.unit.inv, ⟨h.unit.inv_val, h.unit.val_inv⟩⟩ }, fun h =>
    ⟨⟨f, inv f, by simp, by simp⟩, rfl⟩⟩
Characterization of Units in Endomorphism Monoid: Isomorphism Equivalence
Informal description
For any endomorphism $f$ of an object $X$ in a category $C$, $f$ is a unit in the monoid $\text{End}(X)$ if and only if $f$ is an isomorphism (i.e., there exists an inverse morphism $f^{-1}$ such that $f \circ f^{-1} = \text{id}_X$ and $f^{-1} \circ f = \text{id}_X$).
CategoryTheory.Aut definition
(X : C)
Full source 
/-- Automorphisms of an object in a category.

The order of arguments in multiplication agrees with
`Function.comp`, not with `CategoryTheory.CategoryStruct.comp`.
-/
def Aut (X : C) := X ≅ X
Automorphism group of a category object
Informal description
The group of automorphisms of an object $X$ in a category $\mathcal{C}$, consisting of all isomorphisms from $X$ to itself. The multiplication operation in this group is given by composition of morphisms, with the order of composition matching function composition (i.e., $(f \circ g)(x) = f(g(x))$) rather than the usual categorical composition order.
CategoryTheory.Aut.ext theorem
{X : C} {φ₁ φ₂ : Aut X} (h : φ₁.hom = φ₂.hom) : φ₁ = φ₂
Full source 
@[ext]
lemma ext {X : C} {φ₁ φ₂ : Aut X} (h : φ₁.hom = φ₂.hom) : φ₁ = φ₂ :=
  Iso.ext h
Extensionality of Automorphisms via Homomorphism Equality
Informal description
For any two automorphisms $\varphi_1, \varphi_2$ of an object $X$ in a category $\mathcal{C}$, if their underlying homomorphisms are equal ($\varphi_1.\text{hom} = \varphi_2.\text{hom}$), then $\varphi_1 = \varphi_2$.
CategoryTheory.Aut.inhabited instance
: Inhabited (Aut X)
Full source 
protected instance inhabited : Inhabited (Aut X) := ⟨Iso.refl X⟩
Nonemptiness of the Automorphism Group
Informal description
For any object $X$ in a category $\mathcal{C}$, the automorphism group $\mathrm{Aut}(X)$ is nonempty.
CategoryTheory.Aut.instGroup instance
: Group (Aut X)
Full source 
instance : Group (Aut X) where
  one := Iso.refl X
  inv := Iso.symm
  mul x y := Iso.trans y x
  mul_assoc _ _ _ := (Iso.trans_assoc _ _ _).symm
  one_mul := Iso.trans_refl
  mul_one := Iso.refl_trans
  inv_mul_cancel := Iso.self_symm_id
Group Structure on Automorphisms of a Category Object
Informal description
For any object $X$ in a category $\mathcal{C}$, the automorphism group $\mathrm{Aut}(X)$ is a group under composition of morphisms, with the identity isomorphism as the neutral element and the inverse isomorphism as the group inverse.
CategoryTheory.Aut.Aut_mul_def theorem
(f g : Aut X) : f * g = g.trans f
Full source 
theorem Aut_mul_def (f g : Aut X) : f * g = g.trans f := rfl
Group Multiplication in Automorphism Group is Composition of Isomorphisms
Informal description
For any two automorphisms $f, g \in \mathrm{Aut}(X)$ of an object $X$ in a category $\mathcal{C}$, the group multiplication $f * g$ is equal to the composition of isomorphisms $g \circ f$.
CategoryTheory.Aut.Aut_inv_def theorem
(f : Aut X) : f⁻¹ = f.symm
Full source 
theorem Aut_inv_def (f : Aut X) : f⁻¹ = f.symm := rfl
Inverse of an automorphism equals its categorical inverse
Informal description
For any automorphism $f$ of an object $X$ in a category $\mathcal{C}$, the group inverse $f^{-1}$ is equal to the inverse isomorphism $f^{\mathrm{symm}}$.
CategoryTheory.Aut.unitsEndEquivAut definition
: (End X)ˣ ≃* Aut X
Full source 
/-- Units in the monoid of endomorphisms of an object
are (multiplicatively) equivalent to automorphisms of that object.
-/
def unitsEndEquivAut : (End X)ˣ(End X)ˣ ≃* Aut X where
  toFun f := ⟨f.1, f.2, f.4, f.3⟩
  invFun f := ⟨f.1, f.2, f.4, f.3⟩
  left_inv := fun ⟨_, _, _, _⟩ => rfl
  right_inv := fun ⟨_, _, _, _⟩ => rfl
  map_mul' f g := by cases f; cases g; rfl
Equivalence between invertible endomorphisms and automorphisms
Informal description
The multiplicative equivalence between the units of the endomorphism monoid $\text{End}(X)$ and the automorphism group $\text{Aut}(X)$ of an object $X$ in a category $\mathcal{C}$. Specifically, it maps each invertible endomorphism to its corresponding automorphism, and vice versa.
CategoryTheory.Aut.toEnd definition
(X : C) : Aut X →* End X
Full source 
/-- The inclusion of `Aut X` to `End X` as a monoid homomorphism. -/
@[simps!]
def toEnd (X : C) : AutAut X →* End X := (Units.coeHom (End X)).comp (Aut.unitsEndEquivAut X).symm
Inclusion of automorphisms into endomorphisms as a monoid homomorphism
Informal description
The monoid homomorphism that includes the automorphism group $\mathrm{Aut}(X)$ of an object $X$ in a category $\mathcal{C}$ into its endomorphism monoid $\mathrm{End}(X)$. This is constructed by composing the inverse of the multiplicative equivalence between invertible endomorphisms and automorphisms with the natural inclusion of units into the endomorphism monoid.
CategoryTheory.Aut.autMulEquivOfIso definition
{X Y : C} (h : X ≅ Y) : Aut X ≃* Aut Y
Full source 
/-- Isomorphisms induce isomorphisms of the automorphism group -/
def autMulEquivOfIso {X Y : C} (h : X ≅ Y) : AutAut X ≃* Aut Y where
  toFun x := { hom := h.inv ≫ x.hom ≫ h.hom, inv := h.inv ≫ x.inv ≫ h.hom }
  invFun y := { hom := h.hom ≫ y.hom ≫ h.inv, inv := h.hom ≫ y.inv ≫ h.inv }
  left_inv _ := by aesop_cat
  right_inv _ := by aesop_cat
  map_mul' := by simp [Aut_mul_def]
Isomorphism-induced group isomorphism of automorphism groups
Informal description
Given an isomorphism $h : X \cong Y$ between objects $X$ and $Y$ in a category $\mathcal{C}$, the function constructs a group isomorphism between the automorphism groups $\mathrm{Aut}(X)$ and $\mathrm{Aut}(Y)$. Specifically, it maps an automorphism $x \in \mathrm{Aut}(X)$ to the automorphism $h^{-1} \circ x \circ h \in \mathrm{Aut}(Y)$, and conversely maps $y \in \mathrm{Aut}(Y)$ to $h \circ y \circ h^{-1} \in \mathrm{Aut}(X)$. This construction preserves the group structure, i.e., it respects composition of automorphisms.
CategoryTheory.Functor.mapEnd definition
: End X →* End (f.obj X)
Full source 
/-- `f.map` as a monoid hom between endomorphism monoids. -/
@[simps]
def mapEnd : EndEnd X →* End (f.obj X) where
  toFun := f.map
  map_mul' x y := f.map_comp y x
  map_one' := f.map_id X
Functorial action on endomorphism monoids
Informal description
Given a functor $f$ in a category, the function maps an endomorphism $\varphi$ of an object $X$ to the endomorphism $f(\varphi)$ of the object $f(X)$, preserving composition and identity. This defines a monoid homomorphism from the endomorphism monoid of $X$ to the endomorphism monoid of $f(X)$.
CategoryTheory.Functor.mapAut definition
: Aut X →* Aut (f.obj X)
Full source 
/-- `f.mapIso` as a group hom between automorphism groups. -/
def mapAut : AutAut X →* Aut (f.obj X) where
  toFun := f.mapIso
  map_mul' x y := f.mapIso_trans y x
  map_one' := f.mapIso_refl X
Functorial action on automorphism groups
Informal description
The group homomorphism from the automorphism group of an object $X$ in a category $\mathcal{C}$ to the automorphism group of the object $f(X)$ in a category $\mathcal{D}$, induced by a functor $f \colon \mathcal{C} \to \mathcal{D}$. The homomorphism maps each automorphism $\varphi \in \mathrm{Aut}(X)$ to $f(\varphi) \in \mathrm{Aut}(f(X))$, preserving composition and identity. Specifically: - The underlying function is given by $f.\mathrm{mapIso}$. - It satisfies $f.\mathrm{mapAut}(\varphi \circ \psi) = f.\mathrm{mapAut}(\varphi) \circ f.\mathrm{mapAut}(\psi)$ for all $\varphi, \psi \in \mathrm{Aut}(X)$ (using $f.\mathrm{mapIso\_trans}$). - It maps the identity automorphism to the identity automorphism (using $f.\mathrm{mapIso\_refl}$).
CategoryTheory.Functor.FullyFaithful.mulEquivEnd definition
(X : C) : End X ≃* End (f.obj X)
Full source 
/-- `mulEquivEnd` as an isomorphism between endomorphism monoids. -/
@[simps!]
noncomputable def mulEquivEnd (X : C) :
    EndEnd X ≃* End (f.obj X) where
  toEquiv := hf.homEquiv
  __ := mapEnd X f
Isomorphism of endomorphism monoids induced by a fully faithful functor
Informal description
For a fully faithful functor $f$ in a category $C$ and an object $X$ in $C$, the function `mulEquivEnd` is an isomorphism between the monoid of endomorphisms of $X$ and the monoid of endomorphisms of $f(X)$. This isomorphism preserves the monoid structure, where the underlying equivalence is given by the hom-set bijection induced by the fully faithful functor $f$.
CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful definition
(X : C) : Aut X ≃* Aut (f.obj X)
Full source 
/-- `mulEquivAut` as an isomorphism between automorphism groups. -/
@[simps!]
noncomputable def autMulEquivOfFullyFaithful (X : C) :
    AutAut X ≃* Aut (f.obj X) where
  toEquiv := hf.isoEquiv
  __ := mapAut X f
Isomorphism of automorphism groups induced by a fully faithful functor
Informal description
Given a fully faithful functor $f \colon \mathcal{C} \to \mathcal{D}$ and an object $X$ in $\mathcal{C}$, the function `autMulEquivOfFullyFaithful` is an isomorphism between the automorphism group of $X$ and the automorphism group of $f(X)$. This isomorphism preserves the group structure, where the underlying equivalence is given by the bijection between hom-sets induced by the fully faithful functor $f$.