Continuous linear maps on products and Pi types #

In this file, we collect various constructions relating continuous linear maps with (binary or arbitrary) products.

Main definitions #

Binary products (viewed as categorical products):

ContinuousLinearMap.fst R M₁ M₂ : M₁ × M₂ →L[R] M₁ and ContinuousLinearMap.snd R M₁ M₂ : M₁ × M₂ →L[R] M₂ are the two projections, given respectively by fst (x, y) = x and snd (x, y) = y. These are the continuous versions of LinearMap.fst and LinearMap.snd.
ContinuousLinearMap.prod f₁ f₂ is the continuous linear map M →L[R] N₁ × N₂ given by two continuous linear maps f₁ : M →L[R] N₁ and f₂ : M →L[R] N₂. This is the continuous version of LinearMap.prod.
ContinuousLinearMap.prodEquiv shows that the above is a bijection: every continuous linear map to a product is obtained this way. In other words, this is the universal property of the product.
ContinuousLinearMap.prodMap f₁ f₂ is the continuous linear map M₁ × M₂ →L[R] N₁ × N₂ given by two continuous linear maps f₁ : M₁ →L[R] N₁ and f₂ : M₂ →L[R] N₂. This is the continuous version of LinearMap.prodMap.

Binary products (viewed as categorical coproducts):

ContinuousLinearMap.inl R M₁ M₂ : M₁ →L[R] M₁ × M₂ and ContinuousLinearMap.inr R M₁ M₂ : M₂ →L[R] M₁ × M₂ are the two inclusions, given respectively by inl x = (x, 0) and inr x = (0, x). These are the continuous versions of LinearMap.inl and LinearMap.inr.
ContinuousLinearMap.coprod f₁ f₂ is the continuous linear map M₁ × M₂ →L[R] N given by two continuous linear maps f₁ : M₁ →L[R] N and f₂ : M₂ →L[R] N. This is the continuous version of LinearMap.coprod.
ContinuousLinearMap.coprodEquiv shows that the above is a bijection: every continuous linear map from a (binary) product is obtained this way. In other words, this is the universal property of the coproduct.

Indexed products:

ContinuousLinearMap.pi f is the continuous linear map M →L[R] (Π i, N i) given by a family f₁ : Π i, M →L[R] N i of continuous linear maps. This is the continuous version of LinearMap.pi.
ContinuousLinearMap.piMap f is the continuous linear map (Π i, M i) →L[R] (Π i, N i) given by a family f : Π i, M i →L[R] N i of continuous linear maps. This is the continuous version of LinearMap.piMap.
ContinuousLinearMap.proj j : (Π i, M i) →L[R] M j is the projection given by proj i f = f i. This is the continuous version of LinearMap.proj.

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

Instances For

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

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

Instances For

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

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

Instances For

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

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 ∘SL inl R M₁ M₂) v.1 + (L ∘SL inr R M₁ M₂) v.2 = L v

source

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

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

Instances For

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

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

Instances For

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₂) = ContinuousLinearMap.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₃ ∘SL 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₃ ∘SL f.prod g = g

source

@[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₂ ∘SL inl R M₁ M₂ = ContinuousLinearMap.id R M₁

source

@[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₂ ∘SL inr R M₁ M₂ = 0

source

@[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₂ ∘SL inl R M₁ M₂ = 0

source

@[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₂ ∘SL inr R M₁ M₂ = ContinuousLinearMap.id R M₂

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

f₁.prodMap f₂ = (f₁ ∘SL ContinuousLinearMap.fst R M₁ M₃).prod (f₂ ∘SL ContinuousLinearMap.snd R M₁ M₃)

Instances For

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

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

Instances For

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 ∘SL g = pi fun (i : ι) => f i ∘SL 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

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

Instances For

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 ∘SL 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 = ContinuousLinearMap.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 ∘SL 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 : ι), (↑(proj i)).ker = ⊥

source

def ContinuousLinearMap.piMap {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} [(i : ι) → TopologicalSpace (ψ i)] [(i : ι) → AddCommMonoid (ψ i)] [(i : ι) → Module R (ψ i)] (f : (i : ι) → φ i →L[R] ψ i) :

((i : ι) → φ i) →L[R] (i : ι) → ψ i

Construct a continuous linear map between two (dependent) function spaces by applying index-dependent linear maps to the coordinates. A bundled version of Pi.map.

If the index type is finite, then this map can be seen as a “block diagonal” map between indexed products of modules.

Equations

ContinuousLinearMap.piMap f = ContinuousLinearMap.pi fun (i : ι) => f i ∘SL ContinuousLinearMap.proj i

Instances For

source

@[simp]

theorem ContinuousLinearMap.coe_piMap {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} [(i : ι) → TopologicalSpace (ψ i)] [(i : ι) → AddCommMonoid (ψ i)] [(i : ι) → Module R (ψ i)] (f : (i : ι) → φ i →L[R] ψ i) :

↑(piMap f) = LinearMap.piMap fun (i : ι) => ↑(f i)

source

@[simp]

theorem ContinuousLinearMap.coe_piMap' {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} [(i : ι) → TopologicalSpace (ψ i)] [(i : ι) → AddCommMonoid (ψ i)] [(i : ι) → Module R (ψ i)] (f : (i : ι) → φ i →L[R] ψ i) :

⇑(piMap f) = Pi.map fun (i : ι) => ⇑(f 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 := ⋯ }

Instances For

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

ContinuousLinearMap.single R φ i = { toLinearMap := LinearMap.single R φ i, cont := ⋯ }

Instances For

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.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 ∘SL single R φ i) (v i) = L v

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 : (↑f).ker ⊔ (↑g).ker = ⊤) :

(↑(f.prod g)).range = (↑f).range.prod (↑g).range

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₃) :

(↑f).ker.prod (↑g).ker ≤ ((↑f).coprod ↑g).ker

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.

Instances For

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

See ContinuousLinearMap.prodL for the ContinuousLinearEquiv version.

Equations

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

Instances For

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

Instances For

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

(↑(f₁.coprod f₂)).range = (↑f₁).range ⊔ (↑f₂).range

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₁ ∘SL fst R M₁ M₂ + f₂ ∘SL 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 ∘SL g₁.coprod g₂ = (f ∘SL g₁).coprod (f ∘SL 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₂ ∘SL 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₂ ∘SL 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) = ContinuousLinearMap.id R (M × N)

source

@[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 ∘SL inl R M M₁).coprod (f ∘SL inr R M M₁) = f

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.

See ContinuousLinearMap.coprodEquivL for the ContinuousLinearEquiv version.

Equations