Continuous multilinear maps: assume `Finite ι` or not?

Stream: maths

[Yury G. Kudryashov]

If we have a continuous multilinear map (over a nontrivially normed field) on ∀ i, E i, then all but finitely many E i have to be trivial. This means that

• assuming [Finite ι] does not make the theorem less general;
• we can drop this assumption in most lemmas (and save a bit of time every time these lemmas are used).

So, should we assume [Finite ι] or not?

[Yaël Dillies]

Do you mean "cofinitely many E i"? Yes you do

[Yury G. Kudryashov]

E.g., in #10743 (not yet ready for a review) I don't assume [Finite ι] but it makes the proof a bit more complicated.

[Eric Wieser]

Doesn't the zero map still exist in the infinite case?

[Yury G. Kudryashov]

Yes, but we rarely want to build analysis around zero map.

[Yury G. Kudryashov]

... and #10743 is ready for review

[Eric Wieser]

Yury G. Kudryashov said:

Yes, but we rarely want to build analysis around zero map.

Is there a case where you might work with a dependently-typed family of maps, and the indexes are finite for only some of the families?

[Junyan Xu]

Yury G. Kudryashov said:

If we have a continuous multilinear map (over a nontrivially normed field) on ∀ i, E i, then all but finitely many E i have to be trivial.

Two issues with this statement:

• The "nontrivially normed field" condition is irrelevant; it suffices to assume that changing any coordinate to 0 changes the value to 0, which is implied by map_smul' (for any semiring). You do need to assume the codomain is T1, otherwise it could be some non-Hausdorff TVS over the reals, for example, and any multilinear map into the closure of {0} is continuous.

• The conclusion could just sayFinite ι rather than "all but finitely many E i are trivial"; in fact if some E i is trivial (no matter ι is finite or not), then 0 is the only multilinear map.

This is the most general result that I can prove: I think we can be satisfied with a Finite ι ∨ Subsingleton (ContinuousMultilinearMap E _) lemma. (Edit: maybe just use the finite_or_infinite dichotomy and the Subsingleton instance will apply in the second case.)

import Mathlib.Topology.Algebra.Module.Multilinear.Basic

theorem eq_default {ι} [Infinite ι] {X : ι → Type*} {Y} [∀ i, Inhabited (X i)] [Inhabited Y]
    [∀ i, TopologicalSpace (X i)] [TopologicalSpace Y] [T1Space Y] (f : C(∀ i, X i, Y))
    (hf : ∀ (x : ∀ i, X i) (i : ι), x i = default → f x = default) (x) :
    f x = default := by
  contrapose! hf
  obtain ⟨s, U, nhd, subset⟩ := isOpen_pi_iff.mp
    (isOpen_compl_singleton (x := default).preimage f.continuous) x hf
  obtain ⟨i, hi⟩ := Infinite.exists_not_mem_finset s
  classical
  use Function.update x i default, i, Function.update_same _ _ _
  apply subset; intro j hj
  rw [Function.update_noteq (ne_of_mem_of_not_mem hj hi)]
  exact (nhd j hj).2

instance (R) {ι} (M₁ : ι → Type*) (M₂) [Semiring R] [∀ i, AddCommMonoid (M₁ i)] [AddCommMonoid M₂]
    [∀ i, Module R (M₁ i)] [Module R M₂] [∀ i, TopologicalSpace (M₁ i)] [TopologicalSpace M₂]
    [Infinite ι] [T1Space M₂] : Subsingleton (ContinuousMultilinearMap R M₁ M₂) where
  allEq f g := DFunLike.ext f g fun x ↦
    letI (i) : Inhabited (M₁ i) := ⟨0⟩
    letI : Inhabited M₂ := ⟨0⟩
    (eq_default f (fun _ ↦ f.map_coord_zero) x).trans
      (eq_default ⟨g, g.cont⟩ (fun _ ↦ g.map_coord_zero) x).symm

[Junyan Xu]

I realized I didn't know an example of a nontrivial multilinear map with infinite indexing type, so I constructed one (golf welcome!) but then I realized docs#PiTensorProduct.tprod provide canonical examples (but mathlib doesn't know they are nontrivial yet).

import Mathlib.LinearAlgebra.Multilinear.Basic
import Mathlib.SetTheory.Cardinal.Basic

example {ι} : MultilinearMap Cardinal (fun _ : ι ↦ Cardinal) Cardinal where
  toFun := .prod
  map_add' f i x y := by
    simp_rw [Cardinal.prod, Cardinal.add_def, Cardinal.eq]
    refine ⟨.trans (.piSplitAt i _)
      (.trans ?_ <| .sumCongr (.symm <| .piSplitAt i _) <| .symm <| .piSplitAt i _)⟩
    have (z) : (∀ j : {j // j ≠ i}, Quotient.out (Function.update f i z j)) =
        ∀ j : {j // j ≠ i}, Quotient.out (f j) := by
      apply congr_arg (fun t : {j // j ≠ i} → Type _ ↦ ∀ j, t j)
      ext j; rw [Function.update_noteq j.2]
    simp_rw [Function.update_same, this]
    refine .trans (.prodCongrLeft fun _ ↦ Nonempty.some ?_) (.sumProdDistrib _ _ _)
    simp_rw [← Cardinal.eq, ← Cardinal.add_def, Cardinal.mk_out]
  map_smul' f i x y := by
    simp_rw [Cardinal.prod, smul_eq_mul]
    conv_rhs => rw [← x.mk_out, Cardinal.mul_def]
    refine Cardinal.eq.mpr ⟨.trans (.piSplitAt i _) <| .trans (.trans (.prodCongr (Nonempty.some ?_)
      <| .piCongrRight ?_) <| .prodAssoc _ _ _) <| .prodCongrRight fun _ ↦ .symm <| .piSplitAt i _⟩
    · simp_rw [Function.update_same, ← Cardinal.eq, ← Cardinal.mul_def, Cardinal.mk_out]
    · intro j; simp_rw [Function.update_noteq j.2]; rfl

[Antoine Chambert-Loir]

Whenever I browse the web about infinite tensor products, the results that pop out are in fields where the obvious stuff does not work, precisely because there are infinitely many indices.
So I'd guess that the generality is not so important and I'd suggest you to stay with [Finite _].

[Kevin Buzzard]

In the theory of automorphic representations an important notion is the restricted tensor product, where you have a family of (unital) rings and define the tensor product to be the direct limit over finite tensor products, with the embeddings coming from adding $\otimes_t 1$ at the places you're adding, and then if you have a family of modules over those rings together with fixed elements $v_i$ of each module then again you take the direct limit of finite products but extend by adding $\otimes_t v_i$ to define maps between the finite products.

[Yury G. Kudryashov]

Does it apply somehow to multilinear maps?

[Kevin Buzzard]

The theory is built up so that you can say the following thing. Given a family of (topological) groups $G_i$ with (closed) subgroups $K_i$ chosen for all $i$, the restricted product of the $G_i$ with respect to the $K_i$ is the subspace of the product of the $G_i$ consisting of $(g_i)$ with $g_i\in K_i$ for all but finitely many $i$. Given a (smooth) irreducible representation $V$ of the restricted product, it can be decomposed into a restricted tensor product $\bigotimes_i'V_i$ where $V_i$ is a representation of $G_i$ and $V_i^{K_i}$ has dimension 1 for almost all $i$ (and you choose nonzero vectors in these 1-d subspaces to make the restricted tensor product). There is as far as I remember no link to multilinear maps.

My plan was just to develop the theory (which is not too complex) from first principles when I need it for FLT.

[Antoine Chambert-Loir]

Yes, but I don't think it's the same theory. The restricted tensor product is a subset of the tensor product, while @Yury G. Kudryashov is interested in multilinear maps from the whole tensor product.
(I had these restricted tensor products in mind when I wrote that people want to do something else than the full tensor product when they have an infinite set of indices.)