Module docstring
{"# Continuous linear maps on products and Pi types ","### Properties that hold for non-necessarily commutative semirings. "}
ContinuousLinearMap.prod
definition
(f₁ : M₁ →L[R] M₂) (f₂ : M₁ →L[R] M₃) : M₁ →L[R] M₂ × M₃
Full source
/-- The cartesian product of two bounded linear maps, as a bounded linear map. -/
protected def prod (f₁ : M₁ →L[R] M₂) (f₂ : M₁ →L[R] M₃) :
M₁ →L[R] M₂ × M₃ :=
⟨(f₁ : M₁ →ₗ[R] M₂).prod f₂, f₁.2.prodMk f₂.2⟩Informal description
Given two continuous linear maps \( f_1 : M_1 \to M_2 \) and \( f_2 : M_1 \to M_3 \) over a topological ring \( R \), the product map \( f_1 \times f_2 : M_1 \to M_2 \times M_3 \) is defined by \( (f_1 \times f_2)(x) = (f_1(x), f_2(x)) \) for all \( x \in M_1 \). This map is both linear and continuous with respect to the product topology on \( M_2 \times M_3 \).
ContinuousLinearMap.coe_prod
theorem
(f₁ : M₁ →L[R] M₂) (f₂ : M₁ →L[R] M₃) : (f₁.prod f₂ : M₁ →ₗ[R] M₂ × M₃) = LinearMap.prod f₁ f₂
Full source
@[simp, norm_cast]
theorem coe_prod (f₁ : M₁ →L[R] M₂) (f₂ : M₁ →L[R] M₃) :
(f₁.prod f₂ : M₁ →ₗ[R] M₂ × M₃) = LinearMap.prod f₁ f₂ :=
rflInformal description
For any continuous linear maps \( f_1 : M_1 \to M_2 \) and \( f_2 : M_1 \to M_3 \) over a topological ring \( R \), the underlying linear map of the product map \( f_1 \times f_2 \) is equal to the product of the underlying linear maps of \( f_1 \) and \( f_2 \). That is, \( (f_1 \times f_2) = f_1 \times f_2 \) as linear maps.
ContinuousLinearMap.prod_apply
theorem
(f₁ : M₁ →L[R] M₂) (f₂ : M₁ →L[R] M₃) (x : M₁) : f₁.prod f₂ x = (f₁ x, f₂ x)
Full source
@[simp, norm_cast]
theorem prod_apply (f₁ : M₁ →L[R] M₂) (f₂ : M₁ →L[R] M₃) (x : M₁) :
f₁.prod f₂ x = (f₁ x, f₂ x) :=
rflInformal description
For any continuous linear maps $f_1: M_1 \to_L[R] M_2$ and $f_2: M_1 \to_L[R] M_3$ over a topological ring $R$, and for any element $x \in M_1$, the product map $f_1 \times f_2$ evaluated at $x$ is equal to $(f_1(x), f_2(x))$.
ContinuousLinearMap.inl
definition
: M₁ →L[R] M₁ × M₂
Full source
/-- The left injection into a product is a continuous linear map. -/
def inl : M₁ →L[R] M₁ × M₂ :=
(id R M₁).prod 0Informal description
The left injection map \( \text{inl} : M_1 \to M_1 \times M_2 \) is a continuous linear map that sends an element \( x \in M_1 \) to \( (x, 0) \), where \( M_1 \) and \( M_2 \) are topological modules over a semiring \( R \).
ContinuousLinearMap.inr
definition
: M₂ →L[R] M₁ × M₂
Full source
/-- The right injection into a product is a continuous linear map. -/
def inr : M₂ →L[R] M₁ × M₂ :=
(0 : M₂ →L[R] M₁).prod (id R M₂)Informal description
The right injection map from a topological module $M_2$ to the product $M_1 \times M_2$ is a continuous linear map over the semiring $R$. Specifically, it maps each $x \in M_2$ to $(0, x) \in M_1 \times M_2$.
ContinuousLinearMap.inl_apply
theorem
(x : M₁) : inl R M₁ M₂ x = (x, 0)
Informal description
For any element $x$ in the topological module $M_1$ over a semiring $R$, the left injection continuous linear map $\text{inl} : M_1 \to M_1 \times M_2$ satisfies $\text{inl}(x) = (x, 0)$.
ContinuousLinearMap.inr_apply
theorem
(x : M₂) : inr R M₁ M₂ x = (0, x)
Informal description
For any element $x$ in the topological module $M_2$, the right injection continuous linear map $M_2 \to M_1 \times M_2$ maps $x$ to $(0, x)$.
ContinuousLinearMap.coe_inl
theorem
: (inl R M₁ M₂ : M₁ →ₗ[R] M₁ × M₂) = LinearMap.inl R M₁ M₂
Full source
@[simp, norm_cast]
theorem coe_inl : (inl R M₁ M₂ : M₁ →ₗ[R] M₁ × M₂) = LinearMap.inl R M₁ M₂ :=
rflInformal description
The underlying linear map of the continuous left injection map $\text{inl} \colon M_1 \to M_1 \times M_2$ over a topological ring $R$ is equal to the linear left injection map $\text{LinearMap.inl} \colon M_1 \to M_1 \times M_2$.
ContinuousLinearMap.coe_inr
theorem
: (inr R M₁ M₂ : M₂ →ₗ[R] M₁ × M₂) = LinearMap.inr R M₁ M₂
Full source
@[simp, norm_cast]
theorem coe_inr : (inr R M₁ M₂ : M₂ →ₗ[R] M₁ × M₂) = LinearMap.inr R M₁ M₂ :=
rflInformal description
The underlying linear map of the continuous linear right injection map $\text{inr} \colon M_2 \to M_1 \times M_2$ over a topological ring $R$ is equal to the linear right injection map $\text{LinearMap.inr} \colon M_2 \to M_1 \times M_2$.
ContinuousLinearMap.ker_prod
theorem
(f : M₁ →L[R] M₂) (g : M₁ →L[R] M₃) : ker (f.prod g) = ker f ⊓ ker g
Full source
@[simp]
theorem ker_prod (f : M₁ →L[R] M₂) (g : M₁ →L[R] M₃) :
ker (f.prod g) = kerker f ⊓ ker g :=
LinearMap.ker_prod (f : M₁ →ₗ[R] M₂) (g : M₁ →ₗ[R] M₃)Informal description
For continuous linear maps $f \colon M_1 \to M_2$ and $g \colon M_1 \to M_3$ over a topological ring $R$, the kernel of the product map $f \times g \colon M_1 \to M_2 \times M_3$ is equal to the intersection of the kernels of $f$ and $g$. That is,
\[ \ker(f \times g) = \ker f \cap \ker g. \]
ContinuousLinearMap.fst
definition
: M₁ × M₂ →L[R] M₁
Full source
/-- `Prod.fst` as a `ContinuousLinearMap`. -/
def fst : M₁ × M₂M₁ × M₂ →L[R] M₁ where
cont := continuous_fst
toLinearMap := LinearMap.fst R M₁ M₂Informal description
The first projection map $\pi_1 \colon M_1 \times M_2 \to M_1$ from the product of two topological modules $M_1$ and $M_2$ over a topological ring $R$ to $M_1$, viewed as a continuous linear map. This map sends each pair $(x, y) \in M_1 \times M_2$ to its first component $x \in M_1$.
ContinuousLinearMap.snd
definition
: M₁ × M₂ →L[R] M₂
Full source
/-- `Prod.snd` as a `ContinuousLinearMap`. -/
def snd : M₁ × M₂M₁ × M₂ →L[R] M₂ where
cont := continuous_snd
toLinearMap := LinearMap.snd R M₁ M₂Informal description
The second projection map $\text{snd} \colon M_1 \times M_2 \to M_2$ is a continuous linear map between the product module $M_1 \times M_2$ and $M_2$ over a topological ring $R$. This map sends a pair $(x, y)$ to its second component $y$ and is continuous with respect to the product topology on $M_1 \times M_2$ and the given topology on $M_2$.
ContinuousLinearMap.coe_fst
theorem
: ↑(fst R M₁ M₂) = LinearMap.fst R M₁ M₂
Full source
@[simp, norm_cast]
theorem coe_fst : ↑(fst R M₁ M₂) = LinearMap.fst R M₁ M₂ :=
rflInformal description
The underlying linear map of the continuous linear first projection map $\pi_1 \colon M_1 \times M_2 \to M_1$ is equal to the linear first projection map $\text{LinearMap.fst} \colon M_1 \times M_2 \to M_1$.
ContinuousLinearMap.coe_fst'
theorem
: ⇑(fst R M₁ M₂) = Prod.fst
Informal description
The underlying function of the continuous linear first projection map $fst \colon M_1 \times M_2 \to M_1$ is equal to the standard first projection function $\text{Prod.fst} \colon M_1 \times M_2 \to M_1$ that extracts the first component of a pair.
ContinuousLinearMap.coe_snd
theorem
: ↑(snd R M₁ M₂) = LinearMap.snd R M₁ M₂
Full source
@[simp, norm_cast]
theorem coe_snd : ↑(snd R M₁ M₂) = LinearMap.snd R M₁ M₂ :=
rflInformal description
The underlying linear map of the continuous linear second projection map $\text{snd} \colon M_1 \times M_2 \to M_2$ is equal to the linear second projection map $\text{snd} \colon M_1 \times M_2 \to M_2$.
ContinuousLinearMap.coe_snd'
theorem
: ⇑(snd R M₁ M₂) = Prod.snd
Informal description
The underlying function of the continuous linear second projection map $\text{snd} \colon M_1 \times M_2 \to M_2$ is equal to the standard second projection function $\text{Prod.snd} \colon M_1 \times M_2 \to M_2$, which sends a pair $(x, y)$ to $y$.
ContinuousLinearMap.fst_prod_snd
theorem
: (fst R M₁ M₂).prod (snd R M₁ M₂) = id R (M₁ × M₂)
Informal description
For any topological modules $M_1$ and $M_2$ over a topological ring $R$, the product of the first and second projection maps $\pi_1 \times \pi_2 \colon M_1 \times M_2 \to M_1 \times M_2$ is equal to the identity map on $M_1 \times M_2$. That is, $(\pi_1 \times \pi_2)(x, y) = (x, y)$ for all $(x, y) \in M_1 \times M_2$.
ContinuousLinearMap.fst_comp_prod
theorem
(f : M₁ →L[R] M₂) (g : M₁ →L[R] M₃) : (fst R M₂ M₃).comp (f.prod g) = f
Full source
@[simp]
theorem fst_comp_prod (f : M₁ →L[R] M₂) (g : M₁ →L[R] M₃) :
(fst R M₂ M₃).comp (f.prod g) = f :=
ext fun _x => rflInformal description
For any continuous linear maps $f \colon M_1 \to M_2$ and $g \colon M_1 \to M_3$ over a topological ring $R$, the composition of the first projection map $\pi_1 \colon M_2 \times M_3 \to M_2$ with the product map $f \times g \colon M_1 \to M_2 \times M_3$ equals $f$, i.e., $\pi_1 \circ (f \times g) = f$.
ContinuousLinearMap.snd_comp_prod
theorem
(f : M₁ →L[R] M₂) (g : M₁ →L[R] M₃) : (snd R M₂ M₃).comp (f.prod g) = g
Full source
@[simp]
theorem snd_comp_prod (f : M₁ →L[R] M₂) (g : M₁ →L[R] M₃) :
(snd R M₂ M₃).comp (f.prod g) = g :=
ext fun _x => rflInformal description
Let $R$ be a topological ring, and let $M_1$, $M_2$, and $M_3$ be topological modules over $R$. For any continuous linear maps $f \colon M_1 \to M_2$ and $g \colon M_1 \to M_3$, the composition of the second projection map $\text{snd} \colon M_2 \times M_3 \to M_3$ with the product map $f \times g \colon M_1 \to M_2 \times M_3$ equals $g$. That is, $\text{snd} \circ (f \times g) = g$.
ContinuousLinearMap.prodMap
definition
(f₁ : M₁ →L[R] M₂) (f₂ : M₃ →L[R] M₄) : M₁ × M₃ →L[R] M₂ × M₄
Full source
/-- `Prod.map` of two continuous linear maps. -/
def prodMap (f₁ : M₁ →L[R] M₂) (f₂ : M₃ →L[R] M₄) :
M₁ × M₃M₁ × M₃ →L[R] M₂ × M₄ :=
(f₁.comp (fst R M₁ M₃)).prod (f₂.comp (snd R M₁ M₃))Informal description
Given continuous linear maps \( f_1 \colon M_1 \to M_2 \) and \( f_2 \colon M_3 \to M_4 \) over a topological ring \( R \), the product map \( f_1 \times f_2 \colon M_1 \times M_3 \to M_2 \times M_4 \) is defined by \( (f_1 \times f_2)(x, y) = (f_1(x), f_2(y)) \) for all \( (x, y) \in M_1 \times M_3 \). This map is both linear and continuous with respect to the product topologies on \( M_1 \times M_3 \) and \( M_2 \times M_4 \).
ContinuousLinearMap.coe_prodMap
theorem
(f₁ : M₁ →L[R] M₂) (f₂ : M₃ →L[R] M₄) : ↑(f₁.prodMap f₂) = (f₁ : M₁ →ₗ[R] M₂).prodMap (f₂ : M₃ →ₗ[R] M₄)
Full source
@[simp, norm_cast]
theorem coe_prodMap (f₁ : M₁ →L[R] M₂)
(f₂ : M₃ →L[R] M₄) : ↑(f₁.prodMap f₂) = (f₁ : M₁ →ₗ[R] M₂).prodMap (f₂ : M₃ →ₗ[R] M₄) :=
rflInformal description
For any continuous linear maps \( f_1 \colon M_1 \to M_2 \) and \( f_2 \colon M_3 \to M_4 \) over a topological ring \( R \), the underlying linear map of the product map \( f_1 \times f_2 \colon M_1 \times M_3 \to M_2 \times M_4 \) is equal to the product of the underlying linear maps of \( f_1 \) and \( f_2 \). That is, \( (f_1 \times f_2) = f_1 \times f_2 \) as linear maps.
ContinuousLinearMap.coe_prodMap'
theorem
(f₁ : M₁ →L[R] M₂) (f₂ : M₃ →L[R] M₄) : ⇑(f₁.prodMap f₂) = Prod.map f₁ f₂
Full source
@[simp, norm_cast]
theorem coe_prodMap' (f₁ : M₁ →L[R] M₂)
(f₂ : M₃ →L[R] M₄) : ⇑(f₁.prodMap f₂) = Prod.map f₁ f₂ :=
rflInformal description
For any continuous linear maps $f_1 \colon M_1 \to M_2$ and $f_2 \colon M_3 \to M_4$ over a topological ring $R$, the underlying function of the product map $f_1 \times f_2 \colon M_1 \times M_3 \to M_2 \times M_4$ is equal to the product of the underlying functions of $f_1$ and $f_2$, i.e., $(f_1 \times f_2)(x, y) = (f_1(x), f_2(y))$ for all $(x, y) \in M_1 \times M_3$.
ContinuousLinearMap.pi
definition
(f : ∀ i, M →L[R] φ i) : M →L[R] ∀ i, φ i
Full source
/-- `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. -/
def pi (f : ∀ i, M →L[R] φ i) : M →L[R] ∀ i, φ i :=
⟨LinearMap.pi fun i => f i, continuous_pi fun i => (f i).continuous⟩Informal description
Given a family of continuous linear maps \( f_i : M \to \varphi_i \) for each index \( i \) in some index set, the function `ContinuousLinearMap.pi` constructs a continuous linear map from \( M \) to the product space \( \prod_{i} \varphi_i \), defined by \( c \mapsto (f_i(c))_{i} \). This map is continuous with respect to the product topology on the codomain.
ContinuousLinearMap.coe_pi'
theorem
(f : ∀ i, M →L[R] φ i) : ⇑(pi f) = fun c i => f i c
Full source
@[simp]
theorem coe_pi' (f : ∀ i, M →L[R] φ i) : ⇑(pi f) = fun c i => f i c :=
rflInformal description
For any family of continuous linear maps \( f_i : M \to \varphi_i \) indexed by \( i \), the underlying function of the continuous linear map \( \mathrm{pi}\, f \) from \( M \) to the product space \( \prod_{i} \varphi_i \) is given by \( (c, i) \mapsto f_i(c) \).
ContinuousLinearMap.coe_pi
theorem
(f : ∀ i, M →L[R] φ i) : (pi f : M →ₗ[R] ∀ i, φ i) = LinearMap.pi fun i => f i
Full source
@[simp]
theorem coe_pi (f : ∀ i, M →L[R] φ i) : (pi f : M →ₗ[R] ∀ i, φ i) = LinearMap.pi fun i => f i :=
rflInformal description
For any family of continuous linear maps \( f_i : M \to \varphi_i \) indexed by \( i \), the underlying linear map of the product continuous linear map \( \mathrm{pi} \, f \) is equal to the product linear map \( \mathrm{LinearMap.pi} \, (\lambda i, f_i) \). That is, the following diagram commutes:
\[
\mathrm{pi} \, f \text{ (as a linear map)} = \mathrm{LinearMap.pi} \, (\lambda i, f_i).
\]
ContinuousLinearMap.pi_apply
theorem
(f : ∀ i, M →L[R] φ i) (c : M) (i : ι) : pi f c i = f i c
Full source
theorem pi_apply (f : ∀ i, M →L[R] φ i) (c : M) (i : ι) : pi f c i = f i c :=
rflInformal description
For a family of continuous linear maps \( f_i : M \to \varphi_i \) indexed by \( i \in \iota \), the evaluation of the product map \( \pi f \) at a point \( c \in M \) and index \( i \) is equal to the evaluation of \( f_i \) at \( c \), i.e., \( (\pi f)(c)_i = f_i(c) \).
ContinuousLinearMap.pi_eq_zero
theorem
(f : ∀ i, M →L[R] φ i) : pi f = 0 ↔ ∀ i, f i = 0
Full source
theorem pi_eq_zero (f : ∀ i, M →L[R] φ i) : pipi f = 0 ↔ ∀ i, f i = 0 := by
simp only [ContinuousLinearMap.ext_iff, pi_apply, funext_iff]
exact forall_swapInformal description
For a family of continuous linear maps $f_i \colon M \to \varphi_i$ indexed by $i$, the continuous linear map $\prod_i f_i \colon M \to \prod_i \varphi_i$ is the zero map if and only if each $f_i$ is the zero map.
ContinuousLinearMap.pi_zero
theorem
: pi (fun _ => 0 : ∀ i, M →L[R] φ i) = 0
Full source
theorem pi_zero : pi (fun _ => 0 : ∀ i, M →L[R] φ i) = 0 :=
ext fun _ => rflInformal description
The continuous linear map into a product space, constructed from a family of zero maps, is itself the zero map. That is, if for each index $i$, the map $f_i \colon M \to \phi_i$ is the zero map, then the induced map $\prod_i f_i \colon M \to \prod_i \phi_i$ is also the zero map.
ContinuousLinearMap.pi_comp
theorem
(f : ∀ i, M →L[R] φ i) (g : M₂ →L[R] M) : (pi f).comp g = pi fun i => (f i).comp g
Full source
theorem pi_comp (f : ∀ i, M →L[R] φ i) (g : M₂ →L[R] M) :
(pi f).comp g = pi fun i => (f i).comp g :=
rflInformal description
Let $R$ be a semiring, and let $M$, $M_2$, and $\{\phi_i\}_{i \in \iota}$ be topological modules over $R$ with additive commutative monoid structures. Given a family of continuous linear maps $f_i : M \to \phi_i$ for each $i \in \iota$ and a continuous linear map $g : M_2 \to M$, the composition of the product map $\prod_i f_i$ with $g$ equals the product of the compositions $\prod_i (f_i \circ g)$. That is,
$$(\prod_i f_i) \circ g = \prod_i (f_i \circ g).$$
ContinuousLinearMap.proj
definition
(i : ι) : (∀ i, φ i) →L[R] φ i
Full source
/-- The projections from a family of topological modules are continuous linear maps. -/
def proj (i : ι) : (∀ i, φ i) →L[R] φ i :=
⟨LinearMap.proj i, continuous_apply _⟩Informal description
For each index $i$ in the index set $\iota$, the projection map $\text{proj}_i$ is a continuous linear map from the product space $\prod_{i \in \iota} \phi_i$ to the component space $\phi_i$. Specifically, $\text{proj}_i$ evaluates a function $b$ at the index $i$, i.e., $\text{proj}_i(b) = b(i)$.
ContinuousLinearMap.proj_apply
theorem
(i : ι) (b : ∀ i, φ i) : (proj i : (∀ i, φ i) →L[R] φ i) b = b i
Full source
@[simp]
theorem proj_apply (i : ι) (b : ∀ i, φ i) : (proj i : (∀ i, φ i) →L[R] φ i) b = b i :=
rflInformal description
For any index $i$ in the index set $\iota$ and any element $b$ in the product space $\prod_{i \in \iota} \phi_i$, the evaluation of the continuous linear projection map $\text{proj}_i$ at $b$ is equal to $b(i)$, i.e., $\text{proj}_i(b) = b(i)$.
ContinuousLinearMap.proj_pi
theorem
(f : ∀ i, M₂ →L[R] φ i) (i : ι) : (proj i).comp (pi f) = f i
Informal description
Let $R$ be a semiring, $\iota$ an index set, and $\{\phi_i\}_{i \in \iota}$ a family of topological modules over $R$ with additive commutative monoid structures. For any family of continuous linear maps $f_i : M_2 \to \phi_i$ indexed by $i \in \iota$, the composition of the projection map $\text{proj}_i : \prod_{j \in \iota} \phi_j \to \phi_i$ with the product map $\pi(f) : M_2 \to \prod_{j \in \iota} \phi_j$ (defined by $\pi(f)(x) = (f_j(x))_{j \in \iota}$) equals the $i$-th component map $f_i$. In symbols:
\[ \text{proj}_i \circ \pi(f) = f_i \]
ContinuousLinearMap.coe_proj
theorem
(i : ι) : (proj i).toLinearMap = (LinearMap.proj i : ((i : ι) → φ i) →ₗ[R] _)
Full source
@[simp]
theorem coe_proj (i : ι) : (proj i).toLinearMap = (LinearMap.proj i : ((i : ι) → φ i) →ₗ[R] _) :=
rflInformal description
For each index $i$ in the index set $\iota$, the underlying linear map of the continuous linear projection $\text{proj}_i : \prod_{j \in \iota} \phi_j \to \phi_i$ is equal to the linear projection map $\text{proj}_i : \prod_{j \in \iota} \phi_j \to \phi_i$.
ContinuousLinearMap.pi_proj
theorem
: pi proj = .id R (∀ i, φ i)
Informal description
Let $R$ be a semiring, $\iota$ an index set, and $\{\phi_i\}_{i \in \iota}$ a family of topological modules over $R$ with additive commutative monoid structures. The composition of the continuous linear map $\pi$ (which constructs a map into the product space $\prod_{i \in \iota} \phi_i$ from a family of component maps) with the family of projection maps $\{\text{proj}_i\}_{i \in \iota}$ is equal to the identity map on the product space $\prod_{i \in \iota} \phi_i$. In symbols:
\[ \pi(\text{proj}_i)_{i \in \iota} = \text{id}_{\prod_{i \in \iota} \phi_i} \]
ContinuousLinearMap.pi_proj_comp
theorem
(f : M₂ →L[R] ∀ i, φ i) : pi (proj · ∘L f) = f
Full source
@[simp]
theorem pi_proj_comp (f : M₂ →L[R] ∀ i, φ i) : pi (projproj · ∘L f) = f := rflInformal description
Let $R$ be a semiring, $\iota$ an index set, and $\{\phi_i\}_{i \in \iota}$ a family of topological modules over $R$ with additive commutative monoid structures. For any continuous linear map $f : M_2 \to \prod_{i \in \iota} \phi_i$, the composition of the projection maps $\text{proj}_i \circ f$ with the product map $\pi$ equals $f$. In symbols:
\[ \pi(\text{proj}_i \circ f)_{i \in \iota} = f \]
ContinuousLinearMap.iInf_ker_proj
theorem
: (⨅ i, ker (proj i : (∀ i, φ i) →L[R] φ i) : Submodule R (∀ i, φ i)) = ⊥
Full source
theorem iInf_ker_proj : (⨅ i, ker (proj i : (∀ i, φ i) →L[R] φ i) : Submodule R (∀ i, φ i)) = ⊥ :=
LinearMap.iInf_ker_projInformal description
For a family of topological modules $\{\phi_i\}_{i \in \iota}$ over a semiring $R$, the intersection of the kernels of all continuous linear projection maps $\text{proj}_i : \prod_{i \in \iota} \phi_i \to \phi_i$ is the trivial submodule $\{0\}$. In other words:
\[ \bigcap_{i \in \iota} \ker(\text{proj}_i) = \bot \]
Pi.compRightL
definition
{α : Type*} (f : α → ι) : ((i : ι) → φ i) →L[R] ((i : α) → φ (f i))
Full source
/-- 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. -/
def _root_.Pi.compRightL {α : Type*} (f : α → ι) : ((i : ι) → φ i) →L[R] ((i : α) → φ (f i)) where
toFun := fun v i ↦ v (f i)
map_add' := by intros; ext; simp
map_smul' := by intros; ext; simp
cont := by continuityInformal description
Given a function $f: \alpha \to \iota$, the continuous linear map $\text{Pi.compRightL}$ is defined by right composition on product types. Specifically, for any vector $v$ in the product space $\prod_{i \in \iota} \phi_i$, the map sends $v$ to the vector in $\prod_{i \in \alpha} \phi_{f(i)}$ whose $i$-th component is $v(f(i))$. This map is additive, linear, and continuous with respect to the product topologies.
Pi.compRightL_apply
theorem
{α : Type*} (f : α → ι) (v : (i : ι) → φ i) (i : α) : Pi.compRightL R φ f v i = v (f i)
Full source
@[simp] lemma _root_.Pi.compRightL_apply {α : Type*} (f : α → ι) (v : (i : ι) → φ i) (i : α) :
Pi.compRightL R φ f v i = v (f i) := rflInformal description
Let $R$ be a semiring, $\iota$ and $\alpha$ be types, and $(\phi_i)_{i \in \iota}$ be a family of topological $R$-modules. Given a function $f \colon \alpha \to \iota$, a vector $v \in \prod_{i \in \iota} \phi_i$, and an index $i \in \alpha$, the $i$-th component of the continuous linear map $\mathrm{Pi.compRightL}_{R,\phi} f$ applied to $v$ is equal to $v(f(i))$. In other words, $(\mathrm{Pi.compRightL}_{R,\phi} f \, v)_i = v_{f(i)}$.
ContinuousLinearMap.single
definition
[DecidableEq ι] (i : ι) : φ i →L[R] (∀ i, φ i)
Full source
/-- `Pi.single` as a bundled continuous linear map. -/
@[simps! -fullyApplied]
def single [DecidableEq ι] (i : ι) : φ i →L[R] (∀ i, φ i) where
toLinearMap := .single R φ i
cont := continuous_single _Informal description
For a decidable index type $\iota$ and a family of topological $R$-modules $(\phi_i)_{i \in \iota}$, the continuous linear map $\text{single}_i : \phi_i \to \prod_{j \in \iota} \phi_j$ is defined as the continuous linear extension of the function that maps an element $x \in \phi_i$ to the tuple $(0, \ldots, 0, x, 0, \ldots, 0)$ where $x$ appears in the $i$-th position. This is the continuous linear algebra version of the single function in the additive monoid homomorphism context.
ContinuousLinearMap.range_prod_eq
theorem
{f : M →L[R] M₂} {g : M →L[R] M₃} (h : ker f ⊔ ker g = ⊤) : range (f.prod g) = (range f).prod (range g)
Full source
theorem range_prod_eq {f : M →L[R] M₂} {g : M →L[R] M₃} (h : kerker f ⊔ ker g = ⊤) :
range (f.prod g) = (range f).prod (range g) :=
LinearMap.range_prod_eq hInformal description
Let $R$ be a topological ring, and let $M$, $M_2$, and $M_3$ be topological $R$-modules. Given continuous linear maps $f \colon M \to M_2$ and $g \colon M \to M_3$ such that the join of their kernels spans $M$ (i.e., $\ker f \sqcup \ker g = \top$), the range of the product map $f \times g \colon M \to M_2 \times M_3$ is equal to the product of their ranges:
\[ \operatorname{range}(f \times g) = (\operatorname{range} f) \times (\operatorname{range} g). \]
ContinuousLinearMap.ker_prod_ker_le_ker_coprod
theorem
(f : M →L[R] M₃) (g : M₂ →L[R] M₃) : (LinearMap.ker f).prod (LinearMap.ker g) ≤ LinearMap.ker (f.coprod g)
Full source
theorem ker_prod_ker_le_ker_coprod (f : M →L[R] M₃) (g : M₂ →L[R] M₃) :
(LinearMap.ker f).prod (LinearMap.ker g) ≤ LinearMap.ker (f.coprod g) :=
LinearMap.ker_prod_ker_le_ker_coprod f.toLinearMap g.toLinearMapInformal description
Let $R$ be a ring, and let $M$, $M_2$, and $M_3$ be topological $R$-modules. For any continuous linear maps $f \colon M \to M_3$ and $g \colon M_2 \to M_3$, the product of their kernels is contained in the kernel of their coproduct, i.e.,
\[ (\ker f) \times (\ker g) \subseteq \ker (f \operatorname{coprod} g). \]
ContinuousLinearMap.prodEquiv
definition
: (M →L[R] M₂) × (M →L[R] M₃) ≃ (M →L[R] M₂ × M₃)
Full source
/-- `ContinuousLinearMap.prod` as an `Equiv`. -/
@[simps apply]
def prodEquiv : (M →L[R] M₂) × (M →L[R] M₃)(M →L[R] M₂) × (M →L[R] M₃) ≃ (M →L[R] M₂ × M₃) where
toFun f := f.1.prod f.2
invFun f := ⟨(fst _ _ _).comp f, (snd _ _ _).comp f⟩
left_inv f := by ext <;> rfl
right_inv f := by ext <;> rflInformal description
The equivalence between the product of continuous linear maps $(M \to_{L[R]} M_2) \times (M \to_{L[R]} M_3)$ and the continuous linear maps into the product space $M \to_{L[R]} (M_2 \times M_3)$.
Specifically:
- The forward map takes a pair of continuous linear maps $(f_1, f_2)$ to the product map $f_1 \times f_2$ defined by $(f_1 \times f_2)(x) = (f_1(x), f_2(x))$.
- The inverse map takes a continuous linear map $f \colon M \to M_2 \times M_3$ to the pair of maps $(\pi_1 \circ f, \pi_2 \circ f)$, where $\pi_1$ and $\pi_2$ are the first and second projection maps respectively.
This equivalence is bijective and preserves all relevant structures.
ContinuousLinearMap.prod_ext_iff
theorem
{f g : M × M₂ →L[R] M₃} : f = g ↔ f.comp (inl _ _ _) = g.comp (inl _ _ _) ∧ f.comp (inr _ _ _) = g.comp (inr _ _ _)
Full source
theorem prod_ext_iff {f g : M × M₂M × M₂ →L[R] M₃} :
f = g ↔ f.comp (inl _ _ _) = g.comp (inl _ _ _) ∧ f.comp (inr _ _ _) = g.comp (inr _ _ _) := by
simp only [← coe_inj, LinearMap.prod_ext_iff]
rflInformal description
Let $M$, $M_2$, and $M_3$ be topological modules over a semiring $R$, and let $f, g \colon M \times M_2 \to M_3$ be continuous linear maps. Then $f = g$ if and only if both $f \circ \text{inl} = g \circ \text{inl}$ and $f \circ \text{inr} = g \circ \text{inr}$, where $\text{inl} \colon M \to M \times M_2$ and $\text{inr} \colon M_2 \to M \times M_2$ are the canonical left and right injection maps.
ContinuousLinearMap.prod_ext
theorem
{f g : M × M₂ →L[R] M₃} (hl : f.comp (inl _ _ _) = g.comp (inl _ _ _)) (hr : f.comp (inr _ _ _) = g.comp (inr _ _ _)) :
f = g
Informal description
Let $M$, $M_2$, and $M_3$ be topological modules over a semiring $R$, and let $f, g \colon M \times M_2 \to M_3$ be continuous linear maps. If $f \circ \text{inl} = g \circ \text{inl}$ and $f \circ \text{inr} = g \circ \text{inr}$, where $\text{inl} \colon M \to M \times M_2$ and $\text{inr} \colon M_2 \to M \times M_2$ are the canonical left and right injection maps, then $f = g$.
ContinuousLinearMap.prodₗ
definition
: ((M →L[R] M₂) × (M →L[R] M₃)) ≃ₗ[S] M →L[R] M₂ × M₃
Informal description
The linear equivalence between the product of continuous linear maps $(M \to_{L[R]} M_2) \times (M \to_{L[R]} M_3)$ and the space of continuous linear maps from $M$ to the product space $M_2 \times M_3$.
Specifically, this equivalence:
- Takes a pair of continuous linear maps $(f, g)$ to the product map $x \mapsto (f(x), g(x))$
- Has an inverse that decomposes a continuous linear map $h \colon M \to M_2 \times M_3$ into its component maps $(\pi_1 \circ h, \pi_2 \circ h)$
- Preserves addition and scalar multiplication (making it a linear equivalence)
ContinuousLinearMap.coprod
definition
(f₁ : M₁ →L[R] M) (f₂ : M₂ →L[R] M) : M₁ × M₂ →L[R] M
Full source
/-- The continuous linear map given by `(x, y) ↦ f₁ x + f₂ y`. -/
@[simps! coe apply]
def coprod (f₁ : M₁ →L[R] M) (f₂ : M₂ →L[R] M) : M₁ × M₂M₁ × M₂ →L[R] M :=
⟨.coprod f₁ f₂, (f₁.cont.comp continuous_fst).add (f₂.cont.comp continuous_snd)⟩Informal description
Given two continuous linear maps \( f_1 \colon M_1 \to M \) and \( f_2 \colon M_2 \to M \) over a ring \( R \), the continuous linear map \( \operatorname{coprod} f_1 f_2 \colon M_1 \times M_2 \to M \) is defined by \( (x, y) \mapsto f_1(x) + f_2(y) \). This map is continuous with respect to the product topology on \( M_1 \times M_2 \).
ContinuousLinearMap.coprod_add
theorem
(f₁ g₁ : M₁ →L[R] M) (f₂ g₂ : M₂ →L[R] M) : (f₁ + g₁).coprod (f₂ + g₂) = f₁.coprod f₂ + g₁.coprod g₂
Full source
@[simp] lemma coprod_add (f₁ g₁ : M₁ →L[R] M) (f₂ g₂ : M₂ →L[R] M) :
(f₁ + g₁).coprod (f₂ + g₂) = f₁.coprod f₂ + g₁.coprod g₂ := by ext <;> simpInformal description
Let $R$ be a semiring, and let $M_1$, $M_2$, and $M$ be topological modules over $R$. For any continuous linear maps $f_1, g_1 \colon M_1 \to M$ and $f_2, g_2 \colon M_2 \to M$, the coproduct of the sums $f_1 + g_1$ and $f_2 + g_2$ equals the sum of the coproducts $f_1 \coprod f_2$ and $g_1 \coprod g_2$. That is,
$$(f_1 + g_1) \coprod (f_2 + g_2) = (f_1 \coprod f_2) + (g_1 \coprod g_2).$$
ContinuousLinearMap.range_coprod
theorem
(f₁ : M₁ →L[R] M) (f₂ : M₂ →L[R] M) : range (f₁.coprod f₂) = range f₁ ⊔ range f₂
Full source
lemma range_coprod (f₁ : M₁ →L[R] M) (f₂ : M₂ →L[R] M) :
range (f₁.coprod f₂) = rangerange f₁ ⊔ range f₂ := LinearMap.range_coprod ..Informal description
Let $R$ be a semiring, and let $M_1$, $M_2$, and $M$ be topological modules over $R$ with additive commutative monoid structures. Given continuous linear maps $f_1 \colon M_1 \to M$ and $f_2 \colon M_2 \to M$, the range of their coproduct map $(x, y) \mapsto f_1(x) + f_2(y)$ is equal to the supremum of their individual ranges:
\[
\operatorname{range}(f_1 \sqcup f_2) = \operatorname{range}(f_1) \sqcup \operatorname{range}(f_2).
\]
ContinuousLinearMap.comp_fst_add_comp_snd
theorem
(f₁ : M₁ →L[R] M) (f₂ : M₂ →L[R] M) : f₁.comp (.fst _ _ _) + f₂.comp (.snd _ _ _) = f₁.coprod f₂
Full source
lemma comp_fst_add_comp_snd (f₁ : M₁ →L[R] M) (f₂ : M₂ →L[R] M) :
f₁.comp (.fst _ _ _) + f₂.comp (.snd _ _ _) = f₁.coprod f₂ := rflInformal description
Let $R$ be a topological ring, and let $M_1$, $M_2$, and $M$ be topological $R$-modules. For any continuous linear maps $f_1 \colon M_1 \to M$ and $f_2 \colon M_2 \to M$, the sum of the compositions of $f_1$ with the first projection $\pi_1 \colon M_1 \times M_2 \to M_1$ and $f_2$ with the second projection $\pi_2 \colon M_1 \times M_2 \to M_2$ equals the coproduct map $(x,y) \mapsto f_1(x) + f_2(y)$. That is,
$$ f_1 \circ \pi_1 + f_2 \circ \pi_2 = f_1 \coprod f_2. $$
ContinuousLinearMap.comp_coprod
theorem
(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₂)
Full source
lemma comp_coprod (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₂) :=
coe_injective <| LinearMap.comp_coprod ..Informal description
Let $R$ be a ring, and let $M$, $M_1$, $M_2$, and $N$ be topological $R$-modules. For any continuous linear maps $f \colon M \to N$, $g_1 \colon M_1 \to M$, and $g_2 \colon M_2 \to M$, the composition of $f$ with the coproduct of $g_1$ and $g_2$ is equal to the coproduct of the compositions $f \circ g_1$ and $f \circ g_2$. That is,
$$ f \circ (g_1 \coprod g_2) = (f \circ g_1) \coprod (f \circ g_2). $$
ContinuousLinearMap.coprod_comp_inl
theorem
(f₁ : M₁ →L[R] M) (f₂ : M₂ →L[R] M) : (f₁.coprod f₂).comp (.inl _ _ _) = f₁
Full source
@[simp] lemma coprod_comp_inl (f₁ : M₁ →L[R] M) (f₂ : M₂ →L[R] M) :
(f₁.coprod f₂).comp (.inl _ _ _) = f₁ := coe_injective <| LinearMap.coprod_inl ..Informal description
Let $R$ be a ring, and let $M_1$, $M_2$, and $M$ be topological $R$-modules. For any continuous linear maps $f_1 \colon M_1 \to M$ and $f_2 \colon M_2 \to M$, the composition of the coproduct map $f_1 \coprod f_2 \colon M_1 \times M_2 \to M$ with the left injection map $\text{inl} \colon M_1 \to M_1 \times M_2$ equals $f_1$. That is,
$$ (f_1 \coprod f_2) \circ \text{inl} = f_1. $$
ContinuousLinearMap.coprod_comp_inr
theorem
(f₁ : M₁ →L[R] M) (f₂ : M₂ →L[R] M) : (f₁.coprod f₂).comp (.inr _ _ _) = f₂
Full source
@[simp] lemma coprod_comp_inr (f₁ : M₁ →L[R] M) (f₂ : M₂ →L[R] M) :
(f₁.coprod f₂).comp (.inr _ _ _) = f₂ := coe_injective <| LinearMap.coprod_inr ..Informal description
Let $R$ be a ring, and let $M_1$, $M_2$, and $M$ be topological $R$-modules. For any continuous linear maps $f_1 \colon M_1 \to M$ and $f_2 \colon M_2 \to M$, the composition of the coproduct map $f_1 \coprod f_2 \colon M_1 \times M_2 \to M$ with the right injection $\text{inr} \colon M_2 \to M_1 \times M_2$ equals $f_2$. That is,
$$ (f_1 \coprod f_2) \circ \text{inr} = f_2. $$
ContinuousLinearMap.coprod_inl_inr
theorem
: ContinuousLinearMap.coprod (.inl R M N) (.inr R M N) = .id R (M × N)
Full source
@[simp]
lemma coprod_inl_inr : ContinuousLinearMap.coprod (.inl R M N) (.inr R M N) = .id R (M × N) :=
coe_injective <| LinearMap.coprod_inl_inrInformal description
For any topological modules $M$ and $N$ over a semiring $R$, the coproduct of the left injection $\operatorname{inl} \colon M \to M \times N$ and the right injection $\operatorname{inr} \colon N \to M \times N$ equals the identity map on $M \times N$. That is,
$$\operatorname{coprod}(\operatorname{inl}, \operatorname{inr}) = \operatorname{id}_{M \times N}.$$
ContinuousLinearMap.coprodEquiv
definition
[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
Full source
/-- 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`. -/
@[simps]
def coprodEquiv [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 where
toFun f := f.1.coprod f.2
invFun f := (f.comp (.inl ..), f.comp (.inr ..))
left_inv f := by simp
right_inv f := by simp [← comp_coprod f (.inl R M₁ M₂)]
map_add' a b := coprod_add ..
map_smul' r a := by
dsimp
ext <;> simp [smul_add, smul_apply, Prod.smul_snd, Prod.smul_fst, coprod_apply]Informal description
Given topological modules $M_1$, $M_2$, and $M$ over a semiring $R$, with $M$ also being a module over a semiring $S$ and having continuous scalar multiplication by $S$, there is a linear equivalence between the product space of continuous linear maps $(M_1 \toL[R] M) \times (M_2 \toL[R] M)$ and the space of continuous linear maps from the product $M_1 \times M_2$ to $M$. This equivalence is given by the coproduct operation, which combines two maps into one by pointwise addition, and its inverse decomposes a map on the product back into its components via left and right injections.
ContinuousLinearMap.ker_coprod_of_disjoint_range
theorem
{f₁ : M₁ →L[R] M} {f₂ : M₂ →L[R] M} (hf : Disjoint (range f₁) (range f₂)) :
LinearMap.ker (f₁.coprod f₂) = (LinearMap.ker f₁).prod (LinearMap.ker f₂)
Full source
lemma ker_coprod_of_disjoint_range {f₁ : M₁ →L[R] M} {f₂ : M₂ →L[R] M}
(hf : Disjoint (range f₁) (range f₂)) :
LinearMap.ker (f₁.coprod f₂) = (LinearMap.ker f₁).prod (LinearMap.ker f₂) :=
LinearMap.ker_coprod_of_disjoint_range f₁.toLinearMap f₂.toLinearMap hfInformal description
Let $R$ be a semiring, and let $M_1$, $M_2$, and $M$ be topological modules over $R$ with additive commutative monoid structures. Given two continuous linear maps $f_1 \colon M_1 \to M$ and $f_2 \colon M_2 \to M$ such that their ranges are disjoint (i.e., $\operatorname{range} f_1 \cap \operatorname{range} f_2 = \{0\}$), the kernel of their coproduct map $f_1 \operatorname{coprod} f_2 \colon M_1 \times M_2 \to M$ is equal to the product of their kernels:
\[ \ker(f_1 \operatorname{coprod} f_2) = (\ker f_1) \times (\ker f_2). \]