Documentation

Mathlib.CategoryTheory.Endomorphism

Endomorphisms #

Definition and basic properties of endomorphisms and automorphisms of an object in a category.

For each X : C, we define a monoid CategoryTheory.End X which is a 1-field structure that is equipped with a bijection with X ⟶ X. Similarly, we define the group CategoryTheory.Aut X, which is equipped with a bijection with X ≅ X.

source
structure CategoryTheory.End {C : Type u} [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.

  • of :: (
    • asHom : X ⟶ X

      the underlying morphism of an endomorphism

  • )
Instances For
    source
    theorem CategoryTheory.End.ext {C : Type u} {inst✝ : CategoryStruct.{v, u} C} {X : C} {x y : End X} (asHom : x.asHom = y.asHom) :
    x = y
    source
    theorem CategoryTheory.End.ext_iff {C : Type u} {inst✝ : CategoryStruct.{v, u} C} {X : C} {x y : End X} :
    x = y ↔ x.asHom = y.asHom
    source
    @[implicit_reducible]
    def CategoryTheory.End.homEquiv {C : Type u} [CategoryStruct.{v, u} C] {X : C} :
    End X ≃ (X ⟶ X)

    The bijection End X ≃ (X ⟶ X).

    Instances For
      source
      @[simp]
      theorem CategoryTheory.End.homEquiv_symm_apply_asHom {C : Type u} [CategoryStruct.{v, u} C] {X : C} (asHom : X ⟶ X) :
      (homEquiv.symm asHom).asHom = asHom
      source
      @[simp]
      theorem CategoryTheory.End.homEquiv_apply {C : Type u} [CategoryStruct.{v, u} C] {X : C} (self : End X) :
      homEquiv self = self.asHom
      source
      @[instance_reducible]
      instance CategoryTheory.End.instOne {C : Type u} [CategoryStruct.{v, u} C] (X : C) :
      One (End X)
      source
      @[simp]
      theorem CategoryTheory.End.one_asHom {C : Type u} [CategoryStruct.{v, u} C] (X : C) :
      asHom 1 = CategoryStruct.id X
      source
      @[instance_reducible]
      instance CategoryTheory.End.inhabited {C : Type u} [CategoryStruct.{v, u} C] (X : C) :
      Inhabited (End X)
      source
      @[instance_reducible]
      instance CategoryTheory.End.instMul {C : Type u} [CategoryStruct.{v, u} C] (X : C) :
      Mul (End X)

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

      source
      @[simp]
      theorem CategoryTheory.End.mul_asHom {C : Type u} [CategoryStruct.{v, u} C] (X : C) (f g : End X) :
      (f * g).asHom = CategoryStruct.comp g.asHom f.asHom
      source
      @[deprecated CategoryTheory.End.one_asHom (since := "2026-09-12")]
      theorem CategoryTheory.End.one_def {C : Type u} [CategoryStruct.{v, u} C] (X : C) :
      asHom 1 = CategoryStruct.id X

      Alias of CategoryTheory.End.one_asHom.

      source
      @[deprecated CategoryTheory.End.mul_asHom (since := "2026-09-12")]
      theorem CategoryTheory.End.mul_def {C : Type u} [CategoryStruct.{v, u} C] (X : C) (f g : End X) :
      (f * g).asHom = CategoryStruct.comp g.asHom f.asHom

      Alias of CategoryTheory.End.mul_asHom.

      source
      @[instance_reducible]
      instance CategoryTheory.End.monoid {C : Type u} [Category.{v, u} C] {X : C} :
      Monoid (End X)

      Endomorphisms of an object form a monoid

      source
      @[instance_reducible]
      instance CategoryTheory.End.instSMulHom {C : Type u} [Category.{v, u} C] {X Y : C} :
      SMul (End Y) (X ⟶ Y)
      source
      @[instance_reducible]
      instance CategoryTheory.End.instSMulMulOppositeHom {C : Type u} [Category.{v, u} C] {X Y : C} :
      SMul (End X)ᵐᵒᵖ (X ⟶ Y)
      source
      theorem CategoryTheory.End.smul_right {C : Type u} [Category.{v, u} C] {X Y : C} {r : End Y} {f : X ⟶ Y} :
      r • f = CategoryStruct.comp f r.asHom
      source
      theorem CategoryTheory.End.smul_left {C : Type u} [Category.{v, u} C] {X Y : C} {r : (End X)ᵐᵒᵖ} {f : X ⟶ Y} :
      r • f = CategoryStruct.comp (MulOpposite.unop r).asHom f
      source
      @[instance_reducible]
      instance CategoryTheory.End.mulActionRight {C : Type u} [Category.{v, u} C] {X Y : C} :
      MulAction (End Y) (X ⟶ Y)
      source
      @[instance_reducible]
      instance CategoryTheory.End.mulActionLeft {C : Type u} [Category.{v, u} C] {X Y : C} :
      MulAction (End X)ᵐᵒᵖ (X ⟶ Y)
      source
      @[instance_reducible]
      instance CategoryTheory.End.group {C : Type u} [Groupoid C] (X : C) :
      Group (End X)

      In a groupoid, endomorphisms form a group

      source
      theorem CategoryTheory.isUnit_iff_isIso {C : Type u} [Category.{v, u} C] {X : C} (f : End X) :
      IsUnit f ↔ IsIso f.asHom
      source
      structure CategoryTheory.Aut {C : Type u} [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.

      • of :: (
        • asIso : X ≅ X

          the underlying isomorphism of an automorphism

      • )
      Instances For
        source
        theorem CategoryTheory.Aut.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {X : C} {x y : Aut X} :
        x = y ↔ x.asIso = y.asIso
        source
        theorem CategoryTheory.Aut.ext {C : Type u} {inst✝ : Category.{v, u} C} {X : C} {x y : Aut X} (asIso : x.asIso = y.asIso) :
        x = y
        source
        @[implicit_reducible]
        def CategoryTheory.Aut.isoEquiv {C : Type u} [Category.{v, u} C] {X : C} :
        Aut X ≃ (X ≅ X)

        The bijection Aut X ≃ (X ≅ X).

        Instances For
          source
          @[simp]
          theorem CategoryTheory.Aut.isoEquiv_symm_apply_asIso {C : Type u} [Category.{v, u} C] {X : C} (asIso : X ≅ X) :
          (isoEquiv.symm asIso).asIso = asIso
          source
          @[simp]
          theorem CategoryTheory.Aut.isoEquiv_apply {C : Type u} [Category.{v, u} C] {X : C} (self : Aut X) :
          isoEquiv self = self.asIso
          source
          @[instance_reducible]
          instance CategoryTheory.Aut.inhabited {C : Type u} [Category.{v, u} C] (X : C) :
          Inhabited (Aut X)
          source
          @[instance_reducible]
          instance CategoryTheory.Aut.instOne {C : Type u} [Category.{v, u} C] (X : C) :
          One (Aut X)
          source
          @[simp]
          theorem CategoryTheory.Aut.one_asIso {C : Type u} [Category.{v, u} C] (X : C) :
          asIso 1 = Iso.refl X
          source
          @[instance_reducible]
          instance CategoryTheory.Aut.instInv {C : Type u} [Category.{v, u} C] (X : C) :
          Inv (Aut X)
          source
          @[simp]
          theorem CategoryTheory.Aut.inv_asIso {C : Type u} [Category.{v, u} C] (X : C) (e : Aut X) :
          e⁻¹.asIso = e.asIso.symm
          source
          @[instance_reducible]
          instance CategoryTheory.Aut.instMul {C : Type u} [Category.{v, u} C] (X : C) :
          Mul (Aut X)
          source
          @[simp]
          theorem CategoryTheory.Aut.mul_asIso {C : Type u} [Category.{v, u} C] (X : C) (x y : Aut X) :
          (x * y).asIso = y.asIso ≪≫ x.asIso
          source
          @[instance_reducible]
          instance CategoryTheory.Aut.instGroup {C : Type u} [Category.{v, u} C] (X : C) :
          Group (Aut X)
          source
          @[deprecated CategoryTheory.Aut.mul_asIso (since := "2026-09-12")]
          theorem CategoryTheory.Aut.Aut_mul_def {C : Type u} [Category.{v, u} C] (X : C) (x y : Aut X) :
          (x * y).asIso = y.asIso ≪≫ x.asIso

          Alias of CategoryTheory.Aut.mul_asIso.

          source
          @[deprecated CategoryTheory.Aut.inv_asIso (since := "2026-09-12")]
          theorem CategoryTheory.Aut.Aut_inv_def {C : Type u} [Category.{v, u} C] (X : C) (e : Aut X) :
          e⁻¹.asIso = e.asIso.symm

          Alias of CategoryTheory.Aut.inv_asIso.

          source
          def CategoryTheory.Aut.toEnd {C : Type u} [Category.{v, u} C] {X : C} :
          Aut X →* End X

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

          Instances For
            source
            @[simp]
            theorem CategoryTheory.Aut.toEnd_apply_asHom {C : Type u} [Category.{v, u} C] {X : C} (e : Aut X) :
            (toEnd e).asHom = e.asIso.hom
            source
            def CategoryTheory.Aut.unitsEndEquivAut {C : Type u} [Category.{v, u} C] (X : C) :
            (End X)ˣ ≃* Aut X

            Units in the monoid of endomorphisms of an object are (multiplicatively) equivalent to automorphisms of that object.

            Instances For
              source
              @[simp]
              theorem CategoryTheory.Aut.unitsEndEquivAut_apply_asIso_hom {C : Type u} [Category.{v, u} C] (X : C) (f : (End X)ˣ) :
              ((unitsEndEquivAut X) f).asIso.hom = (↑f).asHom
              source
              @[simp]
              theorem CategoryTheory.Aut.val_unitsEndEquivAut_symm_apply_asHom {C : Type u} [Category.{v, u} C] (X : C) (f : Aut X) :
              (↑((unitsEndEquivAut X).symm f)).asHom = f.asIso.hom
              source
              @[simp]
              theorem CategoryTheory.Aut.unitsEndEquivAut_apply_asIso_inv {C : Type u} [Category.{v, u} C] (X : C) (f : (End X)ˣ) :
              ((unitsEndEquivAut X) f).asIso.inv = f.inv.asHom
              source
              @[simp]
              theorem CategoryTheory.Aut.val_inv_unitsEndEquivAut_symm_apply_asHom {C : Type u} [Category.{v, u} C] (X : C) (f : Aut X) :
              (↑((unitsEndEquivAut X).symm f)⁻¹).asHom = f.asIso.inv
              source
              def CategoryTheory.Aut.autMulEquivOfIso {C : Type u} [Category.{v, u} C] {X Y : C} (h : X ≅ Y) :
              Aut X ≃* Aut Y

              Isomorphisms induce isomorphisms of the automorphism group

              Instances For
                source
                @[simp]
                theorem CategoryTheory.Aut.autMulEquivOfIso_apply_asIso {C : Type u} [Category.{v, u} C] {X Y : C} (h : X ≅ Y) (e : Aut X) :
                ((autMulEquivOfIso h) e).asIso = h.symm ≪≫ e.asIso ≪≫ h
                source
                @[simp]
                theorem CategoryTheory.Aut.autMulEquivOfIso_symm_apply_asIso {C : Type u} [Category.{v, u} C] {X Y : C} (h : X ≅ Y) (e : Aut Y) :
                ((autMulEquivOfIso h).symm e).asIso = h ≪≫ e.asIso ≪≫ h.symm
                source
                @[implicit_reducible]
                def CategoryTheory.Functor.mapEnd {C : Type u} [Category.{v, u} C] (X : C) {D : Type u'} [Category.{v', u'} D] (f : Functor C D) :
                End X →* End (f.obj X)

                f.map as a monoid hom between endomorphism monoids.

                Instances For
                  source
                  @[simp]
                  theorem CategoryTheory.Functor.mapEnd_apply_asHom {C : Type u} [Category.{v, u} C] (X : C) {D : Type u'} [Category.{v', u'} D] (f : Functor C D) (e : End X) :
                  ((mapEnd X f) e).asHom = f.map e.asHom
                  source
                  @[implicit_reducible]
                  def CategoryTheory.Functor.mapAut {C : Type u} [Category.{v, u} C] (X : C) {D : Type u'} [Category.{v', u'} D] (f : Functor C D) :
                  Aut X →* Aut (f.obj X)

                  f.mapIso as a group hom between automorphism groups.

                  Instances For
                    source
                    @[simp]
                    theorem CategoryTheory.Functor.mapAut_apply_asIso {C : Type u} [Category.{v, u} C] (X : C) {D : Type u'} [Category.{v', u'} D] (f : Functor C D) (e : Aut X) :
                    ((mapAut X f) e).asIso = f.mapIso e.asIso
                    source
                    noncomputable def CategoryTheory.Functor.FullyFaithful.mulEquivEnd {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {f : Functor C D} (hf : f.FullyFaithful) (X : C) :
                    End X ≃* End (f.obj X)

                    mulEquivEnd as an isomorphism between endomorphism monoids.

                    Instances For
                      source
                      @[simp]
                      theorem CategoryTheory.Functor.FullyFaithful.mulEquivEnd_symm_apply_asHom {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {f : Functor C D} (hf : f.FullyFaithful) (X : C) (a✝ : End (f.obj X)) :
                      ((hf.mulEquivEnd X).symm a✝).asHom = hf.preimage a✝.asHom
                      source
                      @[simp]
                      theorem CategoryTheory.Functor.FullyFaithful.mulEquivEnd_apply_asHom {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {f : Functor C D} (hf : f.FullyFaithful) (X : C) (a✝ : End X) :
                      ((hf.mulEquivEnd X) a✝).asHom = f.map a✝.asHom
                      source
                      noncomputable def CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {f : Functor C D} (hf : f.FullyFaithful) (X : C) :
                      Aut X ≃* Aut (f.obj X)

                      mulEquivAut as an isomorphism between automorphism groups.

                      Instances For
                        source
                        @[simp]
                        theorem CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_symm_apply_asIso_inv {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {f : Functor C D} (hf : f.FullyFaithful) (X : C) (a✝ : Aut (f.obj X)) :
                        ((hf.autMulEquivOfFullyFaithful X).symm a✝).asIso.inv = hf.preimage a✝.asIso.inv
                        source
                        @[simp]
                        theorem CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_apply_asIso_inv {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {f : Functor C D} (hf : f.FullyFaithful) (X : C) (a✝ : Aut X) :
                        ((hf.autMulEquivOfFullyFaithful X) a✝).asIso.inv = f.map a✝.asIso.inv
                        source
                        @[simp]
                        theorem CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_symm_apply_asIso_hom {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {f : Functor C D} (hf : f.FullyFaithful) (X : C) (a✝ : Aut (f.obj X)) :
                        ((hf.autMulEquivOfFullyFaithful X).symm a✝).asIso.hom = hf.preimage a✝.asIso.hom
                        source
                        @[simp]
                        theorem CategoryTheory.Functor.FullyFaithful.autMulEquivOfFullyFaithful_apply_asIso_hom {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] {f : Functor C D} (hf : f.FullyFaithful) (X : C) (a✝ : Aut X) :
                        ((hf.autMulEquivOfFullyFaithful X) a✝).asIso.hom = f.map a✝.asIso.hom
                        source
                        def CategoryTheory.InducedCategory.endEquiv {C : Type u} [Category.{v, u} C] {D : Type u_1} {F : D → C} {X : InducedCategory C F} :
                        End X ≃* End (F X)

                        The multiplicative bijection End X ≃* End (F X) when X : InducedCategory C F.

                        Instances For
                          source
                          @[simp]
                          theorem CategoryTheory.InducedCategory.endEquiv_apply_asHom {C : Type u} [Category.{v, u} C] {D : Type u_1} {F : D → C} {X : InducedCategory C F} (a✝ : End X) :
                          (endEquiv a✝).asHom = a✝.asHom.hom
                          source
                          @[simp]
                          theorem CategoryTheory.InducedCategory.endEquiv_symm_apply_asHom_hom {C : Type u} [Category.{v, u} C] {D : Type u_1} {F : D → C} {X : InducedCategory C F} (a✝ : End (F X)) :
                          (endEquiv.symm a✝).asHom.hom = a✝.asHom