Zulip Chat Archive

Stream: general

Topic: naming

Reid Barton (Sep 09 2018 at 14:59):

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 II is κ\kappa-filtered if any functor from a κ\kappa-small category to I admits a cocone.
  • An object AA of a category is κ\kappa-compact (or κ\kappa-presentable) if Hom(A,)\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 (Sep 09 2018 at 15:01):

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 0\aleph_0-filtered, but in other places we insert "finitely" in place of 0\aleph_0, and "locally presentable" means locally κ\kappa-presentable for some κ\kappa.

Reid Barton (Sep 09 2018 at 15:02):

Things I thought about: something like filtered_wrt κ or filtered_rel κ for κ\kappa-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 pp-group.

Reid Barton (Sep 09 2018 at 15:05):

How would you want to write that GG is a qq-group, or a 2-group?

Bryan Gin-ge Chen (Sep 09 2018 at 15:12):

We currently have zmodp (contrast zmod) and padic_*, but the use of pp 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