Morphism refactor

Stream: general

[Yaël Dillies]

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]

For context, this file defines fun_like

[Eric Wieser]

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]

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

[Eric Rodriguez]

what do the lean4 coes do for us?

[Anne Baanen]

@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]

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

[Johan Commelin]

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

[Anne Baanen]

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

[Johan Commelin]

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]

Should I try to revive lean#557?

[Eric Wieser]

I'd certainly be interested in seeing that revived

[Anne Baanen]

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]

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

[Yaël Dillies]

Here's a non-exhaustive 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]

• docs#locally_constant (to fix https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/congr_arg)

[Anne Baanen]

• docs#ring_equiv should get a ring_equiv_class
• docs#alg_equiv

[Yury G. Kudryashov]

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]

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

[Joseph Myers]

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]

I think, yes.

[Yaël Dillies]

@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]

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]

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]

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.