Documentation

Mathlib.Topology.Algebra.Module.LinearMapPiProd

Continuous linear maps on products and Pi types #

Properties that hold for non-necessarily commutative semirings. #

source
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
  • f₁.prod f₂ = { toLinearMap := (↑f₁).prod ↑f₂, cont := ⋯ }
source
@[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
@[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
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
source
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
source
@[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
@[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
@[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
@[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
@[simp]
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₃) :
LinearMap.ker (f.prod g) = LinearMap.ker f ⊓ LinearMap.ker g
source
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
source
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
source
@[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
@[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
@[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
@[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
@[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₂) = id R (M₁ × M₂)
source
@[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
@[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
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
source
@[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
@[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
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
source
@[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
@[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
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
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
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
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
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
source
@[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
@[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
@[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
@[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 = id R ((i : ι) → φ i)
source
@[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
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 : ι), LinearMap.ker (proj i) = ⊥
source
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
  • Pi.compRightL R φ f = { toFun := fun (v : (i : ι) → φ i) (i : α) => v (f i), map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
source
@[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
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
source
@[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
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 : LinearMap.ker f ⊔ LinearMap.ker g = ⊤) :
LinearMap.range (f.prod g) = (LinearMap.range f).prod (LinearMap.range g)
source
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₃) :
(LinearMap.ker f).prod (LinearMap.ker g) ≤ LinearMap.ker ((↑f).coprod ↑g)
source
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
  • One or more equations did not get rendered due to their size.
source
@[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
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
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.

Equations
source
@[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
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
  • f₁.coprod f₂ = { toLinearMap := (↑f₁).coprod ↑f₂, cont := ⋯ }
source
@[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
@[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
@[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
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) :
LinearMap.range (f₁.coprod f₂) = LinearMap.range f₁ ⊔ LinearMap.range f₂
source
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
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
@[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
@[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
@[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) = id R (M × N)
source
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.

TODO: Upgrade this to a ContinuousLinearEquiv. This should be true for any topological vector space over a normed field thanks to ContinuousLinearMap.precomp and ContinuousLinearMap.postcomp.

Equations
  • One or more equations did not get rendered due to their size.
source
@[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
@[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
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 (LinearMap.range f₁) (LinearMap.range f₂)) :
LinearMap.ker (f₁.coprod f₂) = (LinearMap.ker f₁).prod (LinearMap.ker f₂)