Continuous linear maps on products and Pi types #
Properties that hold for non-necessarily commutative semirings. #
The cartesian product of two bounded linear maps, as a bounded linear map.
Equations
- f₁.prod f₂ = { toLinearMap := (↑f₁).prod ↑f₂, cont := ⋯ }
Instances For
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
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
Prod.fst
as a ContinuousLinearMap
.
Equations
- ContinuousLinearMap.fst R M₁ M₂ = { toLinearMap := LinearMap.fst R M₁ M₂, cont := ⋯ }
Instances For
Prod.snd
as a ContinuousLinearMap
.
Equations
- ContinuousLinearMap.snd R M₁ M₂ = { toLinearMap := LinearMap.snd R M₁ M₂, cont := ⋯ }
Instances For
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
The continuous linear map given by (x, y) ↦ f₁ x + f₂ y
.
Equations
- f₁.coprod f₂ = { toLinearMap := (↑f₁).coprod ↑f₂, cont := ⋯ }
Instances For
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
The projections from a family of topological modules are continuous linear maps.
Equations
- ContinuousLinearMap.proj i = { toLinearMap := LinearMap.proj i, cont := ⋯ }
Instances For
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
ContinuousLinearMap.prod
as an Equiv
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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 := ⋯ }