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

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

    Equations
    Instances For

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

      Equations
      • f.asHom = f
      Instances For

        Endomorphisms of an object form a monoid

        Equations
        • CategoryTheory.End.monoid = Monoid.mk npowRec
        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
        Instances For
          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.
          Instances For

            The inclusion of Aut X to End X as a monoid homomorphism.

            Equations
            Instances For

              Isomorphisms induce isomorphisms of the automorphism group

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

                f.map as a monoid hom between endomorphism monoids.

                Equations
                Instances For

                  f.mapIso as a group hom between automorphism groups.

                  Equations
                  Instances For
                    @[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' := }
                    Instances For
                      @[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' := }
                      Instances For