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

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

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

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

f₁.prodMap f₂ = (f₁.comp (ContinuousLinearMap.fst R M₁ M₃)).prod (f₂.comp (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).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

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

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.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.

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.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

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

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.

Instances For

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

Documentation

Mathlib.Topology.Algebra.Module.LinearMapPiProd

Continuous linear maps on products and Pi types #

Properties that hold for non-necessarily commutative semirings. #