DFunLike with multiple types

Stream: mathlib4

[Alex Meiburg]

DFunLike has the type (F : Sort u) (α : outParam (Sort v)) (β : outParam (α → Sort w)), which means (as I understand it) that it picks the first DFunLike instance for F that it sees, and then picks α and β based on that.

I've got a case where I would really like to equip one class with multiple DFunLike instances. I've defined the type HermitianPreservingMap m n α of linear maps from Matrix m m α to Matrix n n α that are Hermitian preserving, that is, if the input is Hermitian then the output is Hermitian. And I've defined the type HermitianMat n α := selfAdjoint (Matrix n n α), and built a bunch of API around that type.

The most natural FunLike instance for HermitianPreservingMap is then mapping HermitianMat m α to HermitianMat n α. But, at times, I would like to apply this to a plain-old matrix (that isn't Hermitian). Functional extensionality still works: the set of Hermitian matrices span (as a α-vector space) the space of all matrices. So it would be nice to also define a FunLike instance mapping Matrix m m α to Matrix n n α.

(This is a bit of a simplification, but this is the core problem.)

But if I try to define two FunLike instances, it causes lots of problems with inference, I think because of the outParam annotation. So I'm trying to both understand why it's made like that, and what I should do.

[Alex Meiburg]

I think the answer might be something about letting there be a CoeHead from HermitianPreservingMap down to LinearMap or something, but I'm very fuzzy on how that actually is supposed to work.

[Aaron Liu]

I think it's because docs#CoeFun also has the outParam

[Alex Meiburg]

Bumping this: what is the intended or standard way to deal with a type that is, quite naturally, a "function" on two different types?

Another example: for U : Matrix.unitaryGroup n ℂ, I would like to both have it acting on "kets" and "mixed states" in quantum mechanics.

That is, I have the type Ket n for normalized vectors n -> ℂ, and a type MState n for mixed states - PSD matrices with trace 1. These are both pretty standard objects in quantum mechanics. Unitaries naturally act on ket's by multiplication (and of course, they preserve the norm), and they act on mixed states by conjugation (this preserver the PSD condition and the trace). Both would be valid DFunLike instances: they have functional extensionality. And indeed people often do things like composing these (multiplying the unitaries), etc. etc. and I would like to be able to talk about this.

Is there a good solution to this?

[Robin Arnez]

Well I think the idea is that CoeFun (which DFunLike is implemented with) is meant to allow for everything that you could do for regular functions but not more. With regular functions you can't provide parameters of different types unless you add implicit parameters or coercions. I opted for implicits since they work better here:

import Lean.Meta

/-- Class used to tag fun-likes with multiple parameter types -/
class MultiFunLike (α : Sort u) where

class MultiFunLikeRule (α : Sort u) (β : Sort v) (γ : outParam (β → Sort w)) where
  coe : α → (a : β) → γ a

abbrev MultiFunLike.coe {α : Sort u} [MultiFunLike α] (fn : α)
    {β : Sort v} {γ : β → Sort w} [MultiFunLikeRule α β γ] (x : β) : γ x :=
  MultiFunLikeRule.coe fn x

run_meta
  Lean.Meta.registerCoercion ``MultiFunLike.coe (some { type := .coeFun, numArgs := 3, coercee := 2 })

instance [MultiFunLike α] : CoeFun α (fun _ => {β : Sort v} → {γ : β → Sort w} → [MultiFunLikeRule α β γ] → (x : β) → γ x) where
  coe := MultiFunLike.coe

-- coerces to `not` and `Nat.succ`
inductive NotSucc where
  | mk

instance : MultiFunLike NotSucc := ⟨⟩
instance : MultiFunLikeRule NotSucc Bool (fun _ => Bool) := ⟨fun _ => not⟩
instance : MultiFunLikeRule NotSucc Nat (fun _ => Nat) := ⟨fun _ => Nat.succ⟩

#check NotSucc.mk false -- NotSucc.mk false : Bool
#check NotSucc.mk 0 -- NotSucc.mk 0 : Nat

[Robin Carlier]

Note that an other case where something has multiple coercions to functions (though in this case the individual coercions are not injective) is functors in category theory: they act on objects, and on every hom-type between objects.
The CategoryTheory part of the library is probably way too deep in the current design to even consider a refactor if "multiple coercions to functions" were a thing though (I once experimented and tried to put a DFunlike on natural transformations, and soon gave up).

[Alex Meiburg]

@Robin Arnez: Hmm! Well that's a super interesting way to do it. I'll consider it, but also it makes me pretty nervous -- it feels like probably re-inventing the wheel a bit, and I'll have e.g. conflicts if I wanted to use this with anything that expects a DFunLike. Like, I don't think this would easily work with LinearMapClass then, for instance. Of course I could add the typeclass inference from a MultiFunLikeRule to a DFunLike, but then inference will get stuck there again, which is the original problem.

So I guess the answer is, right now it's really intended that you're always supposed to pick one canonical function to cast to. Alright.

[Alex Meiburg]

@Robin Carlier: What does the category theory library do, then? Pick one of the coercions to be the "canonical" one, and refer the other one just by a field name + with manual "ext" lemmas and so on?

[Alex Meiburg]

Okay, actually it looks there's just neither one.

[Robin Carlier]

None of those: we use F.obj _ and F.map _ everywhere, and also have Functor.ext (which is avoided because "equality of objects in categories is bad and functors are objects of functor categories").

[Robin Carlier]

(admittedly, coercions to functions would only be quality of life in category theory, not a game-changing addition)

[Alex Meiburg]

I see.
I would be fine just picking one (or neither), but in order to use LinearMapClass I need to have a DFunLike. And I have two distinct LinearMapClass types I want to provide.

I guess a solution would be to define something like

MyType := ... --thing I want two instances on

instance : FunLike MyType A B := ... --first instance

instance : LinearMapClass MyType A B := ... --building on it

@[reducible] --alias that lets you pick out the other one. (*should* this be reducible?)
def MyTypeOnX : Type := MyType

def MyType.onX := fun x -> x

instance : FunLike MyTypeOnX X Y := ... --second instance

instance : LinearMapClass MyTypeOnX X Y := ... building on it

[Alex Meiburg]

does that look ... reasonable?

[Kevin Buzzard]

These are actions (U is a function from a thing X to itself rather than to another thing) so you can use SMul to have both of these at once.

[Alex Meiburg]

Oh, good point, I'll probably do that for the "unitary acting on normalized vector / mixed states". That's nice.

It doesn't let me get a LinearMapClass, though.

[Alex Meiburg]

I guess I'll build off the above, it mostly matches with the coercions that already exist anyway. (A positive map extends a hermitian preserving map extends a linear map, so the onX will just be the toLinearMap projections that exist anyway.)

[Kevin Buzzard]

We have things like docs#LinearMap.mulLeft if you want the linear map.

[Alex Meiburg]

Interesting, I'll take a look. Thanks a lot for the pointers