issue #1044: bundling morphisms

Stream: triage

[Random Issue Bot]

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?

[Kevin Buzzard]

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?

[Eric Wieser]

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)

[Eric Wieser]

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

[Random Issue Bot]

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?

[Kevin Buzzard]

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?

[Eric Wieser]

@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

[Eric Wieser]

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

[Anne Baanen]

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.

[Anne Baanen]

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.

[Random Issue Bot]

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?

[Kevin Buzzard]

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?

[Random Issue Bot]

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?

[Kevin Buzzard]

Unbundled morphisms are now deprecated but the last comment by Eric on the issue might mean that there are still some interesting questions here. Maybe we could close this issue and open a new one? Very few non-deprecated files import deprecated files by the way, it would be a nice project to finish the job, I just got tired. There is not much left to do.

[Random Issue Bot]

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?

[Kevin Buzzard]

This issue could be closed as far as I'm concerned -- but there is this comment from Eric in September which might be worth keeping around.