Factorisations and MonoFactorisations

Stream: mathlib4

[Fernando Chu]

Mathlib currently has definitions of factorisation of morphisms as well as mono factorisations. Both of these are independent structures. Should these be somehow linked? Maybe mono factorisations should just extend factorisations? Maybe they should be a class?

[Edward van de Meent]

maybe the structures should be generalized using MorphismProperty or something?

[Fernando Chu]

Good point, this is the nlab's approach for images

[Fernando Chu]

Feels like a huge pain though :melting_face:

[Edward van de Meent]

having good abbrevs is important here, i think... i imagine that might get difficult tho

[Fernando Chu]

Actually, this is already defined in MorphismProperty.factorization

[Fernando Chu]

So we have three different notions, though it seems to me that all of them should be instances of this last one

[Edward van de Meent]

yea... i suspect, however, that it will be useful to keep the "no bells and whistles" docs#CategoryTheory.Factorisation, have docs#CategoryTheory.MorphismProperty.MapFactorizationData extend that one, and then have docs#CategoryTheory.Limits.MonoFactorisation be an abbrev with the correct MorphismPropertys

[Edward van de Meent]

(and while we're at it, decide if it is spelled factorization or factorisation)

[Fernando Chu]

I'm not sure what the implications of MorphismProperty.factorization extending CategoryTheory.Factorisation vs the latter being an abbrev of the first one is.

[Edward van de Meent]

(i think) it means it will be easier to construct "normal" factorizations... if this is a good idea will probably become evident once we try to do the refactorization