MorphismProperty for Morphisms between Classes of Objects

Stream: Infinity-Cosmos

[Nima Rasekh]

Following @Emily Riehl discussion in

https://github.com/emilyriehl/infinity-cosmos/pull/36

there seems to be a benefit to having a generalization of MorphismProperty, which not only has as an input a category, but rather a category along with a subclass of objects (and probably separately for the domain and codomain).

There might be a naive solution to this, however, there is a whole MorphismProperty folder and I was wondering if there is a way to add this option in a way that interacts well with everything else. Apparently @Jack McKoen should have a take on this?

[Andrew Yang]

Do you mean something like AlgebraicGeometry.AffineTargetMorphismProperty? (where Scheme is just some category and IsAffine is some predicate on schemes)

I think one can definitely experiment with giving a universal API. The only concern I have is that this might not play well with typeclass synthesis.

But I think this is only useful if you have a bunch of morphism properties of this shape and you need to argue metaproperties of them and juggle with the negation or conjunction of them etc. Judging from the PR message alone (without knowing the big picture so I might be way off), it seems that it's just a single morphism property that does not behave the right way when the codomain is lacking conditions. I would suggest to just give it a "junk value" (following the rest of mathlib) on these non-sensical inputs and add relevant additional hypotheses when needed.

[Jack McKoen]

Nima Rasekh said:

Following Emily Riehl discussion in

https://github.com/emilyriehl/infinity-cosmos/pull/36

there seems to be a benefit to having a generalization of MorphismProperty, which not only has as an input a category, but rather a category along with a subclass of objects

I think I agree that there should be some sort of generalisation, but I'm not sure how to implement it. For now I think the inductive type "workaround" we've been using is sufficient, but it doesn't seem ideal to me

[Nima Rasekh]

Jack McKoen said:

Nima Rasekh said:

Following Emily Riehl discussion in

https://github.com/emilyriehl/infinity-cosmos/pull/36

there seems to be a benefit to having a generalization of MorphismProperty, which not only has as an input a category, but rather a category along with a subclass of objects

I think I agree that there should be some sort of generalisation, but I'm not sure how to implement it. For now I think the inductive type "workaround" we've been using is sufficient, but it doesn't seem ideal to me

Thanks @Andrew Yang and @Jack McKoen !
I guess for now we decided to completely abandon this direction given that there does not appear to be an easy solution, but it's good to know what's out there.