naming

Stream: general

[Reid Barton]

So I have a bunch of standard math terminology which contains a variable (a regular cardinal $\kappa$) in the middle of the term. For example:

• A set is $\kappa$-small if its cardinality is less than $\kappa$.
• A category is $\kappa$-small if its set of morphisms is $\kappa$-small.
• A category $I$ is $\kappa$-filtered if any functor from a $\kappa$-small category to I admits a cocone.
• An object $A$ of a category is $\kappa$-compact (or $\kappa$-presentable) if $\mathrm{Hom}(A, -)$ preserves colimits whose index categories are $\kappa$-filtered.
• A category is locally $\kappa$-presentable if... well you get the idea.

I'm not sure what good Lean names for these predicates would be. Currently I have is_kappa_small, 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 $\kappa$-presentable category, any $\mu$-compact object is a $\mu$-small $\kappa$-filtered colimit of $\kappa$-compact objects.

[Reid Barton]

To make matters worse, if you remove the "$\kappa$-" 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 $\aleph_0$-filtered, but in other places we insert "finitely" in place of $\aleph_0$, and "locally presentable" means locally $\kappa$-presentable for some $\kappa$.

[Reid Barton]

Things I thought about: something like filtered_wrt κ or filtered_rel κ for $\kappa$-filtered, but it's not really standard terminology.

[Reid Barton]

There's probably some more familiar examples as well, like being a $p$-group.

[Reid Barton]

How would you want to write that $G$ is a $q$-group, or a 2-group?

[Bryan Gin-ge Chen]

We currently have zmodp (contrast zmod) and padic_*, but the use of $p$ may be a special case as far as naming goes.

[Reid Barton]

I guess the names with kappa (or maybe κ) in the middle aren't so bad.

[Reid Barton]

I'm also tempted by

notation κ `-filtered`:max := kappa_filtered κ

but I don't know whether that is mathlib-approved

[Patrick Massot]

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 ξ