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 leanprovercommunity/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 extensionalitylike 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_(muladdzeroonedivinvnegsub)'  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/leanprovercommunity/mathlib/compare/fun_like#diff501f1a3fb0d8614260eca7d7b38363503ea7efbe126f783b29d855dfcea0f0f3R13
linearmap
should be linear_map
.
Johan Commelin (Aug 18 2021 at 18:50):
And https://github.com/leanprovercommunity/mathlib/compare/fun_like#diff501f1a3fb0d8614260eca7d7b38363503ea7efbe126f783b29d855dfcea0f0f3R31 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 `linearmap`.
+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 nonexhaustive list of homs which should be refactored:
 docs#non_unital_alg_hom
 docs#alg_hom
 docs#mul_action_hom
 docs#distrib_mul_action_hom
 docs#lie_hom
 docs#lie_module_hom
 docs#continuous_map
 docs#continuous_monoid_hom
 docs#valuation
 docs#nat.arithmetic_function
Anne Baanen (Jan 31 2022 at 10:53):
 docs#locally_constant (to fix https://leanprover.zulipchat.com/#narrow/stream/116395maths/topic/congr_arg)
Anne Baanen (Feb 11 2022 at 13:58):
 docs#ring_equiv should get a
ring_equiv_class
 docs#alg_equiv
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_measure
s (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