The constructor End.of and the algebraic structure of End X

Mathlib describes the monoid, additive group and module structures on CategoryTheory.End X through the projection End.asHom. This file records the same compatibilities for the constructor End.of : (X ⟶ X) → End X: it sends 𝟙 X to 1, a composite f ≫ g to the product End.of g * End.of f, and sums, differences, negatives, zero and scalar multiples to the corresponding operations in End X. As simp lemmas they push End.of inside expressions built from morphisms X ⟶ X, so that algebra maps out of End X can then be applied termwise. We also compute the structure map of an R-linear category, (algebraMap R (End X) r).asHom = r • 𝟙 X.

The native precomposition action of (End X)ᵐᵒᵖ on X ⟶ Y respects the ground scalar tower.

When a scalar multiple r • 𝟙 of the identity is invertible, its inverse commutes with every morphism (CategoryTheory.Linear.comp_inv_smul_id), and an R-linear functor keeps it invertible (CategoryTheory.Functor.isIso_smul_id_obj). For r a natural number or an integer these apply in every preadditive category, through Mathlib's ℕ- and ℤ-linear structures.

An additive linear functor induces an algebra homomorphism on endomorphisms, Functor.mapEndAlgHom, which is injective when the functor is faithful and bijective when the functor is bijective on the object's endomorphisms.

@[simp]

theorem CategoryTheory.End.of_id {C : Type u} [Category.{v, u} C] {X : C} : { asHom := CategoryStruct.id X } = 1

End.of sends the identity to 1.

@[simp]

theorem CategoryTheory.End.of_comp {C : Type u} [Category.{v, u} C] {X : C} (f g : X ⟶ X) : { asHom := CategoryStruct.comp f g } = { asHom := g } * { asHom := f }

End.of sends a composite to the product in the opposite order, since multiplication in End X agrees with function composition.

@[simp]

theorem CategoryTheory.End.of_zero {C : Type u} [Category.{v, u} C] {X : C} [Preadditive C] : { asHom := 0 } = 0

End.of sends the zero morphism to 0.

@[simp]

theorem CategoryTheory.End.of_add {C : Type u} [Category.{v, u} C] {X : C} [Preadditive C] (f g : X ⟶ X) : { asHom := f + g } = { asHom := f } + { asHom := g }

End.of is additive.

@[simp]

theorem CategoryTheory.End.of_neg {C : Type u} [Category.{v, u} C] {X : C} [Preadditive C] (f : X ⟶ X) : { asHom := -f } = -{ asHom := f }

End.of commutes with negation.

@[simp]

theorem CategoryTheory.End.of_sub {C : Type u} [Category.{v, u} C] {X : C} [Preadditive C] (f g : X ⟶ X) : { asHom := f - g } = { asHom := f } - { asHom := g }

End.of commutes with subtraction.

@[simp]

theorem CategoryTheory.End.of_smul {C : Type u} [Category.{v, u} C] {X : C} [Preadditive C] {R : Type w} [Semiring R] [Linear R C] (r : R) (f : X ⟶ X) : { asHom := r • f } = r • { asHom := f }

End.of commutes with scalar multiplication in an R-linear category.

@[simp]

theorem CategoryTheory.End.algebraMap_asHom {C : Type u} [Category.{v, u} C] {X : C} [Preadditive C] {R : Type w} [CommSemiring R] [Linear R C] (r : R) : ((algebraMap R (End X)) r).asHom = r • CategoryStruct.id X

The structure map R → End X of an R-linear category sends r to r • 𝟙 X.

instance CategoryTheory.End.hom_isScalarTower_opEnd {C : Type u} [Category.{v, u} C] {X : C} [Preadditive C] {R : Type w} [Semiring R] [Linear R C] (Y : C) : IsScalarTower R (End X)ᵐᵒᵖ (X ⟶ Y)

The native precomposition action on morphisms respects ground-semiring scalars.

theorem CategoryTheory.Linear.comp_inv_smul_id {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {R : Type u_2} [Semiring R] [Linear R C] {X Y : C} (f : X ⟶ Y) (r : R) [IsIso (r • CategoryStruct.id X)] [IsIso (r • CategoryStruct.id Y)] : CategoryStruct.comp f (inv (r • CategoryStruct.id Y)) = CategoryStruct.comp (inv (r • CategoryStruct.id X)) f

The inverse of multiplication by a scalar r commutes with every morphism.

theorem CategoryTheory.Functor.isIso_smul_id_obj {C : Type u_1} [Category.{u_5, u_1} C] [Preadditive C] {R : Type u_2} [Semiring R] [CategoryTheory.Linear R C] {D : Type u_3} [Category.{u_4, u_3} D] [Preadditive D] [CategoryTheory.Linear R D] (F : Functor C D) [Linear R F] (r : R) (X : C) [IsIso (r • CategoryStruct.id X)] : IsIso (r • CategoryStruct.id (F.obj X))

If multiplication by a scalar r is invertible on X, then it is invertible on the image of X under any R-linear functor.

def CategoryTheory.Functor.mapEndAlgHom {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [Preadditive C] [Preadditive D] (F : Functor C D) (R : Type w) [CommSemiring R] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] [F.Additive] [Linear R F] (X : C) : End X →ₐ[R] End (F.obj X)

An additive linear functor induces an algebra homomorphism on endomorphisms.

@[simp]

theorem CategoryTheory.Functor.mapEndAlgHom_asHom {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [Preadditive C] [Preadditive D] (F : Functor C D) (R : Type w) [CommSemiring R] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] [F.Additive] [Linear R F] (X : C) (f : End X) : ((F.mapEndAlgHom R X) f).asHom = F.map f.asHom

The induced algebra homomorphism acts by the functor on underlying endomorphisms.

theorem CategoryTheory.Functor.mapEndAlgHom_injective {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [Preadditive C] [Preadditive D] (F : Functor C D) (R : Type w) [CommSemiring R] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] [F.Additive] [Linear R F] [F.Faithful] (X : C) : Function.Injective ⇑(F.mapEndAlgHom R X)

A faithful additive linear functor embeds each endomorphism algebra.

theorem CategoryTheory.Functor.mapEndAlgHom_bijective {C : Type u} [Category.{v, u} C] {D : Type u'} [Category.{v', u'} D] [Preadditive C] [Preadditive D] (F : Functor C D) (R : Type w) [CommSemiring R] [CategoryTheory.Linear R C] [CategoryTheory.Linear R D] [F.Additive] [Linear R F] (X : C) (h : Function.Bijective F.map) : Function.Bijective ⇑(F.mapEndAlgHom R X)

An additive linear functor bijective on an object's endomorphisms induces a bijective algebra homomorphism on its endomorphism algebra.