linear map forgetting variables

Stream: mathlib4

[Sébastien Gouëzel]

Given a set s in a type ι, do we have in mathlib the linear map forgetting the coordinates not in s, i.e., ((i : ι) → E₁ i) →ₗ[𝕜] ((i : s) → E₁ i)? I looked for this and for a more general version, replacing the inclusion of s in univ with a general embedding, but I couldn't find it. It's one of these cases where I don't know a good tool to look for these constructions (and there are so many constructions in linear algebra!) (loogle and grep both failed me), so if you have tricks I'm all ears!

[Floris van Doorn]

My strategy is too look manually through Mathlib/LinearAlgebra/Pi.lean, but I don't find that there, so I think it's missing. It should be formulated as the non-equiv version of docs#LinearEquiv.piCongrLeft.

[Adam Topaz]

This should be restriction along the inclusion of s.

[Adam Topaz]

import Mathlib

example {X Y R : Type*} (f : X → Y) [Ring R] : (Y → R) →ₗ[R] (X → R) := LinearMap.funLeft
  R R f

found with exact? :tada:

[Adam Topaz]

oh but you want the dependent product. Does that work? (no :( )

[Sébastien Gouëzel]

Suppose I didn't want the dependent version (which I do). Can you explain how I could have guessed the name funLeft? Is that a standard name scheme in this corner of the library? (It's not even clear to me if fun means function -- because f is a function -- or functor -- since this is the canonical contravariant functor in this setting).

[Adam Topaz]

Well, here's the cleanest version I could come up with:

example {X R : Type*} {EX : X → Type*} [Ring R]
   [∀ x, AddCommGroup (EX x)]
   [∀ x, Module R (EX x)]
   (S : Set X)
   :
   ((x : X) → EX x) →ₗ[R] ((s : S) → EX s) := LinearMap.pi fun i => LinearMap.proj i.val

[Adam Topaz]

I mostly used exact?% and followed my nose.

[Adam Topaz]

It seems that this is just missing.

[Adam Topaz]

I also found funLeft with exact?%.

[Adam Topaz]

FWIW, I think funLeft is quite a bad name. I think it should have precompose or something like that in the name.

[Adam Topaz]

It's possible I don't work in the most efficient way, but I tend to prefer using tools in lean itself over going for loogle/moogle. I use loogle/moogle as a last resort.

[Sébastien Gouëzel]

Thanks!

[Jireh Loreaux]

We have these pre/post-composition defs all over the library, but the naming is absolutely awful (in terms of consistency). There's comp and comp' in some places (you get to guess which is which), or compLeft and compRight (again, you get to guess which is which).

I propose we come up with a standard naming scheme for these, and add it to #naming.

[Jireh Loreaux]

I think precomp and postcomp are clearer that compLeft and compRight, but maybe that's just my own bias showing.

[Eric Wieser]

Part of the problem is that you need to talk about compositions of Hom1s as a Hom2

[Eric Wieser]

Where here Hom1 is just a regular function, and Hom2 is a linear map

[Eric Wieser]

But we also definitely care about the cases where both are linear maps

[Eric Wieser]

And at least theoretically could care about the case where one is only an AddMonoidHom...

[Jireh Loreaux]

I don't think that's a problem? Or at least, it's a separate one? I'm talking about the distinction between docs#ContinuousMap.compStarAlgHom and docs#ContinuousMap.compStarAlgHom', for instance.

[Anatole Dedecker]

I think the point is there are a bunch of naming issues merging here x) I suggested some time ago that bundlings of the "same" function with different hom types could be named function.asSomeType, e.g docs#ContinuousLinearMap.compL could be ContinuousLinearMap.comp.asCLM or something like this.

[Anatole Dedecker]

But I agree this is not precisely the issue at play here.