Zulip Chat Archive

Stream: general

Topic: Hierarchies

Yaël Dillies (Oct 11 2021 at 06:42):

What mathlib hierarchies can you think about? I have in mind:

  • algebraic hierarchy
  • order hierarchy
  • algebraic order hierarchy
  • scalar hierarchy
  • norm hierarchy

Johan Commelin (Oct 11 2021 at 06:44):

  • categorical hierarchy
  • topological hierarchy
  • topologico-algebraic hierarchy

Johan Commelin (Oct 11 2021 at 06:46):

@Yaël Dillies I guess with the norm hierarchy, you have in mind different algebraic structures carrying a norm?

Yaël Dillies (Oct 11 2021 at 06:46):

Yes

Yaël Dillies (Oct 11 2021 at 06:46):

Is metric stuff part of the topological hierarchy?

Johan Commelin (Oct 11 2021 at 06:49):

I guess so, at some point these hierarchies start to blend.

Yaël Dillies (Oct 11 2021 at 06:51):

What would you put in there, at least?

Johan Commelin (Oct 11 2021 at 06:52):

In the topo hierarchy? Stuff like t1_space, t2_space, normal_space, etc...

Yaël Dillies (Oct 11 2021 at 06:52):

uniform_space?

Johan Commelin (Oct 11 2021 at 06:52):

Also, yes.

Yaël Dillies (Oct 11 2021 at 06:54):

And what's in the categorical hierarchy?

Johan Commelin (Oct 11 2021 at 06:55):

Ooh, that will probably be a long list. Certainly things like preadditive, abelian, monoidal.

Johan Commelin (Oct 11 2021 at 06:56):

I don't know if we want to do things with has_limits and has_colimits. There are dozens of variants of those.

Bhavik Mehta (Oct 11 2021 at 12:24):

The hierarchy for limits could be helpful (and the colimits one should be dual); I also have ideas for making a hierarchy of exactness properties in categories to include stuff like disjoint coproducts, extensiveness, etc

Johan Commelin (Oct 11 2021 at 12:32):

That last remark is about new stuff, right? Not about documenting existing hierarchies? (I think Yaël was inquiring about hierarchies that could be documented in some standardised/centralised way...)

Bhavik Mehta (Oct 11 2021 at 17:37):

Yes, sorry for the confusion

Yakov Pechersky (Oct 12 2021 at 16:54):

Is it possible to piecewise refactor to new structures? Or are old structures unable to use new structures?

I've been trying to annotate the existing hierarchies to understand how to redefine them with new structures. For example, here are the classes used and defined in algebra/group/defs:
image.png

The tex file is available in branch#pechersky/algebra-tex. I mostly tried to annotate "data" as solid arrows and bold, only Prop addition via dashed lines, reverse (usually lower priority) instances as dotted lines, instances/defs via @[to_additive] as red, and reducible defs (not instances) as Bar-head arrows.

I noticed some (historical?) oddities, like this
attribute [instance, priority 300] add_comm_group.to_add_comm_monoid
https://github.com/leanprover-community/mathlib/blob/136d0ce97bafcf34872cc0a2d28383b567edc24a/src/algebra/group/defs.lean#L806

Yakov Pechersky (Oct 12 2021 at 16:57):

That is, could we refactor just this single file first?

Yury G. Kudryashov (Oct 12 2021 at 17:07):

AFAIR, new structures can extend old structures but not vice versa.

Yury G. Kudryashov (Oct 12 2021 at 17:08):

(more precisely, they can but it leads to very strange behavior)

Yury G. Kudryashov (Oct 12 2021 at 17:09):

attribute [instance, priority 300] add_comm_group.to_add_comm_monoid is here to help with instance searches in linear algebra.

Yury G. Kudryashov (Oct 12 2021 at 17:09):

I don't know if it is still needed.

Last updated: Dec 20 2023 at 11:08 UTC