feat(topology/algebra/multilinear): add a linear_equiv version of pi (#…

…8064)

This is a weaker version of `continuous_multilinear_map.piₗᵢ` that requires weaker typeclasses.

Unfortunately I don't understand why the typeclass system continues not to cooperate here, but I suspect it's the same class of problem that plagues `dfinsupp`.

src/analysis/normed_space/multilinear.lean

@@ -450,13 +450,12 @@ def piₗᵢ {ι' : Type v'} [fintype ι'] {E' : ι' → Type wE'} [Π i', norme
   @linear_isometry_equiv 𝕜 (Π i', continuous_multilinear_map 𝕜 E (E' i'))
     (continuous_multilinear_map 𝕜 E (Π i, E' i)) _ _ _
       (@pi.module ι' _ 𝕜 _ _ (λ i', infer_instance)) _ :=
-{ to_fun := pi,
-  map_add' := λ f g, rfl,
-  map_smul' := λ c f, rfl,
-  inv_fun := λ f i,
-    (@continuous_linear_map.proj 𝕜 _ _ E' _ _ _ i).comp_continuous_multilinear_map f,
-  left_inv := λ f, by { ext, refl },
-  right_inv := λ f, by { ext, refl },
+{ to_linear_equiv :=
+  -- note: `pi_linear_equiv` does not unify correctly here, presumably due to issues with dependent
+  -- typeclass arguments.
+  { map_add' := λ f g, rfl,
+    map_smul' := λ c f, rfl,
+    .. pi_equiv, },
   norm_map' := norm_pi }
 
 end

src/topology/algebra/mul_action.lean

@@ -245,3 +245,10 @@ instance [topological_space β] [has_scalar M α] [has_scalar M β] [has_continu
   has_continuous_smul M (α × β) :=
 ⟨(continuous_fst.smul (continuous_fst.comp continuous_snd)).prod_mk
   (continuous_fst.smul (continuous_snd.comp continuous_snd))⟩
+
+instance {ι : Type*} {γ : ι → Type}
+  [∀ i, topological_space (γ i)] [Π i, has_scalar M (γ i)] [∀ i, has_continuous_smul M (γ i)] :
+  has_continuous_smul M (Π i, γ i) :=
+⟨continuous_pi $ λ i,
+  (continuous_fst.smul continuous_snd).comp $
+    continuous_fst.prod_mk ((continuous_apply i).comp continuous_snd)⟩

src/topology/algebra/multilinear.lean

@@ -143,19 +143,19 @@ def prod (f : continuous_multilinear_map R M₁ M₂) (g : continuous_multilinea
 
 /-- Combine a family of continuous multilinear maps with the same domain and codomains `M' i` into a
 continuous multilinear map taking values in the space of functions `Π i, M' i`. -/
-def pi {ι' : Type*} {M' : ι' → Type*} [Π i, add_comm_group (M' i)] [Π i, topological_space (M' i)]
+def pi {ι' : Type*} {M' : ι' → Type*} [Π i, add_comm_monoid (M' i)] [Π i, topological_space (M' i)]
   [Π i, module R (M' i)] (f : Π i, continuous_multilinear_map R M₁ (M' i)) :
   continuous_multilinear_map R M₁ (Π i, M' i) :=
 { cont := continuous_pi $ λ i, (f i).coe_continuous,
   to_multilinear_map := multilinear_map.pi (λ i, (f i).to_multilinear_map) }
 
-@[simp] lemma coe_pi {ι' : Type*} {M' : ι' → Type*} [Π i, add_comm_group (M' i)]
+@[simp] lemma coe_pi {ι' : Type*} {M' : ι' → Type*} [Π i, add_comm_monoid (M' i)]
   [Π i, topological_space (M' i)] [Π i, module R (M' i)]
   (f : Π i, continuous_multilinear_map R M₁ (M' i)) :
   ⇑(pi f) = λ m j, f j m :=
 rfl
 
-lemma pi_apply {ι' : Type*} {M' : ι' → Type*} [Π i, add_comm_group (M' i)]
+lemma pi_apply {ι' : Type*} {M' : ι' → Type*} [Π i, add_comm_monoid (M' i)]
   [Π i, topological_space (M' i)] [Π i, module R (M' i)]
   (f : Π i, continuous_multilinear_map R M₁ (M' i)) (m : Π i, M₁ i) (j : ι') :
   pi f m j = f j m :=
@@ -175,6 +175,32 @@ def comp_continuous_linear_map
   g.comp_continuous_linear_map f m = g (λ i, f i $ m i) :=
 rfl
 
+/-- Composing a continuous multilinear map with a continuous linear map gives again a
+continuous multilinear map. -/
+def _root_.continuous_linear_map.comp_continuous_multilinear_map
+  (g : M₂ →L[R] M₃) (f : continuous_multilinear_map R M₁ M₂) :
+  continuous_multilinear_map R M₁ M₃ :=
+{ cont := g.cont.comp f.cont,
+  .. g.to_linear_map.comp_multilinear_map f.to_multilinear_map }
+
+@[simp] lemma _root_.continuous_linear_map.comp_continuous_multilinear_map_coe (g : M₂ →L[R] M₃)
+  (f : continuous_multilinear_map R M₁ M₂) :
+  ((g.comp_continuous_multilinear_map f) : (Πi, M₁ i) → M₃) =
+  (g : M₂ → M₃) ∘ (f : (Πi, M₁ i) → M₂) :=
+by { ext m, refl }
+
+
+/-- `continuous_multilinear_map.pi` as an `equiv`. -/
+@[simps]
+def pi_equiv {ι' : Type*} {M' : ι' → Type*} [Π i, add_comm_monoid (M' i)]
+  [Π i, topological_space (M' i)] [Π i, module R (M' i)] :
+  (Π i, continuous_multilinear_map R M₁ (M' i)) ≃
+  continuous_multilinear_map R M₁ (Π i, M' i) :=
+{ to_fun := continuous_multilinear_map.pi,
+  inv_fun := λ f i, (continuous_linear_map.proj i : _ →L[R] M' i).comp_continuous_multilinear_map f,
+  left_inv := λ f, by { ext, refl },
+  right_inv := λ f, by { ext, refl } }
+
 /-- In the specific case of continuous multilinear maps on spaces indexed by `fin (n+1)`, where one
 can build an element of `Π(i : fin (n+1)), M i` using `cons`, one can express directly the
 additivity of a multilinear map along the first variable. -/
@@ -323,7 +349,6 @@ instance : module R' (continuous_multilinear_map A M₁ M₂) :=
   add_smul := λ r₁ r₂ f, ext $ λ x, add_smul _ _ _,
   zero_smul := λ f, ext $ λ x, zero_smul _ _ }
 
-
 /-- Linear map version of the map `to_multilinear_map` associating to a continuous multilinear map
 the corresponding multilinear map. -/
 @[simps] def to_multilinear_map_linear :
@@ -332,26 +357,21 @@ the corresponding multilinear map. -/
   map_add'  := λ f g, rfl,
   map_smul' := λ c f, rfl }
 
+/-- `continuous_multilinear_map.pi` as a `linear_equiv`. -/
+@[simps {simp_rhs := tt}]
+def pi_linear_equiv {ι' : Type*} {M' : ι' → Type*}
+  [Π i, add_comm_monoid (M' i)] [Π i, topological_space (M' i)] [∀ i, has_continuous_add (M' i)]
+  [Π i, module R' (M' i)] [Π i, module A (M' i)] [∀ i, is_scalar_tower R' A (M' i)]
+  [Π i, has_continuous_smul R' (M' i)] :
+  -- typeclass search doesn't find this instance, presumably due to struggles converting
+  -- `Π i, module R (M' i)` to `Π i, has_scalar R (M' i)` in dependent arguments.
+  let inst : has_continuous_smul R' (Π i, M' i) := pi.has_continuous_smul in
+  (Π i, continuous_multilinear_map A M₁ (M' i)) ≃ₗ[R']
+    continuous_multilinear_map A M₁ (Π i, M' i) :=
+{ map_add' := λ x y, rfl,
+  map_smul' := λ c x, rfl,
+  .. pi_equiv }
+
 end comm_semiring
 
 end continuous_multilinear_map
-
-namespace continuous_linear_map
-variables [ring R] [∀i, add_comm_group (M₁ i)] [add_comm_group M₂] [add_comm_group M₃]
-[∀i, module R (M₁ i)] [module R M₂] [module R M₃]
-[∀i, topological_space (M₁ i)] [topological_space M₂] [topological_space M₃]
-
-/-- Composing a continuous multilinear map with a continuous linear map gives again a
-continuous multilinear map. -/
-def comp_continuous_multilinear_map (g : M₂ →L[R] M₃) (f : continuous_multilinear_map R M₁ M₂) :
-  continuous_multilinear_map R M₁ M₃ :=
-{ cont := g.cont.comp f.cont,
-  .. g.to_linear_map.comp_multilinear_map f.to_multilinear_map }
-
-@[simp] lemma comp_continuous_multilinear_map_coe (g : M₂ →L[R] M₃)
-  (f : continuous_multilinear_map R M₁ M₂) :
-  ((g.comp_continuous_multilinear_map f) : (Πi, M₁ i) → M₃) =
-  (g : M₂ → M₃) ∘ (f : (Πi, M₁ i) → M₂) :=
-by { ext m, refl }
-
-end continuous_linear_map