Reid Barton (Sep 09 2018 at 14:59):
So I have a bunch of standard math terminology which contains a variable (a regular cardinal ) in the middle of the term. For example:
- A set is -small if its cardinality is less than .
- A category is -small if its set of morphisms is -small.
- A category is -filtered if any functor from a -small category to I admits a cocone.
- An object of a category is -compact (or -presentable) if preserves colimits whose index categories are -filtered.
- A category is locally -presentable if... well you get the idea.
I'm not sure what good Lean names for these predicates would be. Currently I have
kappa_filtered etc., but that's not very satisfying because the
kappa part of the name doesn't really refer to anything--these things all take
κ as an explicit argument. Furthermore the
κ will vary in some cases, for example, in a locally -presentable category, any -compact object is a -small -filtered colimit of -compact objects.
Reid Barton (Sep 09 2018 at 15:01):
To make matters worse, if you remove the "-" part of the terminology, then they become new terms with meanings which relate to the original ones in different ways. A filtered category is one which is -filtered, but in other places we insert "finitely" in place of , and "locally presentable" means locally -presentable for some .
Reid Barton (Sep 09 2018 at 15:02):
Things I thought about: something like
filtered_wrt κ or
filtered_rel κ for -filtered, but it's not really standard terminology.
Reid Barton (Sep 09 2018 at 15:04):
There's probably some more familiar examples as well, like being a -group.
Reid Barton (Sep 09 2018 at 15:05):
How would you want to write that is a -group, or a 2-group?
Bryan Gin-ge Chen (Sep 09 2018 at 15:12):
We currently have
padic_*, but the use of may be a special case as far as naming goes.
Reid Barton (Sep 09 2018 at 15:26):
I guess the names with
kappa (or maybe
κ) in the middle aren't so bad.
Reid Barton (Sep 09 2018 at 15:33):
I'm also tempted by
notation κ `-filtered`:max := kappa_filtered κ
but I don't know whether that is mathlib-approved
Patrick Massot (Sep 09 2018 at 18:27):
We also have that kind of problem in symplectic topology. We things called J-holomorphic curves, or ξ-convex surfaces, even when we don't specify an almost complex structure J or a contact structure ξ
Last updated: Aug 03 2023 at 10:10 UTC