Concrete homomorphism type vs abstract class

Stream: mathlib4

[Artie Khovanov]

Should definitions like

def Subring.comap {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) (s : Subring S) :
Subring R

be using [RingHomClass F R S] (f : F) instead of f : R →+* S?

[Yaël Dillies]

Possibly spicy take: No, and docs#LinearMap.ker and alike is the one to be wrong

[Yaël Dillies]

My reasoning: If you have a bundled blah blah (where a blah is something stronger than a linear map), then you can either talk about LinearMap.ker blah or LinearMap.ker blah.toLinearMap. Because Blah is niche, nobody has written API for LinearMap.ker blah, but at the same time it's the nicer to read spelling, so you are willing to use it anyway.

[Johan Commelin]

Sorry, I don't follow your argument. What is the reason to avoid the nice spelling?

[Yaël Dillies]

The reason is that it has no API

[Johan Commelin]

And why would LinearMap.ker blah.toLinearMap have API, if Blah is niche?

[Yaël Dillies]

because LinearMap.ker and Blah.toLinearMap will both have API. I'm not making this situation up. It keeps on happening to me

[Yaël Dillies]

Let's put it another way. Currently, for every Blah, one needs to write the lemma LinearMap.ker_blahZero : ker (0 : blah) = univ, and similarly for other lemmas. So one needs to write quadratically many lemmas. With my suggestion, one needs only one LinearMap.ker lemma, namely LinearMap.ker_zero, and a lemma about Blah, namely Blah.toLinearMap_zero : Blah.toLinearMap 0 = 0, which we should have anyway

[Johan Commelin]

I really don't like the looks of blah.toLinearMap.
Shouldn't LinearMap.ker_zero be a lemma about LinearMapClass F and Zero F, with a suitable mixin, or extension, so that toLinearMap (0 : F) = 0.

[Yaël Dillies]

I am not convinced there is a sensible finite set of axiomatisations that covers everything we need

[Johan Commelin]

But we might still be able to cover 98%

[Christian Merten]

Another issue with the FooHomClass design is the duplication caused by lemmas involving compositions, e.g. docs#Ideal.map_map and docs#Ideal.map_mapₐ Ideal.map_mapₐ

[Kevin Buzzard]

[ooh I thought we'd fixed that linker bug]

[Eric Wieser]

In the same vein, arguably even the coercions from FooHomClass-satisfying types to FooHom are bad, because they also amount to definitions that end up called on a type with no API

[Yaël Dillies]

Yes, exactly. #21031 gets rid of those

[Mitchell Lee]

Johan Commelin said:

I really don't like the looks of blah.toLinearMap.
Shouldn't LinearMap.ker_zero be a lemma about LinearMapClass F and Zero F, with a suitable mixin, or extension, so that toLinearMap (0 : F) = 0.

Why can't toLinearMap be a coercion, so you could still just write LinearMap.ker blah?

[Yaël Dillies]

Yes, Mitchell's suggestion is part of what I am implementing in #21031

[Riccardo Brasca]

I don't have a strong opinion, but I remember being annoyed by ker (or something like that) asking for a linear map and being happy with the new solution. The problems described above surely exist, but I have the impression we notice weaknesses much more than strengths (just because we get very quickly used to something that works).

[Jireh Loreaux]

Indeed. I think we should strive to obliterate hom class coercions in statements as much as possible, which would mean keeping LinearMap.ker as is.

[Eric Wieser]

I would make a different claim that we should eliminate [HomClass _] in defs, and only use them in theorems

[Junyan Xu]

It seems to me that (in the case of ker), this is the only lemma we're actually missing:

import Mathlib.Algebra.Module.Submodule.Ker

variable {R R₂ M M₂ : Type*} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] (f : F)

theorem LinearMap.ker_coe : LinearMap.ker f = LinearMap.ker (f : M →ₛₗ[τ₁₂] M₂) := rfl

If we want to use APIs that are only available for ker of a LinearMap, we can rewrite by this to use them.

[Junyan Xu]

Mitchell Lee said:

Why can't toLinearMap be a coercion, so you could still just write LinearMap.ker blah?

It is a coercion, but Lean usually need to know all three of M, τ₁₂, M₂ for the coercion to work. I encounter this a lot when trying to compose (∘ₗ) LinearMap with LinearEquiv; I frequently need to use LinearEquiv.toLinearMap.

(Update: Actually, not all three. If you replace τ₁₂ or M₂ in M →ₛₗ[τ₁₂] M₂ by _ it will fail, but if you replace M by _ it's okay.)

[Eric Wieser]

But then we also need lemmas about (f : M →ₛₗ[τ₁₂] M₂) for particular choices of F and f, which I think are also absent

[Junyan Xu]

lemmas about (f : M →ₛₗ[τ₁₂] M₂)

I think those lemmas need to exist anyway? According to Yaël:

a lemma about Blah, namely Blah.toLinearMap_zero : Blah.toLinearMap 0 = 0

[Artie Khovanov]

I'm really confused :sad:. Is there any consensus on how to proceed in my specific case?

[Eric Wieser]

Junyan Xu said:

lemmas about (f : M →ₛₗ[τ₁₂] M₂)

I think those lemmas need to exist anyway? According to Yaël:

a lemma about Blah, namely Blah.toLinearMap_zero : Blah.toLinearMap 0 = 0

For toLinearMap, we only need a lemma for every edge of the graph. For the FooHomClass versions, we need a lemma for every path through the graph

[Jireh Loreaux]

@Artie Khovanov not yet, this is an active point of discussion. Give it some more time for the dust to settle.

[Artie Khovanov]

Yeah, no worries -- I just couldn't parse a lot of what people were saying! I guess I'm not familiar enough with the existing design patterns.

[Jireh Loreaux]

once we figure out the correct approach, we'll be sure to distill it down into something manageable.