Documentation

Mathlib.Topology.Algebra.Module.LinearMapPiProd

Continuous linear maps on products and Pi types #

Properties that hold for non-necessarily commutative semirings. #

source
πŸ”Έ coverage
def ContinuousLinearMap.prod {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₃] (f₁ : M₁ β†’L[R] Mβ‚‚) (fβ‚‚ : M₁ β†’L[R] M₃) :
M₁ β†’L[R] Mβ‚‚ Γ— M₃

The Cartesian product of two bounded linear maps, as a bounded linear map.

Equations
    Instances For
      source
      πŸ“ coverage
      @[simp]
      theorem ContinuousLinearMap.coe_prod {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₃] (f₁ : M₁ β†’L[R] Mβ‚‚) (fβ‚‚ : M₁ β†’L[R] M₃) :
      ↑(f₁.prod fβ‚‚) = (↑f₁).prod ↑fβ‚‚
      source
      πŸ“ coverage
      @[simp]
      theorem ContinuousLinearMap.prod_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₃] (f₁ : M₁ β†’L[R] Mβ‚‚) (fβ‚‚ : M₁ β†’L[R] M₃) (x : M₁) :
      (f₁.prod fβ‚‚) x = (f₁ x, fβ‚‚ x)
      source
      πŸ”Έ coverage
      def ContinuousLinearMap.inl (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₁ β†’L[R] M₁ Γ— Mβ‚‚

      The left injection into a product is a continuous linear map.

      Equations
        Instances For
          source
          πŸ”Έ coverage
          def ContinuousLinearMap.inr (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β‚‚ β†’L[R] M₁ Γ— Mβ‚‚

          The right injection into a product is a continuous linear map.

          Equations
            Instances For
              source
              πŸ“ coverage
              @[simp]
              theorem ContinuousLinearMap.inl_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β‚‚] (x : M₁) :
              (inl R M₁ Mβ‚‚) x = (x, 0)
              source
              πŸ“ coverage
              @[simp]
              theorem ContinuousLinearMap.inr_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β‚‚] (x : Mβ‚‚) :
              (inr R M₁ Mβ‚‚) x = (0, x)
              source
              πŸ“ coverage
              @[simp]
              theorem ContinuousLinearMap.coe_inl {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β‚‚] :
              ↑(inl R M₁ Mβ‚‚) = LinearMap.inl R M₁ Mβ‚‚
              source
              πŸ“ coverage
              @[simp]
              theorem ContinuousLinearMap.coe_inr {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β‚‚] :
              ↑(inr R M₁ Mβ‚‚) = LinearMap.inr R M₁ Mβ‚‚
              source
              πŸ“ coverage
              theorem ContinuousLinearMap.comp_inl_add_comp_inr {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₃] (L : M₁ Γ— Mβ‚‚ β†’L[R] M₃) (v : M₁ Γ— Mβ‚‚) :
              (L.comp (inl R M₁ Mβ‚‚)) v.1 + (L.comp (inr R M₁ Mβ‚‚)) v.2 = L v
              source
              πŸ“ coverage
              theorem ContinuousLinearMap.ker_prod {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₃] (f : M₁ β†’L[R] Mβ‚‚) (g : M₁ β†’L[R] M₃) :
              (↑(f.prod g)).ker = (↑f).ker βŠ“ (↑g).ker
              source
              πŸ”Έ coverage
              def ContinuousLinearMap.fst (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₁

              Prod.fst as a ContinuousLinearMap.

              Equations
                Instances For
                  source
                  πŸ”Έ coverage
                  def ContinuousLinearMap.snd (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β‚‚

                  Prod.snd as a ContinuousLinearMap.

                  Equations
                    Instances For
                      source
                      πŸ“ coverage
                      @[simp]
                      theorem ContinuousLinearMap.coe_fst {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β‚‚] :
                      ↑(fst R M₁ Mβ‚‚) = LinearMap.fst R M₁ Mβ‚‚
                      source
                      πŸ“ coverage
                      @[simp]
                      theorem ContinuousLinearMap.coe_fst' {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β‚‚] :
                      ⇑(fst R M₁ Mβ‚‚) = Prod.fst
                      source
                      πŸ“ coverage
                      @[simp]
                      theorem ContinuousLinearMap.coe_snd {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β‚‚] :
                      ↑(snd R M₁ Mβ‚‚) = LinearMap.snd R M₁ Mβ‚‚
                      source
                      πŸ“ coverage
                      @[simp]
                      theorem ContinuousLinearMap.coe_snd' {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β‚‚] :
                      ⇑(snd R M₁ Mβ‚‚) = Prod.snd
                      source
                      πŸ“ coverage
                      @[simp]
                      theorem ContinuousLinearMap.fst_prod_snd {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β‚‚] :
                      (fst R M₁ Mβ‚‚).prod (snd R M₁ Mβ‚‚) = ContinuousLinearMap.id R (M₁ Γ— Mβ‚‚)
                      source
                      πŸ“ coverage
                      @[simp]
                      theorem ContinuousLinearMap.fst_comp_prod {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₃] (f : M₁ β†’L[R] Mβ‚‚) (g : M₁ β†’L[R] M₃) :
                      (fst R Mβ‚‚ M₃).comp (f.prod g) = f
                      source
                      πŸ“ coverage
                      @[simp]
                      theorem ContinuousLinearMap.snd_comp_prod {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₃] (f : M₁ β†’L[R] Mβ‚‚) (g : M₁ β†’L[R] M₃) :
                      (snd R Mβ‚‚ M₃).comp (f.prod g) = g
                      source
                      πŸ“ coverage
                      @[simp]
                      theorem ContinuousLinearMap.fst_comp_inl {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β‚‚] :
                      (fst R M₁ Mβ‚‚).comp (inl R M₁ Mβ‚‚) = ContinuousLinearMap.id R M₁
                      source
                      πŸ“ coverage
                      @[simp]
                      theorem ContinuousLinearMap.fst_comp_inr {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β‚‚] :
                      (fst R M₁ Mβ‚‚).comp (inr R M₁ Mβ‚‚) = 0
                      source
                      πŸ“ coverage
                      @[simp]
                      theorem ContinuousLinearMap.snd_comp_inl {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β‚‚] :
                      (snd R M₁ Mβ‚‚).comp (inl R M₁ Mβ‚‚) = 0
                      source
                      πŸ“ coverage
                      @[simp]
                      theorem ContinuousLinearMap.snd_comp_inr {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β‚‚] :
                      (snd R M₁ Mβ‚‚).comp (inr R M₁ Mβ‚‚) = ContinuousLinearMap.id R Mβ‚‚
                      source
                      πŸ”Έ coverage
                      def ContinuousLinearMap.prodMap {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β‚„] (f₁ : M₁ β†’L[R] Mβ‚‚) (fβ‚‚ : M₃ β†’L[R] Mβ‚„) :
                      M₁ Γ— M₃ β†’L[R] Mβ‚‚ Γ— Mβ‚„

                      Prod.map of two continuous linear maps.

                      Equations
                        Instances For
                          source
                          πŸ“ coverage
                          @[simp]
                          theorem ContinuousLinearMap.coe_prodMap {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β‚„] (f₁ : M₁ β†’L[R] Mβ‚‚) (fβ‚‚ : M₃ β†’L[R] Mβ‚„) :
                          ↑(f₁.prodMap fβ‚‚) = (↑f₁).prodMap ↑fβ‚‚
                          source
                          πŸ“ coverage
                          @[simp]
                          theorem ContinuousLinearMap.coe_prodMap' {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β‚„] (f₁ : M₁ β†’L[R] Mβ‚‚) (fβ‚‚ : M₃ β†’L[R] Mβ‚„) :
                          ⇑(f₁.prodMap fβ‚‚) = Prod.map ⇑f₁ ⇑fβ‚‚
                          source
                          πŸ”Έ coverage
                          def ContinuousLinearMap.pi {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {ΞΉ : Type u_4} {Ο† : ΞΉ β†’ Type u_5} [(i : ΞΉ) β†’ TopologicalSpace (Ο† i)] [(i : ΞΉ) β†’ AddCommMonoid (Ο† i)] [(i : ΞΉ) β†’ Module R (Ο† i)] (f : (i : ΞΉ) β†’ M β†’L[R] Ο† i) :
                          M β†’L[R] (i : ΞΉ) β†’ Ο† i

                          pi construction for continuous linear functions. From a family of continuous linear functions it produces a continuous linear function into a family of topological modules.

                          Equations
                            Instances For
                              source
                              πŸ“ coverage
                              @[simp]
                              theorem ContinuousLinearMap.coe_pi' {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {ΞΉ : Type u_4} {Ο† : ΞΉ β†’ Type u_5} [(i : ΞΉ) β†’ TopologicalSpace (Ο† i)] [(i : ΞΉ) β†’ AddCommMonoid (Ο† i)] [(i : ΞΉ) β†’ Module R (Ο† i)] (f : (i : ΞΉ) β†’ M β†’L[R] Ο† i) :
                              ⇑(pi f) = fun (c : M) (i : ΞΉ) => (f i) c
                              source
                              πŸ“ coverage
                              @[simp]
                              theorem ContinuousLinearMap.coe_pi {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {ΞΉ : Type u_4} {Ο† : ΞΉ β†’ Type u_5} [(i : ΞΉ) β†’ TopologicalSpace (Ο† i)] [(i : ΞΉ) β†’ AddCommMonoid (Ο† i)] [(i : ΞΉ) β†’ Module R (Ο† i)] (f : (i : ΞΉ) β†’ M β†’L[R] Ο† i) :
                              ↑(pi f) = LinearMap.pi fun (i : ΞΉ) => ↑(f i)
                              source
                              πŸ“ coverage
                              theorem ContinuousLinearMap.pi_apply {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {ΞΉ : Type u_4} {Ο† : ΞΉ β†’ Type u_5} [(i : ΞΉ) β†’ TopologicalSpace (Ο† i)] [(i : ΞΉ) β†’ AddCommMonoid (Ο† i)] [(i : ΞΉ) β†’ Module R (Ο† i)] (f : (i : ΞΉ) β†’ M β†’L[R] Ο† i) (c : M) (i : ΞΉ) :
                              (pi f) c i = (f i) c
                              source
                              πŸ“ coverage
                              theorem ContinuousLinearMap.pi_eq_zero {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {ΞΉ : Type u_4} {Ο† : ΞΉ β†’ Type u_5} [(i : ΞΉ) β†’ TopologicalSpace (Ο† i)] [(i : ΞΉ) β†’ AddCommMonoid (Ο† i)] [(i : ΞΉ) β†’ Module R (Ο† i)] (f : (i : ΞΉ) β†’ M β†’L[R] Ο† i) :
                              pi f = 0 ↔ βˆ€ (i : ΞΉ), f i = 0
                              source
                              πŸ“ coverage
                              theorem ContinuousLinearMap.pi_zero {R : Type u_1} [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {ΞΉ : Type u_4} {Ο† : ΞΉ β†’ Type u_5} [(i : ΞΉ) β†’ TopologicalSpace (Ο† i)] [(i : ΞΉ) β†’ AddCommMonoid (Ο† i)] [(i : ΞΉ) β†’ Module R (Ο† i)] :
                              (pi fun (x : ΞΉ) => 0) = 0
                              source
                              πŸ“ coverage
                              theorem ContinuousLinearMap.pi_comp {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β‚‚] {ΞΉ : Type u_4} {Ο† : ΞΉ β†’ Type u_5} [(i : ΞΉ) β†’ TopologicalSpace (Ο† i)] [(i : ΞΉ) β†’ AddCommMonoid (Ο† i)] [(i : ΞΉ) β†’ Module R (Ο† i)] (f : (i : ΞΉ) β†’ M β†’L[R] Ο† i) (g : Mβ‚‚ β†’L[R] M) :
                              (pi f).comp g = pi fun (i : ΞΉ) => (f i).comp g
                              source
                              πŸ”Έ coverage
                              def ContinuousLinearMap.proj {R : Type u_1} [Semiring R] {ΞΉ : Type u_4} {Ο† : ΞΉ β†’ Type u_5} [(i : ΞΉ) β†’ TopologicalSpace (Ο† i)] [(i : ΞΉ) β†’ AddCommMonoid (Ο† i)] [(i : ΞΉ) β†’ Module R (Ο† i)] (i : ΞΉ) :
                              ((i : ΞΉ) β†’ Ο† i) β†’L[R] Ο† i

                              The projections from a family of topological modules are continuous linear maps.

                              Equations
                                Instances For
                                  source
                                  πŸ“ coverage
                                  @[simp]
                                  theorem ContinuousLinearMap.proj_apply {R : Type u_1} [Semiring R] {ΞΉ : Type u_4} {Ο† : ΞΉ β†’ Type u_5} [(i : ΞΉ) β†’ TopologicalSpace (Ο† i)] [(i : ΞΉ) β†’ AddCommMonoid (Ο† i)] [(i : ΞΉ) β†’ Module R (Ο† i)] (i : ΞΉ) (b : (i : ΞΉ) β†’ Ο† i) :
                                  (proj i) b = b i
                                  source
                                  πŸ“ coverage
                                  @[simp]
                                  theorem ContinuousLinearMap.proj_pi {R : Type u_1} [Semiring R] {Mβ‚‚ : Type u_3} [TopologicalSpace Mβ‚‚] [AddCommMonoid Mβ‚‚] [Module R Mβ‚‚] {ΞΉ : Type u_4} {Ο† : ΞΉ β†’ Type u_5} [(i : ΞΉ) β†’ TopologicalSpace (Ο† i)] [(i : ΞΉ) β†’ AddCommMonoid (Ο† i)] [(i : ΞΉ) β†’ Module R (Ο† i)] (f : (i : ΞΉ) β†’ Mβ‚‚ β†’L[R] Ο† i) (i : ΞΉ) :
                                  (proj i).comp (pi f) = f i
                                  source
                                  πŸ“ coverage
                                  @[simp]
                                  theorem ContinuousLinearMap.coe_proj {R : Type u_1} [Semiring R] {ΞΉ : Type u_4} {Ο† : ΞΉ β†’ Type u_5} [(i : ΞΉ) β†’ TopologicalSpace (Ο† i)] [(i : ΞΉ) β†’ AddCommMonoid (Ο† i)] [(i : ΞΉ) β†’ Module R (Ο† i)] (i : ΞΉ) :
                                  ↑(proj i) = LinearMap.proj i
                                  source
                                  πŸ“ coverage
                                  @[simp]
                                  theorem ContinuousLinearMap.pi_proj {R : Type u_1} [Semiring R] {ΞΉ : Type u_4} {Ο† : ΞΉ β†’ Type u_5} [(i : ΞΉ) β†’ TopologicalSpace (Ο† i)] [(i : ΞΉ) β†’ AddCommMonoid (Ο† i)] [(i : ΞΉ) β†’ Module R (Ο† i)] :
                                  pi proj = ContinuousLinearMap.id R ((i : ΞΉ) β†’ Ο† i)
                                  source
                                  πŸ“ coverage
                                  @[simp]
                                  theorem ContinuousLinearMap.pi_proj_comp {R : Type u_1} [Semiring R] {Mβ‚‚ : Type u_3} [TopologicalSpace Mβ‚‚] [AddCommMonoid Mβ‚‚] [Module R Mβ‚‚] {ΞΉ : Type u_4} {Ο† : ΞΉ β†’ Type u_5} [(i : ΞΉ) β†’ TopologicalSpace (Ο† i)] [(i : ΞΉ) β†’ AddCommMonoid (Ο† i)] [(i : ΞΉ) β†’ Module R (Ο† i)] (f : Mβ‚‚ β†’L[R] (i : ΞΉ) β†’ Ο† i) :
                                  (pi fun (x : ΞΉ) => (proj x).comp f) = f
                                  source
                                  πŸ“ coverage
                                  theorem ContinuousLinearMap.iInf_ker_proj {R : Type u_1} [Semiring R] {ΞΉ : Type u_4} {Ο† : ΞΉ β†’ Type u_5} [(i : ΞΉ) β†’ TopologicalSpace (Ο† i)] [(i : ΞΉ) β†’ AddCommMonoid (Ο† i)] [(i : ΞΉ) β†’ Module R (Ο† i)] :
                                  β¨… (i : ΞΉ), (↑(proj i)).ker = βŠ₯
                                  source
                                  πŸ”Έ coverage
                                  def Pi.compRightL (R : Type u_1) [Semiring R] {ΞΉ : Type u_4} (Ο† : ΞΉ β†’ Type u_5) [(i : ΞΉ) β†’ TopologicalSpace (Ο† i)] [(i : ΞΉ) β†’ AddCommMonoid (Ο† i)] [(i : ΞΉ) β†’ Module R (Ο† i)] {Ξ± : Type u_6} (f : Ξ± β†’ ΞΉ) :
                                  ((i : ΞΉ) β†’ Ο† i) β†’L[R] (i : Ξ±) β†’ Ο† (f i)

                                  Given a function f : Ξ± β†’ ΞΉ, it induces a continuous linear function by right composition on product types. For f = Subtype.val, this corresponds to forgetting some set of variables.

                                  Equations
                                    Instances For
                                      source
                                      πŸ“ coverage
                                      @[simp]
                                      theorem Pi.compRightL_apply (R : Type u_1) [Semiring R] {ΞΉ : Type u_4} (Ο† : ΞΉ β†’ Type u_5) [(i : ΞΉ) β†’ TopologicalSpace (Ο† i)] [(i : ΞΉ) β†’ AddCommMonoid (Ο† i)] [(i : ΞΉ) β†’ Module R (Ο† i)] {Ξ± : Type u_6} (f : Ξ± β†’ ΞΉ) (v : (i : ΞΉ) β†’ Ο† i) (i : Ξ±) :
                                      (compRightL R Ο† f) v i = v (f i)
                                      source
                                      πŸ”Έ coverage
                                      def ContinuousLinearMap.single (R : Type u_1) [Semiring R] {ΞΉ : Type u_4} (Ο† : ΞΉ β†’ Type u_5) [(i : ΞΉ) β†’ TopologicalSpace (Ο† i)] [(i : ΞΉ) β†’ AddCommMonoid (Ο† i)] [(i : ΞΉ) β†’ Module R (Ο† i)] [DecidableEq ΞΉ] (i : ΞΉ) :
                                      Ο† i β†’L[R] (i : ΞΉ) β†’ Ο† i

                                      Pi.single as a bundled continuous linear map.

                                      Equations
                                        Instances For
                                          source
                                          πŸ“ coverage
                                          @[simp]
                                          theorem ContinuousLinearMap.single_apply (R : Type u_1) [Semiring R] {ΞΉ : Type u_4} (Ο† : ΞΉ β†’ Type u_5) [(i : ΞΉ) β†’ TopologicalSpace (Ο† i)] [(i : ΞΉ) β†’ AddCommMonoid (Ο† i)] [(i : ΞΉ) β†’ Module R (Ο† i)] [DecidableEq ΞΉ] (i : ΞΉ) :
                                          ⇑(single R Ο† i) = Pi.single i
                                          source
                                          πŸ“ coverage
                                          theorem ContinuousLinearMap.sum_comp_single (R : Type u_1) [Semiring R] {M : Type u_2} [TopologicalSpace M] [AddCommMonoid M] [Module R M] {ΞΉ : Type u_4} (Ο† : ΞΉ β†’ Type u_5) [(i : ΞΉ) β†’ TopologicalSpace (Ο† i)] [(i : ΞΉ) β†’ AddCommMonoid (Ο† i)] [(i : ΞΉ) β†’ Module R (Ο† i)] [Fintype ΞΉ] [DecidableEq ΞΉ] (L : ((i : ΞΉ) β†’ Ο† i) β†’L[R] M) (v : (i : ΞΉ) β†’ Ο† i) :
                                          βˆ‘ i : ΞΉ, (L.comp (single R Ο† i)) (v i) = L v
                                          source
                                          πŸ“ coverage
                                          theorem ContinuousLinearMap.range_prod_eq {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {Mβ‚‚ : Type u_3} [TopologicalSpace Mβ‚‚] [AddCommGroup Mβ‚‚] [Module R Mβ‚‚] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommGroup M₃] [Module R M₃] {f : M β†’L[R] Mβ‚‚} {g : M β†’L[R] M₃} (h : (↑f).ker βŠ” (↑g).ker = ⊀) :
                                          (↑(f.prod g)).range = (↑f).range.prod (↑g).range
                                          source
                                          πŸ“ coverage
                                          theorem ContinuousLinearMap.ker_prod_ker_le_ker_coprod {R : Type u_1} [Ring R] {M : Type u_2} [TopologicalSpace M] [AddCommGroup M] [Module R M] {Mβ‚‚ : Type u_3} [TopologicalSpace Mβ‚‚] [AddCommGroup Mβ‚‚] [Module R Mβ‚‚] {M₃ : Type u_4} [TopologicalSpace M₃] [AddCommGroup M₃] [Module R M₃] (f : M β†’L[R] M₃) (g : Mβ‚‚ β†’L[R] M₃) :
                                          (↑f).ker.prod (↑g).ker ≀ ((↑f).coprod ↑g).ker
                                          source
                                          πŸ”Έ coverage
                                          def ContinuousLinearMap.prodEquiv {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 β†’L[R] Mβ‚‚) Γ— (M β†’L[R] M₃) ≃ (M β†’L[R] Mβ‚‚ Γ— M₃)

                                          ContinuousLinearMap.prod as an Equiv.

                                          Equations
                                            Instances For
                                              source
                                              πŸ“ coverage
                                              @[simp]
                                              theorem ContinuousLinearMap.prodEquiv_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₃] (f : (M β†’L[R] Mβ‚‚) Γ— (M β†’L[R] M₃)) :
                                              prodEquiv f = f.1.prod f.2
                                              source
                                              πŸ“ coverage
                                              theorem ContinuousLinearMap.prod_ext_iff {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₃] {f g : M Γ— Mβ‚‚ β†’L[R] M₃} :
                                              f = g ↔ f.comp (inl R M Mβ‚‚) = g.comp (inl R M Mβ‚‚) ∧ f.comp (inr R M Mβ‚‚) = g.comp (inr R M Mβ‚‚)
                                              source
                                              theorem ContinuousLinearMap.prod_ext {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₃] {f g : M Γ— Mβ‚‚ β†’L[R] M₃} (hl : f.comp (inl R M Mβ‚‚) = g.comp (inl R M Mβ‚‚)) (hr : f.comp (inr R M Mβ‚‚) = g.comp (inr R M Mβ‚‚)) :
                                              f = g
                                              source
                                              πŸ”Έ coverage
                                              def ContinuousLinearMap.prodβ‚— {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₃] (S : Type u_5) [Semiring S] [Module S Mβ‚‚] [ContinuousAdd Mβ‚‚] [SMulCommClass R S Mβ‚‚] [ContinuousConstSMul S Mβ‚‚] [Module S M₃] [ContinuousAdd M₃] [SMulCommClass R S M₃] [ContinuousConstSMul S M₃] :
                                              ((M β†’L[R] Mβ‚‚) Γ— (M β†’L[R] M₃)) ≃ₗ[S] M β†’L[R] Mβ‚‚ Γ— M₃

                                              ContinuousLinearMap.prod as a LinearEquiv.

                                              See ContinuousLinearMap.prodL for the ContinuousLinearEquiv version.

                                              Equations
                                                Instances For
                                                  source
                                                  πŸ“ coverage
                                                  @[simp]
                                                  theorem ContinuousLinearMap.prodβ‚—_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₃] (S : Type u_5) [Semiring S] [Module S Mβ‚‚] [ContinuousAdd Mβ‚‚] [SMulCommClass R S Mβ‚‚] [ContinuousConstSMul S Mβ‚‚] [Module S M₃] [ContinuousAdd M₃] [SMulCommClass R S M₃] [ContinuousConstSMul S M₃] (a✝ : (M β†’L[R] Mβ‚‚) Γ— (M β†’L[R] M₃)) :
                                                  (prodβ‚— S) a✝ = prodEquiv.toFun a✝
                                                  source
                                                  πŸ”Έ coverage
                                                  def ContinuousLinearMap.coprod {R : Type u_1} {M : Type u_3} {M₁ : Type u_5} {Mβ‚‚ : Type u_6} [Semiring R] [TopologicalSpace M] [TopologicalSpace M₁] [TopologicalSpace Mβ‚‚] [AddCommMonoid M] [Module R M] [ContinuousAdd M] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid Mβ‚‚] [Module R Mβ‚‚] (f₁ : M₁ β†’L[R] M) (fβ‚‚ : Mβ‚‚ β†’L[R] M) :
                                                  M₁ Γ— Mβ‚‚ β†’L[R] M

                                                  The continuous linear map given by (x, y) ↦ f₁ x + fβ‚‚ y.

                                                  Equations
                                                    Instances For
                                                      source
                                                      πŸ“ coverage
                                                      @[simp]
                                                      theorem ContinuousLinearMap.coe_coprod {R : Type u_1} {M : Type u_3} {M₁ : Type u_5} {Mβ‚‚ : Type u_6} [Semiring R] [TopologicalSpace M] [TopologicalSpace M₁] [TopologicalSpace Mβ‚‚] [AddCommMonoid M] [Module R M] [ContinuousAdd M] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid Mβ‚‚] [Module R Mβ‚‚] (f₁ : M₁ β†’L[R] M) (fβ‚‚ : Mβ‚‚ β†’L[R] M) :
                                                      ↑(f₁.coprod fβ‚‚) = (↑f₁).coprod ↑fβ‚‚
                                                      source
                                                      πŸ“ coverage
                                                      @[simp]
                                                      theorem ContinuousLinearMap.coprod_apply {R : Type u_1} {M : Type u_3} {M₁ : Type u_5} {Mβ‚‚ : Type u_6} [Semiring R] [TopologicalSpace M] [TopologicalSpace M₁] [TopologicalSpace Mβ‚‚] [AddCommMonoid M] [Module R M] [ContinuousAdd M] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid Mβ‚‚] [Module R Mβ‚‚] (f₁ : M₁ β†’L[R] M) (fβ‚‚ : Mβ‚‚ β†’L[R] M) (a : M₁ Γ— Mβ‚‚) :
                                                      (f₁.coprod fβ‚‚) a = f₁ a.1 + fβ‚‚ a.2
                                                      source
                                                      πŸ“ coverage
                                                      @[simp]
                                                      theorem ContinuousLinearMap.coprod_add {R : Type u_1} {M : Type u_3} {M₁ : Type u_5} {Mβ‚‚ : Type u_6} [Semiring R] [TopologicalSpace M] [TopologicalSpace M₁] [TopologicalSpace Mβ‚‚] [AddCommMonoid M] [Module R M] [ContinuousAdd M] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid Mβ‚‚] [Module R Mβ‚‚] (f₁ g₁ : M₁ β†’L[R] M) (fβ‚‚ gβ‚‚ : Mβ‚‚ β†’L[R] M) :
                                                      (f₁ + g₁).coprod (fβ‚‚ + gβ‚‚) = f₁.coprod fβ‚‚ + g₁.coprod gβ‚‚
                                                      source
                                                      πŸ“ coverage
                                                      theorem ContinuousLinearMap.range_coprod {R : Type u_1} {M : Type u_3} {M₁ : Type u_5} {Mβ‚‚ : Type u_6} [Semiring R] [TopologicalSpace M] [TopologicalSpace M₁] [TopologicalSpace Mβ‚‚] [AddCommMonoid M] [Module R M] [ContinuousAdd M] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid Mβ‚‚] [Module R Mβ‚‚] (f₁ : M₁ β†’L[R] M) (fβ‚‚ : Mβ‚‚ β†’L[R] M) :
                                                      (↑(f₁.coprod fβ‚‚)).range = (↑f₁).range βŠ” (↑fβ‚‚).range
                                                      source
                                                      πŸ“ coverage
                                                      theorem ContinuousLinearMap.comp_fst_add_comp_snd {R : Type u_1} {M : Type u_3} {M₁ : Type u_5} {Mβ‚‚ : Type u_6} [Semiring R] [TopologicalSpace M] [TopologicalSpace M₁] [TopologicalSpace Mβ‚‚] [AddCommMonoid M] [Module R M] [ContinuousAdd M] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid Mβ‚‚] [Module R Mβ‚‚] (f₁ : M₁ β†’L[R] M) (fβ‚‚ : Mβ‚‚ β†’L[R] M) :
                                                      f₁.comp (fst R M₁ Mβ‚‚) + fβ‚‚.comp (snd R M₁ Mβ‚‚) = f₁.coprod fβ‚‚
                                                      source
                                                      πŸ“ coverage
                                                      theorem ContinuousLinearMap.comp_coprod {R : Type u_1} {M : Type u_3} {N : Type u_4} {M₁ : Type u_5} {Mβ‚‚ : Type u_6} [Semiring R] [TopologicalSpace M] [TopologicalSpace N] [TopologicalSpace M₁] [TopologicalSpace Mβ‚‚] [AddCommMonoid M] [Module R M] [ContinuousAdd M] [AddCommMonoid N] [Module R N] [ContinuousAdd N] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid Mβ‚‚] [Module R Mβ‚‚] (f : M β†’L[R] N) (g₁ : M₁ β†’L[R] M) (gβ‚‚ : Mβ‚‚ β†’L[R] M) :
                                                      f.comp (g₁.coprod gβ‚‚) = (f.comp g₁).coprod (f.comp gβ‚‚)
                                                      source
                                                      πŸ“ coverage
                                                      @[simp]
                                                      theorem ContinuousLinearMap.coprod_comp_inl {R : Type u_1} {M : Type u_3} {M₁ : Type u_5} {Mβ‚‚ : Type u_6} [Semiring R] [TopologicalSpace M] [TopologicalSpace M₁] [TopologicalSpace Mβ‚‚] [AddCommMonoid M] [Module R M] [ContinuousAdd M] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid Mβ‚‚] [Module R Mβ‚‚] (f₁ : M₁ β†’L[R] M) (fβ‚‚ : Mβ‚‚ β†’L[R] M) :
                                                      (f₁.coprod fβ‚‚).comp (inl R M₁ Mβ‚‚) = f₁
                                                      source
                                                      πŸ“ coverage
                                                      @[simp]
                                                      theorem ContinuousLinearMap.coprod_comp_inr {R : Type u_1} {M : Type u_3} {M₁ : Type u_5} {Mβ‚‚ : Type u_6} [Semiring R] [TopologicalSpace M] [TopologicalSpace M₁] [TopologicalSpace Mβ‚‚] [AddCommMonoid M] [Module R M] [ContinuousAdd M] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid Mβ‚‚] [Module R Mβ‚‚] (f₁ : M₁ β†’L[R] M) (fβ‚‚ : Mβ‚‚ β†’L[R] M) :
                                                      (f₁.coprod fβ‚‚).comp (inr R M₁ Mβ‚‚) = fβ‚‚
                                                      source
                                                      πŸ“ coverage
                                                      @[simp]
                                                      theorem ContinuousLinearMap.coprod_inl_inr {R : Type u_1} {M : Type u_3} {N : Type u_4} [Semiring R] [TopologicalSpace M] [TopologicalSpace N] [AddCommMonoid M] [Module R M] [ContinuousAdd M] [AddCommMonoid N] [Module R N] [ContinuousAdd N] :
                                                      (inl R M N).coprod (inr R M N) = ContinuousLinearMap.id R (M Γ— N)
                                                      source
                                                      πŸ“ coverage
                                                      @[simp]
                                                      theorem ContinuousLinearMap.coprod_comp_inl_inr {R : Type u_1} {M : Type u_3} {M₁ : Type u_5} {Mβ‚‚ : Type u_6} [Semiring R] [TopologicalSpace M] [TopologicalSpace M₁] [TopologicalSpace Mβ‚‚] [AddCommMonoid M] [Module R M] [ContinuousAdd M] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid Mβ‚‚] [Module R Mβ‚‚] [ContinuousAdd M₁] [ContinuousAdd Mβ‚‚] (f : M Γ— M₁ β†’L[R] Mβ‚‚) :
                                                      (f.comp (inl R M M₁)).coprod (f.comp (inr R M M₁)) = f
                                                      source
                                                      πŸ”Έ coverage
                                                      def ContinuousLinearMap.coprodEquiv {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₁ : Type u_5} {Mβ‚‚ : Type u_6} [Semiring R] [TopologicalSpace M] [TopologicalSpace M₁] [TopologicalSpace Mβ‚‚] [AddCommMonoid M] [Module R M] [ContinuousAdd M] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid Mβ‚‚] [Module R Mβ‚‚] [ContinuousAdd M₁] [ContinuousAdd Mβ‚‚] [Semiring S] [Module S M] [ContinuousConstSMul S M] [SMulCommClass R S M] :
                                                      ((M₁ β†’L[R] M) Γ— (Mβ‚‚ β†’L[R] M)) ≃ₗ[S] M₁ Γ— Mβ‚‚ β†’L[R] M

                                                      Taking the product of two maps with the same codomain is equivalent to taking the product of their domains. See note [bundled maps over different rings] for why separate R and S semirings are used.

                                                      See ContinuousLinearMap.coprodEquivL for the ContinuousLinearEquiv version.

                                                      Equations
                                                        Instances For
                                                          source
                                                          πŸ“ coverage
                                                          @[simp]
                                                          theorem ContinuousLinearMap.coprodEquiv_apply {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₁ : Type u_5} {Mβ‚‚ : Type u_6} [Semiring R] [TopologicalSpace M] [TopologicalSpace M₁] [TopologicalSpace Mβ‚‚] [AddCommMonoid M] [Module R M] [ContinuousAdd M] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid Mβ‚‚] [Module R Mβ‚‚] [ContinuousAdd M₁] [ContinuousAdd Mβ‚‚] [Semiring S] [Module S M] [ContinuousConstSMul S M] [SMulCommClass R S M] (f : (M₁ β†’L[R] M) Γ— (Mβ‚‚ β†’L[R] M)) :
                                                          coprodEquiv f = f.1.coprod f.2
                                                          source
                                                          πŸ“ coverage
                                                          @[simp]
                                                          theorem ContinuousLinearMap.coprodEquiv_symm_apply {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₁ : Type u_5} {Mβ‚‚ : Type u_6} [Semiring R] [TopologicalSpace M] [TopologicalSpace M₁] [TopologicalSpace Mβ‚‚] [AddCommMonoid M] [Module R M] [ContinuousAdd M] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid Mβ‚‚] [Module R Mβ‚‚] [ContinuousAdd M₁] [ContinuousAdd Mβ‚‚] [Semiring S] [Module S M] [ContinuousConstSMul S M] [SMulCommClass R S M] (f : M₁ Γ— Mβ‚‚ β†’L[R] M) :
                                                          coprodEquiv.symm f = (f.comp (inl R M₁ Mβ‚‚), f.comp (inr R M₁ Mβ‚‚))
                                                          source
                                                          πŸ“ coverage
                                                          theorem ContinuousLinearMap.ker_coprod_of_disjoint_range {R : Type u_1} {M : Type u_3} {M₁ : Type u_5} {Mβ‚‚ : Type u_6} [Semiring R] [TopologicalSpace M] [TopologicalSpace M₁] [TopologicalSpace Mβ‚‚] [AddCommGroup M] [Module R M] [ContinuousAdd M] [AddCommMonoid M₁] [Module R M₁] [AddCommGroup Mβ‚‚] [Module R Mβ‚‚] {f₁ : M₁ β†’L[R] M} {fβ‚‚ : Mβ‚‚ β†’L[R] M} (hf : Disjoint (↑f₁).range (↑fβ‚‚).range) :
                                                          (↑(f₁.coprod fβ‚‚)).ker = (↑f₁).ker.prod (↑fβ‚‚).ker