Zulip Chat Archive

Stream: general

Topic: image factorization to functor


view this post on Zulip Qais Hamarneh (Jul 27 2019 at 19:09):

I have a functor (F : Type u ⥤ Type u) using the category types as defined in
mathlib.category_theory.types.lean
and a function (f: A → F.obj A .
I would like to define the image_factorization of this function on (S : set A) as a : S → F.obj S .
However, I am not able to “convince” lean that (f s ∈ F.obj S).
I tried both subsets and subtypes and it didn’t work.

view this post on Zulip Johan Commelin (Jul 27 2019 at 19:40):

@Qais Hamarneh Why would it be true?

view this post on Zulip Johan Commelin (Jul 27 2019 at 19:41):

You need some compatibility between f and the functor F, right?

view this post on Zulip Qais Hamarneh (Jul 27 2019 at 20:11):

Actually @Johan Commelin , you're right, it might not hold up. Forget about it.


Last updated: May 12 2021 at 23:13 UTC