Zulip Chat Archive

Stream: triage

Topic: issue #1044: bundling morphisms


view this post on Zulip Random Issue Bot (Jan 20 2021 at 14:45):

Today I chose issue 1044 for discussion!

bundling morphisms
Created by @Kevin Buzzard (@kbuzzard) on 2019-05-17
Labels: needs-refactor

Is this issue still relevant? Any recent updates? Anyone making progress?

view this post on Zulip Kevin Buzzard (Jan 20 2021 at 14:48):

My current understanding is that we would like to retain is_linear_map and the nature of the refactor is that it should be changed from a structure to a class. Is this correct? To be frank I am confused about what we are tying to do with that deprecated directory. It would be nice to hear some advice from the maintainers about where the issue of bundling morphisms is going. Is it clear what is happening with Lean 4? Are we going back to unbundled morphisms and classes (like is_linear_map)? If so, what should we be doing with Lean 3?

view this post on Zulip Eric Wieser (Jan 20 2021 at 15:39):

There was another proposal that @Anne Baanen and I discussed somewhere either here on Zulip or on Github that suggested changing from

class is_whatever_map {A B : Type*} (f : A  B) :=
(map_add' :  x y, f (x + y) = f x + f y)

to something like

class is_whatever_map' {A B : Type*} {F : Type*} [has_coe F (A  B)] :=
(map_add' :  (f : F) (x y : A), f (x + y) = f x + f y)

Which resolves the problem with is_whatever_map.map_add' being ineligible for simp (which I think is why they were deprecated in the first place)

view this post on Zulip Eric Wieser (Jan 20 2021 at 15:40):

But still has the advantage that lemmas can say "well obviously a linear_map is an add_monoid_hom" in the same way we're used to saying "well obviously a group is a monoid", rather than having to play some horrible dance with to_add_monoid_hom

view this post on Zulip Random Issue Bot (Mar 02 2021 at 14:17):

Today I chose issue 1044 for discussion!

bundling morphisms
Created by @Kevin Buzzard (@kbuzzard) on 2019-05-17
Labels: needs-refactor

Is this issue still relevant? Any recent updates? Anyone making progress?

view this post on Zulip Kevin Buzzard (Mar 02 2021 at 14:54):

Good question. I opened this issue to make a note of the fact that we had two ways of doing the same thing. Now one is deprecated. I am not clear on the state of either this issue or the more general issue of what the heck is supposed to be happening with the deprecated stuff. I can ask my questions in the issue or I can ask them here. The questions are:

1) Unbundled morphisms between algebraic structures. Example: deprecated/group.lean defines a class docs#is_monoid_hom . Is the general feeling of the community that this structure is useful but shouldn't be a class, so the action here is to do a refactor which makes it a structure not a class and then moves this file back to the group_theory directory with a module doc explaining what is going on? Or is the plan to remove this structure completely?

2) Unbundled substructures. Example: docs#is_subgroup defined in deprecated/subgroup.lean. Same question.

3) What are the plans for Lean 4? What would be a good experiment?

view this post on Zulip Eric Wieser (Mar 02 2021 at 14:58):

@Adam Topaz ran into an interesting situation where simply using

structure bundled_hom (A B : Type*) :=
(to_fun : A  B)

means that we can use

class is_add_monoid_hom {A B} (f : bundled_hom A B) :=
(map_zero : f 0 = 0)
(map_add : f (a + b) = f a + f b)

attribute [simp] is_add_monoid_hom.map_add

and simp can actually fire on map_add, which I believe does not work with the current version of is_add_monoid_hom

view this post on Zulip Eric Wieser (Mar 02 2021 at 14:59):

With the key reason here being that docs#is_add_monoid_hom.map_add has f as a head symbol, but the one in that snippet has coe_fn as the head symbol

view this post on Zulip Anne Baanen (Mar 02 2021 at 15:13):

My intuition is saying that the typeclass is_add_monoid_hom f, rather than add_monoid_hom A B, may not be nice to work with since f will have various defeq-but-not-syntax-eq representations in practice. So finding the instance may depend on how much the term gets unfolded (or did :four_leaf_clover: solve this?), and there might be issues of the form "motive is incorrect" if you rewrite f.

view this post on Zulip Anne Baanen (Mar 02 2021 at 15:14):

With typeclasses that use types as a parameter, this is not such an issue since you don't want to deal with equality of types anyway.

view this post on Zulip Random Issue Bot (Apr 09 2021 at 14:24):

Today I chose issue 1044 for discussion!

bundling morphisms
Created by @Kevin Buzzard (@kbuzzard) on 2019-05-17
Labels: needs-refactor

Is this issue still relevant? Any recent updates? Anyone making progress?

view this post on Zulip Kevin Buzzard (Apr 09 2021 at 14:30):

I don't have anything to add here. I would still be interested in hearing what the plan is with the deprecated is_ predicates. Is the idea that we're supposed to be changing them from classes to structures and then marking them as undeprecated?


Last updated: May 09 2021 at 16:20 UTC