category of objects with distinguished endomorphism

Stream: Is there code for X?

[Johan Commelin]

We have the arrow category. Do we also have the following construction? Let C be a category. Then build a new category whose objects are pairs (X, f), where X : C and f : X ⟶ X.
For C = Module R this construction spits out Module (polynomial R) (up to canonical equivalence).

[Alex J. Best]

This is https://mathoverflow.net/q/149007/23872 right? Not that it answers your question :upside_down:

[Scott Morrison]

No, we don't have it.

[Scott Morrison]

I did have the Karoubi envelope / idempotent completion (the same, but with f^2 = f), but I don't think it ever made it to mathlib.

[Matthew Ballard]

Can't you do something like functor.category single_obj \N C?

[Adam Topaz]

Looking at docs#category_theory.single_obj now, it looks like we're missing some construction like single_obj.lift of the following form

import category_theory.single_obj

open category_theory

variables {α : Type*} [monoid α] {C : Type*} [category C]

def category_theory.single_obj.lift {X : C} (f : α →* End X) : single_obj α ⥤ C :=
{ obj := λ _, X,
  map := λ i j g,
  match i, j, g with
  | punit.star, punit.star, g := f g
  end,
  map_id' := begin
    rintro ⟨⟩,
    exact f.map_one,
  end,
  map_comp' := begin
    rintro ⟨⟩ ⟨⟩ ⟨⟩ a b,
    apply f.map_mul,
  end }

[Adam Topaz]

If we combine that with docs#free_monoid.lift then that already get fairly close to what @Johan Commelin is looking for, I think.