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.

Instances For

    Multiplication of endomorphisms agrees with Function.comp, not with CategoryTheory.CategoryStruct.comp.

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

    Instances For

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

      Instances For

        Endomorphisms of an object form a monoid

        In a groupoid, endomorphisms form a group

        Automorphisms of an object in a category.

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

        Instances For
          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.

          Instances For

            Isomorphisms induce isomorphisms of the automorphism group

            Instances For

              f.map as a monoid hom between endomorphism monoids.

              Instances For

                f.mapIso as a group hom between automorphism groups.

                Instances For