Continuous linear maps on products and Pi types

Properties that hold for non-necessarily commutative semirings.

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 := ⋯ }

@[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₂

@[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)

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

• ContinuousLinearMap.inl R M₁ M₂ = (ContinuousLinearMap.id R M₁).prod 0

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

• ContinuousLinearMap.inr R M₁ M₂ = ContinuousLinearMap.prod 0 (ContinuousLinearMap.id R M₂)

@[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₁) : (ContinuousLinearMap.inl R M₁ M₂) x = (x, 0)

@[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₂) : (ContinuousLinearMap.inr R M₁ M₂) x = (0, x)

@[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₂] : ↑(ContinuousLinearMap.inl R M₁ M₂) = LinearMap.inl R M₁ M₂

@[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₂] : ↑(ContinuousLinearMap.inr R M₁ M₂) = LinearMap.inr R M₁ M₂

@[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

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

• ContinuousLinearMap.fst R M₁ M₂ = { toLinearMap := LinearMap.fst R M₁ M₂, cont := ⋯ }

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

• ContinuousLinearMap.snd R M₁ M₂ = { toLinearMap := LinearMap.snd R M₁ M₂, cont := ⋯ }

@[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₂] : ↑(ContinuousLinearMap.fst R M₁ M₂) = LinearMap.fst R M₁ M₂

@[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₂] : ⇑(ContinuousLinearMap.fst R M₁ M₂) = Prod.fst

@[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₂] : ↑(ContinuousLinearMap.snd R M₁ M₂) = LinearMap.snd R M₁ M₂

@[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₂] : ⇑(ContinuousLinearMap.snd R M₁ M₂) = Prod.snd

@[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₂] : (ContinuousLinearMap.fst R M₁ M₂).prod (ContinuousLinearMap.snd R M₁ M₂) = ContinuousLinearMap.id R (M₁ × M₂)

@[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₃) : (ContinuousLinearMap.fst R M₂ M₃).comp (f.prod g) = f

@[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₃) : (ContinuousLinearMap.snd R M₂ M₃).comp (f.prod g) = g

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

• f₁.prodMap f₂ = (f₁.comp (ContinuousLinearMap.fst R M₁ M₃)).prod (f₂.comp (ContinuousLinearMap.snd R M₁ M₃))

@[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₂

@[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₂

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

• ContinuousLinearMap.pi f = { toLinearMap := LinearMap.pi fun (i : ι) => ↑(f i), cont := ⋯ }

@[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) : ⇑(ContinuousLinearMap.pi f) = fun (c : M) (i : ι) => (f i) c

@[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) : ↑(ContinuousLinearMap.pi f) = LinearMap.pi fun (i : ι) => ↑(f i)

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 : ι) : (ContinuousLinearMap.pi f) c i = (f i) c

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) : ContinuousLinearMap.pi f = 0 ↔ ∀ (i : ι), f i = 0

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)] : (ContinuousLinearMap.pi fun (x : ι) => 0) = 0

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) : (ContinuousLinearMap.pi f).comp g = ContinuousLinearMap.pi fun (i : ι) => (f i).comp g

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

• ContinuousLinearMap.proj i = { toLinearMap := LinearMap.proj i, cont := ⋯ }

@[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) : (ContinuousLinearMap.proj i) b = b i

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 : ι) : (ContinuousLinearMap.proj i).comp (ContinuousLinearMap.pi f) = f i

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 (ContinuousLinearMap.proj i) = ⊥

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 := ⋯ }

@[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 : α) : (Pi.compRightL R φ f) v i = v (f i)

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)

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)

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.

@[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₃)) : ContinuousLinearMap.prodEquiv f = f.1.prod f.2

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 (ContinuousLinearMap.inl R M M₂) = g.comp (ContinuousLinearMap.inl R M M₂) ∧ f.comp (ContinuousLinearMap.inr R M M₂) = g.comp (ContinuousLinearMap.inr R M M₂)

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 (ContinuousLinearMap.inl R M M₂) = g.comp (ContinuousLinearMap.inl R M M₂)) (hr : f.comp (ContinuousLinearMap.inr R M M₂) = g.comp (ContinuousLinearMap.inr R M M₂)) : f = g

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

• ContinuousLinearMap.prodₗ S = { toFun := ContinuousLinearMap.prodEquiv.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := ContinuousLinearMap.prodEquiv.invFun, left_inv := ⋯, right_inv := ⋯ }

@[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₃)) : (ContinuousLinearMap.prodₗ S) a✝ = ContinuousLinearMap.prodEquiv.toFun a✝

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 := ⋯ }

@[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₂

@[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

@[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₂

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₂

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 (ContinuousLinearMap.fst R M₁ M₂) + f₂.comp (ContinuousLinearMap.snd R M₁ M₂) = f₁.coprod f₂

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₂)

@[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 (ContinuousLinearMap.inl R M₁ M₂) = f₁

@[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 (ContinuousLinearMap.inr R M₁ M₂) = f₂

@[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] : (ContinuousLinearMap.inl R M N).coprod (ContinuousLinearMap.inr R M N) = ContinuousLinearMap.id R (M × N)

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.

@[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)) : ContinuousLinearMap.coprodEquiv f = f.1.coprod f.2

@[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) : ContinuousLinearMap.coprodEquiv.symm f = (f.comp (ContinuousLinearMap.inl R M₁ M₂), f.comp (ContinuousLinearMap.inr R M₁ M₂))

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₂)