ContinuousLinearPMap

Stream: mathlib4

[Etienne Marion]

Hi, I'd like to add a type for continuous partial linear maps modeled on LinearPMap. I'd like to generalize lemmas like docs#LinearPMap.map_zero, docs#LinearPMap.map_add etc. so that they apply both to LinearPMap and ContinuousLinearPMap. However I don't know how to do that, the usual mechanism of using some class like docs#AddHomClass does not work because the domain depends on the map, I can't even provide a FunLike instance. Any suggestions are welcome!

[Yaël Dillies]

Do you know about docs#DFunLike ?

[Etienne Marion]

I do, but I don't see how it helps. f : LinearPMap R E F is a function from f.domain to F, so the domain depends on the function, while I was under the impression that a DFunLike instance just coerces to a dependent function type with a fixed domain.

[Yaël Dillies]

Ah, I see what you mean!

[Etienne Marion]

Maybe introducing a PFunLike class might work, but this would require a different notion of partial function than docs#PFun, and I don't feel like it's worth it, so I'll just duplicate lemmas.

[Jireh Loreaux]

Moritz Doll and I had a long discussion (it's in a public thread somewhere) about such a class, and using it in precisely this context. It was probably sometime during the port.

[Etienne Marion]

Found it here

[Etienne Marion]

I would be happy to try and implement this. My understanding of the typeclass inference is not so deep however, and I would need some guidance. Also, I had in mind that it would be easier to just define this separately from LinearMapClass rather than creating a LinearPMapClass instance for LinearMap. That would of course gives us two separate systems while one is a particular case of the other mathematically, so not very nice, but I don’t know if considering a LinearMap as a LinearPMap with domain top will give us something as smooth as what we have right now.

[Jireh Loreaux]

I think there should not be an instance for LinearMap for the reasons Moritz and I encountered in the other thread. Users should have to pass through an explicit equivalent between linear maps and the subtype of linear pmaps with domain = top.

[Etienne Marion]

I just opened #20663. It is a minimal implementation to get a LinearPMapClass instance for LinearPMap with basic mapping lemmas. I imitated the already existing system to build the hierarchy but did not implement all the different types of homs, only the homclasses.

It went well except for an issue because of (I suspect) the defeq LinearPMap.domain vs PFunLike.domain which is not always seen through. It appears at two places:

• In the file Algebra.Module.Injective in the theorem extension_property, the proof went h ▸ ⟨⟩ and it broke so I had to replace it with have : ... := h; this ▸ ⟨⟩ to get it to work, where ... is the same as h but replacing LinearPMap.domain with PFunLike.Domain.
• In the file LinearAlgebra.LinearPMap in the theorem supSpanSingleton_apply_mk, it had a simp attribute but did not pass the linter because it could not simplify itself. I removed the simp tag and nothing broke.

Apart from that replacing all the LinearPMap.map_add by pmap_add and so on went without any trouble. I'm not sure what should be added or removed in what I did. I think it's very minimal but I did not want to add too much in case I was going the wrong way.

[Jireh Loreaux]

At a (very brief) glance, it looks reasonable. Unfortunately, I probably won't have much time to look at it soon, as I'm about to be burdened with many commitments.