Documentation

Mathlib.Topology.Algebra.Module.Equiv.Prod

Continuous linear equivalences on products of topological modules #

Main Definitions #

source
def ContinuousLinearEquiv.prodCongr {R : Type u_1} [Semiring R] {M₁ : Type u_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] {M₄ : Type u_5} [TopologicalSpace M₄] [AddCommMonoid M₄] [Module R M₄] (e : M₁ ≃L[R] M₂) (e' : M₃ ≃L[R] M₄) :
(M₁ × M₃) ≃L[R] M₂ × M₄

Product of two continuous linear equivalences. The map comes from Equiv.prodCongr.

Instances For
    source
    @[simp]
    theorem ContinuousLinearEquiv.prodCongr_apply {R : Type u_1} [Semiring R] {M₁ : Type u_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] {M₄ : Type u_5} [TopologicalSpace M₄] [AddCommMonoid M₄] [Module R M₄] (e : M₁ ≃L[R] M₂) (e' : M₃ ≃L[R] M₄) (x : M₁ × M₃) :
    (e.prodCongr e') x = (e x.1, e' x.2)
    source
    @[simp]
    theorem ContinuousLinearEquiv.coe_prodCongr {R : Type u_1} [Semiring R] {M₁ : Type u_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] {M₄ : Type u_5} [TopologicalSpace M₄] [AddCommMonoid M₄] [Module R M₄] (e : M₁ ≃L[R] M₂) (e' : M₃ ≃L[R] M₄) :
    ↑(e.prodCongr e') = (↑e).prodMap ↑e'
    source
    @[simp]
    theorem ContinuousLinearEquiv.prodCongr_symm {R : Type u_1} [Semiring R] {M₁ : Type u_2} [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] {M₂ : Type u_3} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] {M₄ : Type u_5} [TopologicalSpace M₄] [AddCommMonoid M₄] [Module R M₄] (e : M₁ ≃L[R] M₂) (e' : M₃ ≃L[R] M₄) :
    (e.prodCongr e').symm = e.symm.prodCongr e'.symm
    source
    def ContinuousLinearEquiv.prodComm (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] :
    (M₁ × M₂) ≃L[R] M₂ × M₁

    Product of topological modules is commutative up to continuous linear isomorphism.

    Instances For
      source
      @[simp]
      theorem ContinuousLinearEquiv.prodComm_toLinearEquiv (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] :
      ↑(prodComm R M₁ M₂) = LinearEquiv.prodComm R M₁ M₂
      source
      @[simp]
      theorem ContinuousLinearEquiv.prodComm_apply (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] (a✝ : M₁ × M₂) :
      (prodComm R M₁ M₂) a✝ = a✝.swap
      source
      @[simp]
      theorem ContinuousLinearEquiv.prodComm_symm (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] :
      (prodComm R M₁ M₂).symm = prodComm R M₂ M₁
      source
      @[simp]
      theorem ContinuousLinearEquiv.prodComm_trans_prodComm (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] :
      (prodComm R M₁ M₂).trans (prodComm R M₂ M₁) = ContinuousLinearEquiv.refl R (M₁ × M₂)
      source
      theorem ContinuousLinearMap.coprod_comp_prodComm (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] [ContinuousAdd M₃] (f : M₁ →L[R] M₃) (g : M₂ →L[R] M₃) :
      f.coprod g ∘SL ↑(ContinuousLinearEquiv.prodComm R M₂ M₁) = g.coprod f

      Composition of a map on a product with the exchange of the product factors

      source
      def ContinuousLinearEquiv.prodAssoc (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] (M₃ : Type u_4) [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] :
      ((M₁ × M₂) × M₃) ≃L[R] M₁ × M₂ × M₃

      The product of topological modules is associative up to continuous linear isomorphism. This is LinearEquiv.prodAssoc prodAssoc as a continuous linear equivalence.

      Instances For
        source
        @[simp]
        theorem ContinuousLinearEquiv.prodAssoc_toLinearEquiv (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] (M₃ : Type u_4) [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] :
        ↑(prodAssoc R M₁ M₂ M₃) = LinearEquiv.prodAssoc R M₁ M₂ M₃
        source
        @[simp]
        theorem ContinuousLinearEquiv.coe_prodAssoc (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] (M₃ : Type u_4) [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] :
        ⇑(prodAssoc R M₁ M₂ M₃) = ⇑(Equiv.prodAssoc M₁ M₂ M₃)
        source
        @[simp]
        theorem ContinuousLinearEquiv.prodAssoc_apply (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] (M₃ : Type u_4) [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] (p₁ : M₁) (p₂ : M₂) (p₃ : M₃) :
        (prodAssoc R M₁ M₂ M₃) ((p₁, p₂), p₃) = (p₁, p₂, p₃)
        source
        @[simp]
        theorem ContinuousLinearEquiv.prodAssoc_symm_apply (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] (M₃ : Type u_4) [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] (p₁ : M₁) (p₂ : M₂) (p₃ : M₃) :
        (prodAssoc R M₁ M₂ M₃).symm (p₁, p₂, p₃) = ((p₁, p₂), p₃)
        source
        def ContinuousLinearEquiv.prodProdProdComm (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] (M₃ : Type u_4) [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] (M₄ : Type u_5) [TopologicalSpace M₄] [AddCommMonoid M₄] [Module R M₄] :
        ((M₁ × M₂) × M₃ × M₄) ≃L[R] (M₁ × M₃) × M₂ × M₄

        The product of topological modules is four-way commutative up to continuous linear isomorphism. This is LinearEquiv.prodProdProdComm prodAssoc as a continuous linear equivalence.

        Instances For
          source
          @[simp]
          theorem ContinuousLinearEquiv.prodProdProdComm_symm (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] (M₃ : Type u_4) [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] (M₄ : Type u_5) [TopologicalSpace M₄] [AddCommMonoid M₄] [Module R M₄] :
          (prodProdProdComm R M₁ M₂ M₃ M₄).symm = prodProdProdComm R M₁ M₃ M₂ M₄
          source
          @[simp]
          theorem ContinuousLinearEquiv.prodProdProdComm_toLinearEquiv (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] (M₃ : Type u_4) [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] (M₄ : Type u_5) [TopologicalSpace M₄] [AddCommMonoid M₄] [Module R M₄] :
          ↑(prodProdProdComm R M₁ M₂ M₃ M₄) = LinearEquiv.prodProdProdComm R M₁ M₂ M₃ M₄
          source
          @[simp]
          theorem ContinuousLinearEquiv.coe_prodProdProdComm (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] (M₃ : Type u_4) [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] (M₄ : Type u_5) [TopologicalSpace M₄] [AddCommMonoid M₄] [Module R M₄] :
          ⇑(prodProdProdComm R M₁ M₂ M₃ M₄) = ⇑(Equiv.prodProdProdComm M₁ M₂ M₃ M₄)
          source
          @[simp]
          theorem ContinuousLinearEquiv.prodProdProdComm_apply (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] (M₃ : Type u_4) [TopologicalSpace M₃] [AddCommMonoid M₃] [Module R M₃] (M₄ : Type u_5) [TopologicalSpace M₄] [AddCommMonoid M₄] [Module R M₄] (p₁ : M₁) (p₂ : M₂) (p₃ : M₃) (p₄ : M₄) :
          (prodProdProdComm R M₁ M₂ M₃ M₄) ((p₁, p₂), p₃, p₄) = ((p₁, p₃), p₂, p₄)
          source
          def ContinuousLinearEquiv.prodUnique (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] [Unique M₂] :
          (M₁ × M₂) ≃L[R] M₁

          The natural equivalence M × N ≃L[R] M for any Unique type N. This is Equiv.prodUnique as a continuous linear equivalence.

          Instances For
            source
            @[simp]
            theorem ContinuousLinearEquiv.coe_prodUnique (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] [Unique M₂] :
            (↑(prodUnique R M₁ M₂)).toEquiv = Equiv.prodUnique M₁ M₂
            source
            @[simp]
            theorem ContinuousLinearEquiv.prodUnique_apply (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] [Unique M₂] (x : M₁ × M₂) :
            (prodUnique R M₁ M₂) x = x.1
            source
            @[simp]
            theorem ContinuousLinearEquiv.prodUnique_symm_apply (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] [Unique M₂] (x : M₁) :
            (prodUnique R M₁ M₂).symm x = (x, default)
            source
            def ContinuousLinearEquiv.uniqueProd (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] [Unique M₂] :
            (M₂ × M₁) ≃L[R] M₁

            The natural equivalence N × M ≃L[R] M for any Unique type N. This is Equiv.uniqueProd as a continuous linear equivalence.

            Instances For
              source
              @[simp]
              theorem ContinuousLinearEquiv.coe_uniqueProd (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] [Unique M₂] :
              (↑(uniqueProd R M₁ M₂)).toEquiv = Equiv.uniqueProd M₁ M₂
              source
              @[simp]
              theorem ContinuousLinearEquiv.uniqueProd_apply (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] [Unique M₂] (x : M₂ × M₁) :
              (uniqueProd R M₁ M₂) x = x.2
              source
              @[simp]
              theorem ContinuousLinearEquiv.uniqueProd_symm_apply (R : Type u_1) [Semiring R] (M₁ : Type u_2) [TopologicalSpace M₁] [AddCommMonoid M₁] [Module R M₁] (M₂ : Type u_3) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M₂] [Unique M₂] (x : M₁) :
              (uniqueProd R M₁ M₂).symm x = (default, x)