Type Class question

Stream: mathlib4

[Antoine Chambert-Loir]

Imagine I want a Class to extend two preexisting classes, but I want the name of one of the fields of one of them to be renamed to something else. What is the recommended way?

In practice, I refactored MulActionHomto authorise equivariant actions that pass through a morphism, where the field is called map_smul, and then this needs to be passed to LinearMap, where the field is called map_smulₛₗ.

class MulActionHomClass (F : Type _) {M N : outParam (Type _)}
(φ : outParam (M → N)) (X Y : outParam (Type _)) [SMul M X] [SMul N Y] extends
  FunLike F X fun _ => Y where
  /-- The proposition that the function preserves the action. -/
  map_smul : ∀ (f : F) (c : M) (x : X), f (c • x) = (φ c) • (f x)


class SemilinearMapClass (F : Type _)
  {R S : outParam (Type _)} [Semiring R] [Semiring S]
  (σ : outParam (R →+* S))
  (M M₂ : outParam (Type _)) [AddCommMonoid M] [AddCommMonoid M₂]
  [Module R M] [Module S M₂]
  extends AddHomClass F M M₂, MulActionHomClass F σ M M₂

but the field map_smul inherited from MulActionHomClass should be called map_smulₛₗ to avoid changing the whole library…

[Yury G. Kudryashov]

BTW, should we merge docs#LinearMap and docs#DistribMulActionHom ?

[Anatole Dedecker]

The fact that we have both of these is quite funny x)

[Kevin Buzzard]

To be quite honest the word "DistribMulActionHom" is already pretty funny. That's what happens if you let computer scientists name things... (cf also this)

[Adam Topaz]

In lean3 we could have written extends foo renaming bar -> baz. Do we not have such a thing in lean4? I just tried and it doesn't work.

[Eric Wieser]

Yury G. Kudryashov said:

BTW, should we merge docs#LinearMap and docs#DistribMulActionHom ?

I had a mathlib3 PR that did this (pre-semilinear map) but had timeout issues. Extra generality sadly comes with performance costs, and "it would be tidier to merge these" isnt a very valuable generalization.