Generators for (morphisms of) a category?

Stream: mathlib4

[Kim Morrison]

Do we have somewhere the notion of generating sets of morphisms for a category? (Either written as a family of sets of morphisms satisfying some property, or perhaps as a condition on a Prefunctor from a Quiv to a Category?)

And then that f ∈ F.sections ↔ ... the relevant condition in terms of generators ...?

I feel like this is so simple it must be somewhere?

[Kim Morrison]

(Not super urgent, I was just looking at an erw in docs#CategoryTheory.Limits.Types.surjective_π_app_zero_of_surjective_map_aux, which we would avoid if we proved this theorem by using the fact that ℕᵒᵖ is generated by the n + 1 ⟶ n morphisms.)

[Johan Commelin]

There was work recently on generators of the simplex category...

[Johan Commelin]

But now I can't find that discussion...
@Nick Ward could you help us with a pointer?

[Joël Riou]

Using a combination of the definitions that @Robin Carlier and I introduced, we could do the following:

import Mathlib.CategoryTheory.MorphismProperty.Composition

namespace CategoryTheory

open MorphismProperty

def NatTrans.mkOfMultiplicativeClosureEqTop
    {C D : Type*} [Category C] [Category D]
    {F G : C ⥤ D} (app : ∀ X, F.obj X ⟶ G.obj X)
    (W : MorphismProperty C) (hW : W.multiplicativeClosure = ⊤)
    (naturality : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f),
      F.map f ≫ app Y = app X ≫ G.map f) : F ⟶ G where
  app := app
  naturality := by
    suffices ⊤ ≤ naturalityProperty app from
      fun _ _ f ↦ this _ (by simp)
    rw [← hW, multiplicativeClosure_le_iff]
    aesop

end CategoryTheory

As a section of a functor to types identifies to a natural transformation from the constant functor with value PUnit, it should be possible to get the exact lemma. Alternatively, instead of using MorphismProperty.naturalityProperty, given F : C ⥤ Type uand f : ∀ j, F.obj j, it could be possible to introduce the class of morphisms p : X ⟶ Y in C such that F.map p (f X) = f Y, show it is multiplicative and argue as above.

[Nick Ward]

Johan Commelin said:

But now I can't find that discussion...
Nick Ward could you help us with a pointer?

Probably too late to be helpful, but #PR reviews > #21741 -> #21748: presentation of `SimplexCategory` @ 💬 is the thread for Robin Carlier's PRs (#21749).