Documentation

Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm

Injective seminorm on the tensor of a finite family of normed spaces. #

Let π•œ be a nontrivially normed field and E be a family of normed π•œ-vector spaces Eα΅’, indexed by a finite type ΞΉ. We define a seminorm on ⨂[π•œ] i, Eα΅’, which we call the "injective seminorm". It is chosen to satisfy the following property: for every normed π•œ-vector space F, the linear equivalence MultilinearMap π•œ E F ≃ₗ[π•œ] (⨂[π•œ] i, Eα΅’) β†’β‚—[π•œ] F expressing the universal property of the tensor product induces an isometric linear equivalence ContinuousMultilinearMap π•œ E F ≃ₗᡒ[π•œ] (⨂[π•œ] i, Eα΅’) β†’L[π•œ] F.

The idea is the following: Every normed π•œ-vector space F defines a linear map from ⨂[π•œ] i, Eα΅’ to ContinuousMultilinearMap π•œ E F β†’β‚—[π•œ] F, which sends x to the map f ↦ f.lift x. Thanks to PiTensorProduct.norm_eval_le_projectiveSeminorm, this map lands in ContinuousMultilinearMap π•œ E F β†’L[π•œ] F. As this last space has a natural operator (semi)norm, we get an induced seminorm on ⨂[π•œ] i, Eα΅’, which, by PiTensorProduct.norm_eval_le_projectiveSeminorm, is bounded above by the projective seminorm PiTensorProduct.projectiveSeminorm. We then take the sup of these seminorms as F varies; as this family of seminorms is bounded, its sup has good properties.

In fact, we cannot take the sup over all normed spaces F because of set-theoretical issues, so we only take spaces F in the same universe as ⨂[π•œ] i, Eα΅’. We prove in norm_eval_le_injectiveSeminorm that this gives the same result, because every multilinear map from E = Ξ α΅’ Eα΅’ to F factors though a normed vector space in the same universe as ⨂[π•œ] i, Eα΅’.

We then prove the universal property and the functoriality of ⨂[π•œ] i, Eα΅’ as a normed vector space.

Main definitions #

Main results #

TODO #

@[simp]
theorem PiTensorProduct.toDualContinuousMultilinearMap_apply_toFun {ΞΉ : Type uΞΉ} [Fintype ΞΉ] {π•œ : Type uπ•œ} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] (F : Type uF) [SeminormedAddCommGroup F] [NormedSpace π•œ F] (x : PiTensorProduct π•œ fun (i : ΞΉ) => E i) :
βˆ€ (a : ContinuousMultilinearMap π•œ E F), ((PiTensorProduct.toDualContinuousMultilinearMap F) x) a = (PiTensorProduct.lift a.toMultilinearMap) x
@[simp]
theorem PiTensorProduct.toDualContinuousMultilinearMap_apply_apply {ΞΉ : Type uΞΉ} [Fintype ΞΉ] {π•œ : Type uπ•œ} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] (F : Type uF) [SeminormedAddCommGroup F] [NormedSpace π•œ F] (x : PiTensorProduct π•œ fun (i : ΞΉ) => E i) :
βˆ€ (a : ContinuousMultilinearMap π•œ E F), ((PiTensorProduct.toDualContinuousMultilinearMap F) x) a = (PiTensorProduct.lift a.toMultilinearMap) x
noncomputable def PiTensorProduct.toDualContinuousMultilinearMap {ΞΉ : Type uΞΉ} [Fintype ΞΉ] {π•œ : Type uπ•œ} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] (F : Type uF) [SeminormedAddCommGroup F] [NormedSpace π•œ F] :
(PiTensorProduct π•œ fun (i : ΞΉ) => E i) β†’β‚—[π•œ] ContinuousMultilinearMap π•œ E F β†’L[π•œ] F

The linear map from ⨂[π•œ] i, Eα΅’ to ContinuousMultilinearMap π•œ E F β†’L[π•œ] F sending x in ⨂[π•œ] i, Eα΅’ to the map f ↦ f.lift x.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem PiTensorProduct.toDualContinuousMultilinearMap_le_projectiveSeminorm {ΞΉ : Type uΞΉ} [Fintype ΞΉ] {π•œ : Type uπ•œ} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] {F : Type uF} [SeminormedAddCommGroup F] [NormedSpace π•œ F] (x : PiTensorProduct π•œ fun (i : ΞΉ) => E i) :
    β€–(PiTensorProduct.toDualContinuousMultilinearMap F) xβ€– ≀ PiTensorProduct.projectiveSeminorm x
    @[irreducible]
    noncomputable def PiTensorProduct.injectiveSeminorm {ΞΉ : Type u_1} [Fintype ΞΉ] {π•œ : Type u_2} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type u_3} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] :
    Seminorm π•œ (PiTensorProduct π•œ fun (i : ΞΉ) => E i)

    The injective seminorm on ⨂[π•œ] i, Eα΅’. Morally, it sends x in ⨂[π•œ] i, Eα΅’ to the sup of the operator norms of the PiTensorProduct.toDualContinuousMultilinearMap F x, for all normed vector spaces F. In fact, we only take in the same universe as ⨂[π•œ] i, Eα΅’, and then prove in PiTensorProduct.norm_eval_le_injectiveSeminorm that this gives the same result.

    Equations
    Instances For
      theorem PiTensorProduct.injectiveSeminorm_def {ΞΉ : Type u_1} [Fintype ΞΉ] {π•œ : Type u_2} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type u_3} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] :
      PiTensorProduct.injectiveSeminorm = sSup {p : Seminorm π•œ (PiTensorProduct π•œ fun (i : ΞΉ) => E i) | βˆƒ (G : Type (max u_1 u_2 u_3)) (x : SeminormedAddCommGroup G) (x_1 : NormedSpace π•œ G), p = (normSeminorm π•œ (ContinuousMultilinearMap π•œ E G β†’L[π•œ] G)).comp (PiTensorProduct.toDualContinuousMultilinearMap G)}
      theorem PiTensorProduct.dualSeminorms_bounded {ΞΉ : Type uΞΉ} [Fintype ΞΉ] {π•œ : Type uπ•œ} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] :
      BddAbove {p : Seminorm π•œ (PiTensorProduct π•œ fun (i : ΞΉ) => E i) | βˆƒ (G : Type (max uΞΉ uπ•œ uE)) (x : SeminormedAddCommGroup G) (x_1 : NormedSpace π•œ G), p = (normSeminorm π•œ (ContinuousMultilinearMap π•œ E G β†’L[π•œ] G)).comp (PiTensorProduct.toDualContinuousMultilinearMap G)}
      theorem PiTensorProduct.injectiveSeminorm_apply {ΞΉ : Type uΞΉ} [Fintype ΞΉ] {π•œ : Type uπ•œ} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] (x : PiTensorProduct π•œ fun (i : ΞΉ) => E i) :
      PiTensorProduct.injectiveSeminorm x = ⨆ (p : ↑{p : Seminorm π•œ (PiTensorProduct π•œ fun (i : ΞΉ) => E i) | βˆƒ (G : Type (max uΞΉ uπ•œ uE)) (x : SeminormedAddCommGroup G) (x_1 : NormedSpace π•œ G), p = (normSeminorm π•œ (ContinuousMultilinearMap π•œ E G β†’L[π•œ] G)).comp (PiTensorProduct.toDualContinuousMultilinearMap G)}), ↑p x
      theorem PiTensorProduct.norm_eval_le_injectiveSeminorm {ΞΉ : Type uΞΉ} [Fintype ΞΉ] {π•œ : Type uπ•œ} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] {F : Type uF} [SeminormedAddCommGroup F] [NormedSpace π•œ F] (f : ContinuousMultilinearMap π•œ E F) (x : PiTensorProduct π•œ fun (i : ΞΉ) => E i) :
      β€–(PiTensorProduct.lift f.toMultilinearMap) xβ€– ≀ β€–fβ€– * PiTensorProduct.injectiveSeminorm x
      theorem PiTensorProduct.injectiveSeminorm_le_projectiveSeminorm {ΞΉ : Type uΞΉ} [Fintype ΞΉ] {π•œ : Type uπ•œ} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] :
      PiTensorProduct.injectiveSeminorm ≀ PiTensorProduct.projectiveSeminorm
      theorem PiTensorProduct.injectiveSeminorm_tprod_le {ΞΉ : Type uΞΉ} [Fintype ΞΉ] {π•œ : Type uπ•œ} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] (m : (i : ΞΉ) β†’ E i) :
      PiTensorProduct.injectiveSeminorm (β¨‚β‚œ[π•œ] (i : ΞΉ), m i) ≀ ∏ i : ΞΉ, β€–m iβ€–
      noncomputable instance PiTensorProduct.instSeminormedAddCommGroup {ΞΉ : Type uΞΉ} [Fintype ΞΉ] {π•œ : Type uπ•œ} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] :
      SeminormedAddCommGroup (PiTensorProduct π•œ fun (i : ΞΉ) => E i)
      Equations
      • PiTensorProduct.instSeminormedAddCommGroup = PiTensorProduct.injectiveSeminorm.toSeminormedAddCommGroup
      noncomputable instance PiTensorProduct.instNormedSpace {ΞΉ : Type uΞΉ} [Fintype ΞΉ] {π•œ : Type uπ•œ} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] :
      NormedSpace π•œ (PiTensorProduct π•œ fun (i : ΞΉ) => E i)
      Equations
      @[simp]
      theorem PiTensorProduct.liftEquiv_apply {ΞΉ : Type uΞΉ} [Fintype ΞΉ] (π•œ : Type uπ•œ) [NontriviallyNormedField π•œ] (E : ΞΉ β†’ Type uE) [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] (F : Type uF) [SeminormedAddCommGroup F] [NormedSpace π•œ F] (f : ContinuousMultilinearMap π•œ E F) :
      (PiTensorProduct.liftEquiv π•œ E F) f = (PiTensorProduct.lift f.toMultilinearMap).mkContinuous β€–fβ€– β‹―
      @[simp]
      theorem PiTensorProduct.liftEquiv_symm_apply {ΞΉ : Type uΞΉ} [Fintype ΞΉ] (π•œ : Type uπ•œ) [NontriviallyNormedField π•œ] (E : ΞΉ β†’ Type uE) [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] (F : Type uF) [SeminormedAddCommGroup F] [NormedSpace π•œ F] (l : (PiTensorProduct π•œ fun (i : ΞΉ) => E i) β†’L[π•œ] F) :
      (PiTensorProduct.liftEquiv π•œ E F).symm l = (PiTensorProduct.lift.symm ↑l).mkContinuous β€–lβ€– β‹―
      noncomputable def PiTensorProduct.liftEquiv {ΞΉ : Type uΞΉ} [Fintype ΞΉ] (π•œ : Type uπ•œ) [NontriviallyNormedField π•œ] (E : ΞΉ β†’ Type uE) [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] (F : Type uF) [SeminormedAddCommGroup F] [NormedSpace π•œ F] :
      ContinuousMultilinearMap π•œ E F ≃ₗ[π•œ] (PiTensorProduct π•œ fun (i : ΞΉ) => E i) β†’L[π•œ] F

      The linear equivalence between ContinuousMultilinearMap π•œ E F and (⨂[π•œ] i, Eα΅’) β†’L[π•œ] F induced by PiTensorProduct.lift, for every normed space F.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        noncomputable def PiTensorProduct.liftIsometry {ΞΉ : Type uΞΉ} [Fintype ΞΉ] (π•œ : Type uπ•œ) [NontriviallyNormedField π•œ] (E : ΞΉ β†’ Type uE) [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] (F : Type uF) [SeminormedAddCommGroup F] [NormedSpace π•œ F] :
        ContinuousMultilinearMap π•œ E F ≃ₗᡒ[π•œ] (PiTensorProduct π•œ fun (i : ΞΉ) => E i) β†’L[π•œ] F

        For a normed space F, we have constructed in PiTensorProduct.liftEquiv the canonical linear equivalence between ContinuousMultilinearMap π•œ E F and (⨂[π•œ] i, Eα΅’) β†’L[π•œ] F (induced by PiTensorProduct.lift). Here we give the upgrade of this equivalence to an isometric linear equivalence; in particular, it is a continuous linear equivalence.

        Equations
        Instances For
          @[simp]
          theorem PiTensorProduct.liftIsometry_apply_apply {ΞΉ : Type uΞΉ} [Fintype ΞΉ] {π•œ : Type uπ•œ} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] {F : Type uF} [SeminormedAddCommGroup F] [NormedSpace π•œ F] (f : ContinuousMultilinearMap π•œ E F) (x : PiTensorProduct π•œ fun (i : ΞΉ) => E i) :
          ((PiTensorProduct.liftIsometry π•œ E F) f) x = (PiTensorProduct.lift f.toMultilinearMap) x
          @[simp]
          theorem PiTensorProduct.tprodL_toFun {ΞΉ : Type uΞΉ} [Fintype ΞΉ] (π•œ : Type uπ•œ) [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] :
          βˆ€ (a : (i : ΞΉ) β†’ E i), (PiTensorProduct.tprodL π•œ) a = (PiTensorProduct.tprod π•œ) a
          @[simp]
          theorem PiTensorProduct.tprodL_apply {ΞΉ : Type uΞΉ} [Fintype ΞΉ] (π•œ : Type uπ•œ) [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] :
          βˆ€ (a : (i : ΞΉ) β†’ E i), (PiTensorProduct.tprodL π•œ) a = (PiTensorProduct.tprod π•œ) a
          noncomputable def PiTensorProduct.tprodL {ΞΉ : Type uΞΉ} [Fintype ΞΉ] (π•œ : Type uπ•œ) [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] :
          ContinuousMultilinearMap π•œ E (PiTensorProduct π•œ fun (i : ΞΉ) => E i)

          The canonical continuous multilinear map from E = Ξ α΅’ Eα΅’ to ⨂[π•œ] i, Eα΅’.

          Equations
          Instances For
            @[simp]
            theorem PiTensorProduct.tprodL_coe {ΞΉ : Type uΞΉ} [Fintype ΞΉ] {π•œ : Type uπ•œ} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] :
            (PiTensorProduct.tprodL π•œ).toMultilinearMap = PiTensorProduct.tprod π•œ
            @[simp]
            theorem PiTensorProduct.liftIsometry_symm_apply {ΞΉ : Type uΞΉ} [Fintype ΞΉ] {π•œ : Type uπ•œ} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] {F : Type uF} [SeminormedAddCommGroup F] [NormedSpace π•œ F] (l : (PiTensorProduct π•œ fun (i : ΞΉ) => E i) β†’L[π•œ] F) :
            (PiTensorProduct.liftIsometry π•œ E F).symm l = l.compContinuousMultilinearMap (PiTensorProduct.tprodL π•œ)
            @[simp]
            theorem PiTensorProduct.liftIsometry_tprodL {ΞΉ : Type uΞΉ} [Fintype ΞΉ] {π•œ : Type uπ•œ} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] :
            (PiTensorProduct.liftIsometry π•œ E (PiTensorProduct π•œ fun (i : ΞΉ) => E i)) (PiTensorProduct.tprodL π•œ) = ContinuousLinearMap.id π•œ (PiTensorProduct π•œ fun (i : ΞΉ) => E i)
            noncomputable def PiTensorProduct.mapL {ΞΉ : Type uΞΉ} [Fintype ΞΉ] {π•œ : Type uπ•œ} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] {E' : ΞΉ β†’ Type u_1} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E' i)] (f : (i : ΞΉ) β†’ E i β†’L[π•œ] E' i) :
            (PiTensorProduct π•œ fun (i : ΞΉ) => E i) β†’L[π•œ] PiTensorProduct π•œ fun (i : ΞΉ) => E' i

            Let Eα΅’ and E'α΅’ be two families of normed π•œ-vector spaces. Let f be a family of continuous π•œ-linear maps between Eα΅’ and E'α΅’, i.e. f : Ξ α΅’ Eα΅’ β†’L[π•œ] E'α΅’, then there is an induced continuous linear map ⨂ᡒ Eα΅’ β†’ ⨂ᡒ E'α΅’ by ⨂ aα΅’ ↦ ⨂ fα΅’ aα΅’.

            Equations
            Instances For
              @[simp]
              theorem PiTensorProduct.mapL_coe {ΞΉ : Type uΞΉ} [Fintype ΞΉ] {π•œ : Type uπ•œ} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] {E' : ΞΉ β†’ Type u_1} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E' i)] (f : (i : ΞΉ) β†’ E i β†’L[π•œ] E' i) :
              ↑(PiTensorProduct.mapL f) = PiTensorProduct.map fun (i : ΞΉ) => ↑(f i)
              @[simp]
              theorem PiTensorProduct.mapL_apply {ΞΉ : Type uΞΉ} [Fintype ΞΉ] {π•œ : Type uπ•œ} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] {E' : ΞΉ β†’ Type u_1} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E' i)] (f : (i : ΞΉ) β†’ E i β†’L[π•œ] E' i) (x : PiTensorProduct π•œ fun (i : ΞΉ) => E i) :
              (PiTensorProduct.mapL f) x = (PiTensorProduct.map fun (i : ΞΉ) => ↑(f i)) x
              noncomputable def PiTensorProduct.mapLIncl {ΞΉ : Type uΞΉ} [Fintype ΞΉ] {π•œ : Type uπ•œ} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] (p : (i : ΞΉ) β†’ Submodule π•œ (E i)) :
              (PiTensorProduct π•œ fun (i : ΞΉ) => β†₯(p i)) β†’L[π•œ] PiTensorProduct π•œ fun (i : ΞΉ) => E i

              Given submodules pα΅’ βŠ† Eα΅’, this is the natural map: ⨂[π•œ] i, pα΅’ β†’ ⨂[π•œ] i, Eα΅’. This is the continuous version of PiTensorProduct.mapIncl.

              Equations
              Instances For
                theorem PiTensorProduct.mapL_comp {ΞΉ : Type uΞΉ} [Fintype ΞΉ] {π•œ : Type uπ•œ} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] {E' : ΞΉ β†’ Type u_1} {E'' : ΞΉ β†’ Type u_2} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E' i)] [(i : ΞΉ) β†’ SeminormedAddCommGroup (E'' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E'' i)] (g : (i : ΞΉ) β†’ E' i β†’L[π•œ] E'' i) (f : (i : ΞΉ) β†’ E i β†’L[π•œ] E' i) :
                (PiTensorProduct.mapL fun (i : ΞΉ) => (g i).comp (f i)) = (PiTensorProduct.mapL g).comp (PiTensorProduct.mapL f)
                theorem PiTensorProduct.liftIsometry_comp_mapL {ΞΉ : Type uΞΉ} [Fintype ΞΉ] {π•œ : Type uπ•œ} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] {F : Type uF} [SeminormedAddCommGroup F] [NormedSpace π•œ F] {E' : ΞΉ β†’ Type u_1} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E' i)] (f : (i : ΞΉ) β†’ E i β†’L[π•œ] E' i) (h : ContinuousMultilinearMap π•œ E' F) :
                ((PiTensorProduct.liftIsometry π•œ E' F) h).comp (PiTensorProduct.mapL f) = (PiTensorProduct.liftIsometry π•œ E F) (h.compContinuousLinearMap f)
                @[simp]
                theorem PiTensorProduct.mapL_id {ΞΉ : Type uΞΉ} [Fintype ΞΉ] {π•œ : Type uπ•œ} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] :
                (PiTensorProduct.mapL fun (i : ΞΉ) => ContinuousLinearMap.id π•œ (E i)) = ContinuousLinearMap.id π•œ (PiTensorProduct π•œ fun (i : ΞΉ) => E i)
                @[simp]
                theorem PiTensorProduct.mapL_one {ΞΉ : Type uΞΉ} [Fintype ΞΉ] {π•œ : Type uπ•œ} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] :
                (PiTensorProduct.mapL fun (i : ΞΉ) => 1) = 1
                theorem PiTensorProduct.mapL_mul {ΞΉ : Type uΞΉ} [Fintype ΞΉ] {π•œ : Type uπ•œ} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] (f₁ : (i : ΞΉ) β†’ E i β†’L[π•œ] E i) (fβ‚‚ : (i : ΞΉ) β†’ E i β†’L[π•œ] E i) :
                (PiTensorProduct.mapL fun (i : ΞΉ) => f₁ i * fβ‚‚ i) = PiTensorProduct.mapL f₁ * PiTensorProduct.mapL fβ‚‚
                @[simp]
                theorem PiTensorProduct.mapLMonoidHom_apply {ΞΉ : Type uΞΉ} [Fintype ΞΉ] {π•œ : Type uπ•œ} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] (f : (i : ΞΉ) β†’ E i β†’L[π•œ] E i) :
                PiTensorProduct.mapLMonoidHom f = PiTensorProduct.mapL f
                noncomputable def PiTensorProduct.mapLMonoidHom {ΞΉ : Type uΞΉ} [Fintype ΞΉ] {π•œ : Type uπ•œ} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] :
                ((i : ΞΉ) β†’ E i β†’L[π•œ] E i) β†’* (PiTensorProduct π•œ fun (i : ΞΉ) => E i) β†’L[π•œ] PiTensorProduct π•œ fun (i : ΞΉ) => E i

                Upgrading PiTensorProduct.mapL to a MonoidHom when E = E'.

                Equations
                • PiTensorProduct.mapLMonoidHom = { toFun := PiTensorProduct.mapL, map_one' := β‹―, map_mul' := β‹― }
                Instances For
                  @[simp]
                  theorem PiTensorProduct.mapL_pow {ΞΉ : Type uΞΉ} [Fintype ΞΉ] {π•œ : Type uπ•œ} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] (f : (i : ΞΉ) β†’ E i β†’L[π•œ] E i) (n : β„•) :
                  theorem PiTensorProduct.mapL_add {ΞΉ : Type uΞΉ} [Fintype ΞΉ] {π•œ : Type uπ•œ} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] {E' : ΞΉ β†’ Type u_1} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E' i)] (f : (i : ΞΉ) β†’ E i β†’L[π•œ] E' i) [DecidableEq ΞΉ] (i : ΞΉ) (u : E i β†’L[π•œ] E' i) (v : E i β†’L[π•œ] E' i) :
                  theorem PiTensorProduct.mapL_smul {ΞΉ : Type uΞΉ} [Fintype ΞΉ] {π•œ : Type uπ•œ} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] {E' : ΞΉ β†’ Type u_1} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E' i)] (f : (i : ΞΉ) β†’ E i β†’L[π•œ] E' i) [DecidableEq ΞΉ] (i : ΞΉ) (c : π•œ) (u : E i β†’L[π•œ] E' i) :
                  theorem PiTensorProduct.mapL_opNorm {ΞΉ : Type uΞΉ} [Fintype ΞΉ] {π•œ : Type uπ•œ} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] {E' : ΞΉ β†’ Type u_1} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E' i)] (f : (i : ΞΉ) β†’ E i β†’L[π•œ] E' i) :
                  @[simp]
                  theorem PiTensorProduct.mapLMultilinear_apply_toFun {ΞΉ : Type uΞΉ} [Fintype ΞΉ] (π•œ : Type uπ•œ) [NontriviallyNormedField π•œ] (E : ΞΉ β†’ Type uE) [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] (E' : ΞΉ β†’ Type u_1) [(i : ΞΉ) β†’ SeminormedAddCommGroup (E' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E' i)] (f : (i : ΞΉ) β†’ E i β†’L[π•œ] E' i) :
                  βˆ€ (a : PiTensorProduct π•œ fun (i : ΞΉ) => E i), ((PiTensorProduct.mapLMultilinear π•œ E E') f) a = (PiTensorProduct.liftAux ((PiTensorProduct.tprodL π•œ).compContinuousLinearMap f).toMultilinearMap) a
                  @[simp]
                  theorem PiTensorProduct.mapLMultilinear_apply_apply {ΞΉ : Type uΞΉ} [Fintype ΞΉ] (π•œ : Type uπ•œ) [NontriviallyNormedField π•œ] (E : ΞΉ β†’ Type uE) [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] (E' : ΞΉ β†’ Type u_1) [(i : ΞΉ) β†’ SeminormedAddCommGroup (E' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E' i)] (f : (i : ΞΉ) β†’ E i β†’L[π•œ] E' i) :
                  βˆ€ (a : PiTensorProduct π•œ fun (i : ΞΉ) => E i), ((PiTensorProduct.mapLMultilinear π•œ E E') f) a = (PiTensorProduct.liftAux ((PiTensorProduct.tprodL π•œ).compContinuousLinearMap f).toMultilinearMap) a
                  @[simp]
                  theorem PiTensorProduct.mapLMultilinear_toFun_apply {ΞΉ : Type uΞΉ} [Fintype ΞΉ] (π•œ : Type uπ•œ) [NontriviallyNormedField π•œ] (E : ΞΉ β†’ Type uE) [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] (E' : ΞΉ β†’ Type u_1) [(i : ΞΉ) β†’ SeminormedAddCommGroup (E' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E' i)] (f : (i : ΞΉ) β†’ E i β†’L[π•œ] E' i) :
                  βˆ€ (a : PiTensorProduct π•œ fun (i : ΞΉ) => E i), ((PiTensorProduct.mapLMultilinear π•œ E E') f) a = (PiTensorProduct.liftAux ((PiTensorProduct.tprodL π•œ).compContinuousLinearMap f).toMultilinearMap) a
                  @[simp]
                  theorem PiTensorProduct.mapLMultilinear_toFun_toFun {ΞΉ : Type uΞΉ} [Fintype ΞΉ] (π•œ : Type uπ•œ) [NontriviallyNormedField π•œ] (E : ΞΉ β†’ Type uE) [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] (E' : ΞΉ β†’ Type u_1) [(i : ΞΉ) β†’ SeminormedAddCommGroup (E' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E' i)] (f : (i : ΞΉ) β†’ E i β†’L[π•œ] E' i) :
                  βˆ€ (a : PiTensorProduct π•œ fun (i : ΞΉ) => E i), ((PiTensorProduct.mapLMultilinear π•œ E E') f) a = (PiTensorProduct.liftAux ((PiTensorProduct.tprodL π•œ).compContinuousLinearMap f).toMultilinearMap) a
                  noncomputable def PiTensorProduct.mapLMultilinear {ΞΉ : Type uΞΉ} [Fintype ΞΉ] (π•œ : Type uπ•œ) [NontriviallyNormedField π•œ] (E : ΞΉ β†’ Type uE) [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] (E' : ΞΉ β†’ Type u_1) [(i : ΞΉ) β†’ SeminormedAddCommGroup (E' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E' i)] :
                  ContinuousMultilinearMap π•œ (fun (i : ΞΉ) => E i β†’L[π•œ] E' i) ((PiTensorProduct π•œ fun (i : ΞΉ) => E i) β†’L[π•œ] PiTensorProduct π•œ fun (i : ΞΉ) => E' i)

                  The tensor of a family of linear maps from Eα΅’ to E'α΅’, as a continuous multilinear map of the family.

                  Equations
                  Instances For
                    theorem PiTensorProduct.mapLMultilinear_opNorm {ΞΉ : Type uΞΉ} [Fintype ΞΉ] {π•œ : Type uπ•œ} [NontriviallyNormedField π•œ] {E : ΞΉ β†’ Type uE} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E i)] {E' : ΞΉ β†’ Type u_1} [(i : ΞΉ) β†’ SeminormedAddCommGroup (E' i)] [(i : ΞΉ) β†’ NormedSpace π•œ (E' i)] :