Zulip Chat Archive

Stream: general

Topic: Morphism refactor

Yaël Dillies (Aug 18 2021 at 16:59):

So we want to refactor how morphisms are done. Instead of stating lemmas on bundled homs, we will state them on typeclasses which will be instantiated by the bundled homs. This is reminiscent of how the order refactor is introducing typeclasses, whose content is basically a specific lemma holding true, between order classes and order lemmas.

@Anne Baanen, I read your branch#fun_like and I'm surprised so as to how you approach the thing (you are most probably right, I mustn't have thought about it enough). Why do we want fun_like and why aren't we nuking lemmas like some_bundled_map.map_add?

Eric Wieser (Aug 18 2021 at 17:23):

For context, this file defines fun_like

Eric Wieser (Aug 18 2021 at 17:24):

We want fun_like for the same reason as we have docs#set_like; it unifies a lot of boring lemmas about extensionality. Meanwhile, we want to_fun from that PR because we don't have leanprover-community/lean#557 yet.

Eric Wieser (Aug 18 2021 at 17:26):

As for leaving behind the some_bundled_map.map_add lemmas, it's probably a dot notation and reducing work thing.

Eric Rodriguez (Aug 18 2021 at 17:51):

what do the lean4 coes do for us?

Anne Baanen (Aug 18 2021 at 18:29):

@Eric Wieser is exactly correct, but let me expand a bit.

First of all, it's important to note that my plan is to instantiate typeclasses on types of bundled homs, not the homs themselves (so not like the old is_monoid_hom class used to do).

to_fun is needed for 2 reasons: one is lean4 compatibility, the other is that has_coe_to_fun makes it impossible to state in the typeclass what the return type of the coe actually is, so it's impossible to state something like map_mul: if you can't specify at the type level that has_coe_to_fun.F f = M → N, there's no way to write [has_mul M] [has_mul N] (x y : M). So the return type needs to be part of the typeclass.

Then fun_like is for the boring extensionality-like lemmas, it's mostly there as a placeholder for someone to do a set_like refactor with.

Finally, the bundled_map.map_whatever-style lemmas can stay for now, as they are too many to deal with at once. (I count exactly 2000 of the basic ones: rg '\.map_(mul|add|zero|one|div|inv|neg|sub)' | wc -l) Originally I wanted to try to get rid of them all, but as more and more get added each day this was a bit too optimistic. Now they'll just be demoted from simp lemma to protected lemma, to be phased out later.

Johan Commelin (Aug 18 2021 at 18:49):

Quick comment: https://github.com/leanprover-community/mathlib/compare/fun_like#diff-501f1a3fb0d8614260eca7d7b38363503ea7efbe126f783b29d855dfcea0f0f3R13
linear-map should be linear_map.

Johan Commelin (Aug 18 2021 at 18:50):

And https://github.com/leanprover-community/mathlib/compare/fun_like#diff-501f1a3fb0d8614260eca7d7b38363503ea7efbe126f783b29d855dfcea0f0f3R31 should be removed, I think

Anne Baanen (Aug 19 2021 at 10:03):

Those links don't work for me - could you comment on the commits instead?

Johan Commelin (Aug 19 2021 at 11:25):

I just pushed

commit a496eb0ae152cd7cc1ca85c799c1254a619da66a (HEAD -> fun_like, origin/fun_like)
Author: Johan Commelin <johan@commelin.net>
Date:   Thu Aug 19 11:25:16 2021 +0000

    little fix in doc

diff --git a/src/data/fun_like.lean b/src/data/fun_like.lean
index fc91eff7ce..4b373bd921 100644
--- a/src/data/fun_like.lean
+++ b/src/data/fun_like.lean
@@ -10,7 +10,7 @@ import tactic.norm_cast
 # Typeclass for a type `F` with an injective map to `A → B`

-This typeclass is primarily for use by homomorphisms like `monoid_hom` and `linear-map`.
+This typeclass is primarily for use by homomorphisms like `monoid_hom` and `linear_map`.

 A typical type of morphisms should be declared as:
@@ -28,8 +28,6 @@ instance : fun_like (my_hom A B) A B :=
 /-- Helper instance for when there's too many metavariables to apply `to_fun.to_coe_fn` directly. -/
 instance : has_coe_to_fun (M →ₗ[R] M₂) := to_fun.to_coe_fn

-@[simp] lemma to_fun_eq_coe {f : M →ₗ[R] M₂} : f.to_fun = (f : M → M₂) := rfl
 @[simp] lemma to_fun_eq_coe {f : my_hom A B} : f.to_fun = (f : A → B) := rfl

 @[ext] theorem ext {f g : my_hom A B} (h : ∀ x, f x = g x) : f = g := fun_like.ext f g h

to your branch

Yury G. Kudryashov (Sep 11 2021 at 20:06):

Should I try to revive lean#557?

Eric Wieser (Sep 11 2021 at 20:11):

I'd certainly be interested in seeing that revived

Anne Baanen (Sep 13 2021 at 07:45):

I would be very happy to see the new definition of has_coe_to_fun being merged and have some more time to work on the morphism refactor from this/next week on, so let me know if there's anything I can do for lean#557!

Yury G. Kudryashov (Sep 13 2021 at 21:28):

Once we have #9165 merged, I'll merge master into #7033, push it to github, and see what fails.

Yaël Dillies (Jan 25 2022 at 17:53):

Here's a non-exhaustive list of homs which should be refactored:

Anne Baanen (Jan 31 2022 at 10:53):

Anne Baanen (Feb 11 2022 at 13:58):

Yury G. Kudryashov (Feb 11 2022 at 15:12):

If we add a class for docs#measure_theory.outer_measure, then we can avoid repeating lemmas for outer_measure and measure.

Yury G. Kudryashov (Feb 11 2022 at 16:00):

And we can generalize the ae filter to outer_measures (with fewer properties).

Joseph Myers (Feb 11 2022 at 19:42):

Are isometries within scope for this refactor? There are at least five bundled types for isometries (docs#isometric docs#linear_isometry docs#linear_isometry_equiv docs#affine_isometry docs#affine_isometry_equiv) as well as the unbundled predicate on functions (docs#isometry).

Yury G. Kudryashov (Feb 11 2022 at 19:51):

I think, yes.

Yaël Dillies (Feb 21 2022 at 23:57):

@Andrew Yang, I heard you say that you were defining many types of morphisms. Are you following the hom refactor? Do you know how to? May I help?

Andrew Yang (Feb 22 2022 at 00:48):

I think this is far away from me since the “morphisms” I have in mind are morphisms in the category of schemes, which are not (yet?) concrete morphisms between Types.
And I’m merely adding typeclasses that looks like “forall {X Y : Scheme
} (f : X —> Y), Prop”
I might be wrong though.

Yaël Dillies (Feb 22 2022 at 00:50):

Okay. I've been defining lots categories of orders recently (see #11677 for the master plan) and the pattern always has been "order structure, bundled morphisms, category".

Andrew Yang (Feb 22 2022 at 02:21):

I see. I won't be needing the bundled version, and I'll keep them as unbundled predicates if that does not conflict with your plans.

Last updated: Dec 20 2023 at 11:08 UTC