Lifting a Pi-type linear map to a linear map

Stream: Is there code for X?

[Alex Meiburg]

I'm looking for this:

def LinearMap.pi_lift [Ring R] [AddCommMonoid M] [Module R M]
    (fs : α → (M →ₗ[R] R)) : (α → M) →ₗ[R] R := by
  sorry

where (α → M) has the natural Module structure as a pi-type. I would also like the corresponding thing for AffineMap. I suspect the answer may lie with TensorProduct but I'm not sure. Loogle turned up nothing:
https://loogle.lean-lang.org/?q=%22LinearMap%22%2C+%28%3Fa+%E2%86%92+%28LinearMap+%3Fr+%3Fm+_%29%29+-%3E+%28LinearMap+%3Fr+%28%3Fa+-%3E+%3Fm%29+_%29

[Alex Meiburg]

The affine one (which is the one I really need I guess) would be

def AffineMap.pi_lift [Ring R] [AddCommMonoid M] [Module R M] [AddTorsor R M]
    (fs : α → (M →ᵃ[R] R)) : (α → M) →ᵃ[R] R := by
  sorry

[Kim Morrison]

I don't think this exists (mathematically). Can you describe what the output should be in a simple example (e.g. α = Fin 2, M = R)?

[Kevin Buzzard]

In case you're thinking "both sides are surely the same because function composition is associative" or something -- that's ∘. The pi type → is not in general associative, for the same reason that ^ isn't. The numbers 3^(1^2) and (3^1)^2 are different -- one is 3 and one is 3^2.

[Kevin Buzzard]

But the size of A → B is $b^a$ if $a,b$ are the sizes of A and B.

[Alex Meiburg]

Right, I'm aware that -> isn't associative, but I think this exists. For a=Fin 2 and M=R, the original form fs is a pair of linear maps R -> R.

In the image, (Fin 2->R) is the free rank-2 module over R. This already exists as an instance in mathlib. If I label the basis elements of that module as b0 and b1, I get a linear map defined by mapping b0 to ((fs 0) 1), and mapping b1 to ((fs 1) 1). Those extend to a full linear map in the natural way then

[Kim Morrison]

You will need to say either finitely supported functions on α, or add a hypothesis that α is finite.

Then you can define your function on f as a sum over i : α of fs i (f i).

[Alex Meiburg]

Mm, so [Fintype a]?

[Kevin Buzzard]

I think [Finite a] is easier to prove with (but harder to compute with)

[Alex Meiburg]

Turns out I had myself mixed up and this wasn't even what I wanted :joy:
I actually just wanted docs#LinearMap.pi

[Alex Meiburg]

Which helped me quickly write the Affine one (which I think doesn't exist otherwise):

def AffineMap.pi [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R M₂]
    (fs : α → (M →ᵃ[R] M₂)) : M →ᵃ[R] (α → M₂) :=
  ⟨fun m a ↦ (fs a).1 m, LinearMap.pi (AffineMap.linear ∘ fs),
   fun _ _ ↦ funext fun a ↦ (fs a).3 _ _⟩

[Eric Wieser]

It would be better style to write that using where, but otherwise that would be a good PR

[Eric Wieser]

Oh, and it should be defined for an arbitrary affine space, not just a module!

[Junyan Xu]

Alex Meiburg said:

I'm looking for this:

def LinearMap.pi_lift [Ring R] [AddCommMonoid M] [Module R M]
    (fs : α → (M →ₗ[R] R)) : (α → M) →ₗ[R] R := by
  sorry

With the α → M replaced by Finsupp α M, this is docs#Finsupp.lsum (you also need R to be commutative).

[Alex Meiburg]

Eric Wieser said:

It would be better style to write that using where, but otherwise that would be a good PR

Done! mathlib4#10147