Pi types of modules #
This file defines constructors for linear maps whose domains or codomains are pi types.
It contains theorems relating these to each other, as well as to linear_map.ker.
Main definitions #
- pi types in the codomain:
- pi types in the domain:
linear_map.diag
def
linear_map.pi
{R : Type u}
{M₂ : Type w}
{ι : Type x}
[semiring R]
[add_comm_monoid M₂]
[module R M₂]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(f : Π (i : ι), M₂ →ₗ[R] φ i) :
pi construction for linear functions. From a family of linear functions it produces a linear
function into a family of modules.
@[simp]
theorem
linear_map.pi_apply
{R : Type u}
{M₂ : Type w}
{ι : Type x}
[semiring R]
[add_comm_monoid M₂]
[module R M₂]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(f : Π (i : ι), M₂ →ₗ[R] φ i)
(c : M₂)
(i : ι) :
⇑(linear_map.pi f) c i = ⇑(f i) c
theorem
linear_map.ker_pi
{R : Type u}
{M₂ : Type w}
{ι : Type x}
[semiring R]
[add_comm_monoid M₂]
[module R M₂]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(f : Π (i : ι), M₂ →ₗ[R] φ i) :
(linear_map.pi f).ker = ⨅ (i : ι), (f i).ker
theorem
linear_map.pi_eq_zero
{R : Type u}
{M₂ : Type w}
{ι : Type x}
[semiring R]
[add_comm_monoid M₂]
[module R M₂]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(f : Π (i : ι), M₂ →ₗ[R] φ i) :
linear_map.pi f = 0 ↔ ∀ (i : ι), f i = 0
theorem
linear_map.pi_zero
{R : Type u}
{M₂ : Type w}
{ι : Type x}
[semiring R]
[add_comm_monoid M₂]
[module R M₂]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)] :
linear_map.pi (λ (i : ι), 0) = 0
theorem
linear_map.pi_comp
{R : Type u}
{M₂ : Type w}
{M₃ : Type y}
{ι : Type x}
[semiring R]
[add_comm_monoid M₂]
[module R M₂]
[add_comm_monoid M₃]
[module R M₃]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(f : Π (i : ι), M₂ →ₗ[R] φ i)
(g : M₃ →ₗ[R] M₂) :
(linear_map.pi f).comp g = linear_map.pi (λ (i : ι), (f i).comp g)
def
linear_map.proj
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(i : ι) :
The projections from a family of modules are linear maps.
Note: known here as linear_map.proj, this construction is in other categories called eval, for
example pi.eval_monoid_hom, pi.eval_ring_hom.
Equations
- linear_map.proj i = {to_fun := function.eval i, map_add' := _, map_smul' := _}
@[simp]
theorem
linear_map.coe_proj
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(i : ι) :
⇑(linear_map.proj i) = function.eval i
theorem
linear_map.proj_apply
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(i : ι)
(b : Π (i : ι), φ i) :
⇑(linear_map.proj i) b = b i
theorem
linear_map.proj_pi
{R : Type u}
{M₂ : Type w}
{ι : Type x}
[semiring R]
[add_comm_monoid M₂]
[module R M₂]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(f : Π (i : ι), M₂ →ₗ[R] φ i)
(i : ι) :
(linear_map.proj i).comp (linear_map.pi f) = f i
theorem
linear_map.infi_ker_proj
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)] :
(⨅ (i : ι), (linear_map.proj i).ker) = ⊥
@[simp]
theorem
linear_map.comp_left_apply
{R : Type u}
{M₂ : Type w}
{M₃ : Type y}
[semiring R]
[add_comm_monoid M₂]
[module R M₂]
[add_comm_monoid M₃]
[module R M₃]
(f : M₂ →ₗ[R] M₃)
(I : Type u_1)
(h : I → M₂)
(ᾰ : I) :
def
linear_map.comp_left
{R : Type u}
{M₂ : Type w}
{M₃ : Type y}
[semiring R]
[add_comm_monoid M₂]
[module R M₂]
[add_comm_monoid M₃]
[module R M₃]
(f : M₂ →ₗ[R] M₃)
(I : Type u_1) :
Linear map between the function spaces I → M₂ and I → M₃, induced by a linear map f
between M₂ and M₃.
theorem
linear_map.apply_single
{R : Type u}
{M : Type v}
{ι : Type x}
[semiring R]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[add_comm_monoid M]
[module R M]
[decidable_eq ι]
(f : Π (i : ι), φ i →ₗ[R] M)
(i j : ι)
(x : φ i) :
def
linear_map.single
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[decidable_eq ι]
(i : ι) :
The linear_map version of add_monoid_hom.single and pi.single.
@[simp]
theorem
linear_map.coe_single
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[decidable_eq ι]
(i : ι) :
⇑(linear_map.single i) = pi.single i
def
linear_map.lsum
(R : Type u)
{M : Type v}
{ι : Type x}
[semiring R]
(φ : ι → Type i)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(S : Type u_1)
[add_comm_monoid M]
[module R M]
[fintype ι]
[decidable_eq ι]
[semiring S]
[module S M]
[smul_comm_class R S M] :
The linear equivalence between linear functions on a finite product of modules and families of functions on these modules. See note [bundled maps over different rings].
@[simp]
theorem
linear_map.lsum_apply
(R : Type u)
{M : Type v}
{ι : Type x}
[semiring R]
(φ : ι → Type i)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(S : Type u_1)
[add_comm_monoid M]
[module R M]
[fintype ι]
[decidable_eq ι]
[semiring S]
[module S M]
[smul_comm_class R S M]
(f : Π (i : ι), φ i →ₗ[R] M) :
⇑(linear_map.lsum R φ S) f = ∑ (i : ι), (f i).comp (linear_map.proj i)
@[simp]
theorem
linear_map.lsum_symm_apply
(R : Type u)
{M : Type v}
{ι : Type x}
[semiring R]
(φ : ι → Type i)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(S : Type u_1)
[add_comm_monoid M]
[module R M]
[fintype ι]
[decidable_eq ι]
[semiring S]
[module S M]
[smul_comm_class R S M]
(f : (Π (i : ι), φ i) →ₗ[R] M)
(i : ι) :
⇑((linear_map.lsum R φ S).symm) f i = f.comp (linear_map.single i)
theorem
linear_map.pi_ext
{R : Type u}
{M : Type v}
{ι : Type x}
[semiring R]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[fintype ι]
[decidable_eq ι]
[add_comm_monoid M]
[module R M]
{f g : (Π (i : ι), φ i) →ₗ[R] M}
(h : ∀ (i : ι) (x : φ i), ⇑f (pi.single i x) = ⇑g (pi.single i x)) :
f = g
theorem
linear_map.pi_ext_iff
{R : Type u}
{M : Type v}
{ι : Type x}
[semiring R]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[fintype ι]
[decidable_eq ι]
[add_comm_monoid M]
[module R M]
{f g : (Π (i : ι), φ i) →ₗ[R] M} :
@[ext]
theorem
linear_map.pi_ext'
{R : Type u}
{M : Type v}
{ι : Type x}
[semiring R]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[fintype ι]
[decidable_eq ι]
[add_comm_monoid M]
[module R M]
{f g : (Π (i : ι), φ i) →ₗ[R] M}
(h : ∀ (i : ι), f.comp (linear_map.single i) = g.comp (linear_map.single i)) :
f = g
This is used as the ext lemma instead of linear_map.pi_ext for reasons explained in
note [partially-applied ext lemmas].
theorem
linear_map.pi_ext'_iff
{R : Type u}
{M : Type v}
{ι : Type x}
[semiring R]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[fintype ι]
[decidable_eq ι]
[add_comm_monoid M]
[module R M]
{f g : (Π (i : ι), φ i) →ₗ[R] M} :
f = g ↔ ∀ (i : ι), f.comp (linear_map.single i) = g.comp (linear_map.single i)
def
linear_map.infi_ker_proj_equiv
(R : Type u)
{ι : Type x}
[semiring R]
(φ : ι → Type i)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
{I J : set ι}
[decidable_pred (λ (i : ι), i ∈ I)]
(hd : disjoint I J)
(hu : set.univ ⊆ I ∪ J) :
If I and J are disjoint index sets, the product of the kernels of the Jth projections of
φ is linearly equivalent to the product over I.
Equations
- linear_map.infi_ker_proj_equiv R φ hd hu = linear_equiv.of_linear (linear_map.pi (λ (i : ↥I), (linear_map.proj ↑i).comp (⨅ (i : ι) (H : i ∈ J), (linear_map.proj i).ker).subtype)) (linear_map.cod_restrict (⨅ (i : ι) (H : i ∈ J), (linear_map.proj i).ker) (linear_map.pi (λ (i : ι), dite (i ∈ I) (λ (h : i ∈ I), linear_map.proj ⟨i, h⟩) (λ (h : i ∉ I), 0))) _) _ _
def
linear_map.diag
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[decidable_eq ι]
(i j : ι) :
diag i j is the identity map if i = j. Otherwise it is the constant 0 map.
Equations
- linear_map.diag i j = function.update 0 i linear_map.id j
theorem
linear_map.update_apply
{R : Type u}
{M₂ : Type w}
{ι : Type x}
[semiring R]
[add_comm_monoid M₂]
[module R M₂]
{φ : ι → Type i}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[decidable_eq ι]
(f : Π (i : ι), M₂ →ₗ[R] φ i)
(c : M₂)
(i j : ι)
(b : M₂ →ₗ[R] φ i) :
⇑(function.update f i b j) c = function.update (λ (i : ι), ⇑(f i) c) i (⇑b c) j
def
submodule.pi
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type u_1}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(I : set ι)
(p : Π (i : ι), submodule R (φ i)) :
submodule R (Π (i : ι), φ i)
A version of set.pi for submodules. Given an index set I and a family of submodules
p : Π i, submodule R (φ i), pi I s is the submodule of dependent functions f : Π i, φ i
such that f i belongs to p a whenever i ∈ I.
@[simp]
theorem
submodule.mem_pi
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type u_1}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
{I : set ι}
{p : Π (i : ι), submodule R (φ i)}
{x : Π (i : ι), φ i} :
x ∈ submodule.pi I p ↔ ∀ (i : ι), i ∈ I → x i ∈ p i
@[simp]
theorem
submodule.coe_pi
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type u_1}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
{I : set ι}
{p : Π (i : ι), submodule R (φ i)} :
↑(submodule.pi I p) = I.pi (λ (i : ι), ↑(p i))
theorem
submodule.binfi_comap_proj
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type u_1}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
{I : set ι}
{p : Π (i : ι), submodule R (φ i)} :
(⨅ (i : ι) (H : i ∈ I), submodule.comap (linear_map.proj i) (p i)) = submodule.pi I p
theorem
submodule.infi_comap_proj
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type u_1}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
{p : Π (i : ι), submodule R (φ i)} :
(⨅ (i : ι), submodule.comap (linear_map.proj i) (p i)) = submodule.pi set.univ p
theorem
submodule.supr_map_single
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type u_1}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
{p : Π (i : ι), submodule R (φ i)}
[decidable_eq ι]
[fintype ι] :
(⨆ (i : ι), submodule.map (linear_map.single i) (p i)) = submodule.pi set.univ p
def
linear_equiv.Pi_congr_right
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type u_1}
{ψ : ι → Type u_2}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[Π (i : ι), add_comm_monoid (ψ i)]
[Π (i : ι), module R (ψ i)]
(e : Π (i : ι), φ i ≃ₗ[R] ψ i) :
Combine a family of linear equivalences into a linear equivalence of pi-types.
This is equiv.Pi_congr_right as a linear_equiv
@[simp]
theorem
linear_equiv.Pi_congr_right_apply
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type u_1}
{ψ : ι → Type u_2}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[Π (i : ι), add_comm_monoid (ψ i)]
[Π (i : ι), module R (ψ i)]
(e : Π (i : ι), φ i ≃ₗ[R] ψ i)
(f : Π (i : ι), φ i)
(i : ι) :
⇑(linear_equiv.Pi_congr_right e) f i = ⇑(e i) (f i)
@[simp]
theorem
linear_equiv.Pi_congr_right_refl
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type u_1}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)] :
linear_equiv.Pi_congr_right (λ (j : ι), linear_equiv.refl R (φ j)) = linear_equiv.refl R (Π (i : ι), φ i)
@[simp]
theorem
linear_equiv.Pi_congr_right_symm
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type u_1}
{ψ : ι → Type u_2}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[Π (i : ι), add_comm_monoid (ψ i)]
[Π (i : ι), module R (ψ i)]
(e : Π (i : ι), φ i ≃ₗ[R] ψ i) :
(linear_equiv.Pi_congr_right e).symm = linear_equiv.Pi_congr_right (λ (i : ι), (e i).symm)
@[simp]
theorem
linear_equiv.Pi_congr_right_trans
{R : Type u}
{ι : Type x}
[semiring R]
{φ : ι → Type u_1}
{ψ : ι → Type u_2}
{χ : ι → Type u_3}
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
[Π (i : ι), add_comm_monoid (ψ i)]
[Π (i : ι), module R (ψ i)]
[Π (i : ι), add_comm_monoid (χ i)]
[Π (i : ι), module R (χ i)]
(e : Π (i : ι), φ i ≃ₗ[R] ψ i)
(f : Π (i : ι), ψ i ≃ₗ[R] χ i) :
(linear_equiv.Pi_congr_right e).trans (linear_equiv.Pi_congr_right f) = linear_equiv.Pi_congr_right (λ (i : ι), (e i).trans (f i))
def
linear_equiv.Pi_congr_left'
(R : Type u)
{ι : Type x}
{ι' : Type x'}
[semiring R]
(φ : ι → Type u_1)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(e : ι ≃ ι') :
Transport dependent functions through an equivalence of the base space.
This is equiv.Pi_congr_left' as a linear_equiv.
Equations
- linear_equiv.Pi_congr_left' R φ e = {to_fun := (equiv.Pi_congr_left' φ e).to_fun, map_add' := _, map_smul' := _, inv_fun := (equiv.Pi_congr_left' φ e).inv_fun, left_inv := _, right_inv := _}
@[simp]
theorem
linear_equiv.Pi_congr_left'_symm_apply
(R : Type u)
{ι : Type x}
{ι' : Type x'}
[semiring R]
(φ : ι → Type u_1)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(e : ι ≃ ι')
(ᾰ : Π (b : ι'), φ (⇑(e.symm) b))
(a : ι) :
@[simp]
theorem
linear_equiv.Pi_congr_left'_apply
(R : Type u)
{ι : Type x}
{ι' : Type x'}
[semiring R]
(φ : ι → Type u_1)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(e : ι ≃ ι')
(ᾰ : Π (a : ι), φ a)
(b : ι') :
⇑(linear_equiv.Pi_congr_left' R φ e) ᾰ b = ᾰ (⇑(e.symm) b)
def
linear_equiv.Pi_congr_left
(R : Type u)
{ι : Type x}
{ι' : Type x'}
[semiring R]
(φ : ι → Type u_1)
[Π (i : ι), add_comm_monoid (φ i)]
[Π (i : ι), module R (φ i)]
(e : ι' ≃ ι) :
Transporting dependent functions through an equivalence of the base, expressed as a "simplification".
This is equiv.Pi_congr_left as a linear_equiv
Equations
- linear_equiv.Pi_congr_left R φ e = (linear_equiv.Pi_congr_left' R φ e.symm).symm
def
linear_equiv.pi_ring
(R : Type u)
(M : Type v)
(ι : Type x)
[semiring R]
(S : Type u_4)
[fintype ι]
[decidable_eq ι]
[semiring S]
[add_comm_monoid M]
[module R M]
[module S M]
[smul_comm_class R S M] :
Linear equivalence between linear functions Rⁿ → M and Mⁿ. The spaces Rⁿ and Mⁿ
are represented as ι → R and ι → M, respectively, where ι is a finite type.
This as an S-linear equivalence, under the assumption that S acts on M commuting with R.
When R is commutative, we can take this to be the usual action with S = R.
Otherwise, S = ℕ shows that the equivalence is additive.
See note [bundled maps over different rings].
Equations
- linear_equiv.pi_ring R M ι S = (linear_map.lsum R (λ (i : ι), R) S).symm.trans (linear_equiv.Pi_congr_right (λ (i : ι), linear_map.ring_lmap_equiv_self R M S))
@[simp]
theorem
linear_equiv.pi_ring_apply
{R : Type u}
{M : Type v}
{ι : Type x}
[semiring R]
(S : Type u_4)
[fintype ι]
[decidable_eq ι]
[semiring S]
[add_comm_monoid M]
[module R M]
[module S M]
[smul_comm_class R S M]
(f : (ι → R) →ₗ[R] M)
(i : ι) :
⇑(linear_equiv.pi_ring R M ι S) f i = ⇑f (pi.single i 1)
@[simp]
theorem
linear_equiv.pi_ring_symm_apply
{R : Type u}
{M : Type v}
{ι : Type x}
[semiring R]
(S : Type u_4)
[fintype ι]
[decidable_eq ι]
[semiring S]
[add_comm_monoid M]
[module R M]
[module S M]
[smul_comm_class R S M]
(f : ι → M)
(g : ι → R) :
def
linear_equiv.sum_arrow_lequiv_prod_arrow
(α : Type u_1)
(β : Type u_2)
(R : Type u_3)
(M : Type u_4)
[semiring R]
[add_comm_monoid M]
[module R M] :
equiv.sum_arrow_equiv_prod_arrow as a linear equivalence.
Equations
- linear_equiv.sum_arrow_lequiv_prod_arrow α β R M = {to_fun := (equiv.sum_arrow_equiv_prod_arrow α β M).to_fun, map_add' := _, map_smul' := _, inv_fun := (equiv.sum_arrow_equiv_prod_arrow α β M).inv_fun, left_inv := _, right_inv := _}
@[simp]
theorem
linear_equiv.sum_arrow_lequiv_prod_arrow_apply_fst
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[module R M]
{α : Type u_1}
{β : Type u_2}
(f : α ⊕ β → M)
(a : α) :
(⇑(linear_equiv.sum_arrow_lequiv_prod_arrow α β R M) f).fst a = f (sum.inl a)
@[simp]
theorem
linear_equiv.sum_arrow_lequiv_prod_arrow_apply_snd
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[module R M]
{α : Type u_1}
{β : Type u_2}
(f : α ⊕ β → M)
(b : β) :
(⇑(linear_equiv.sum_arrow_lequiv_prod_arrow α β R M) f).snd b = f (sum.inr b)
@[simp]
theorem
linear_equiv.sum_arrow_lequiv_prod_arrow_symm_apply_inl
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[module R M]
{α : Type u_1}
{β : Type u_2}
(f : α → M)
(g : β → M)
(a : α) :
⇑((linear_equiv.sum_arrow_lequiv_prod_arrow α β R M).symm) (f, g) (sum.inl a) = f a
@[simp]
theorem
linear_equiv.sum_arrow_lequiv_prod_arrow_symm_apply_inr
{R : Type u}
{M : Type v}
[semiring R]
[add_comm_monoid M]
[module R M]
{α : Type u_1}
{β : Type u_2}
(f : α → M)
(g : β → M)
(b : β) :
⇑((linear_equiv.sum_arrow_lequiv_prod_arrow α β R M).symm) (f, g) (sum.inr b) = g b