Zulip Chat Archive

Stream: general

Topic: bicompr for linear maps

Filippo A. E. Nuccio (Jun 29 2021 at 11:37):

The definition of bicompr I find is

def bicompr (f : γ  δ) (g : α  β  γ) (a b) :=
f (g a b)

and it allows to compose an unary function f with a binary function g. I wonder if we have the same for more advanced morphisms, like

def foo (f : P →ₗ[R] Q) (g: M →ₗ[R] N →ₗ[R] P) : (M →ₗ[R] N →ₗ[R] Q) :=

for linear maps (or for other structures).

Filippo A. E. Nuccio (Jun 29 2021 at 11:47):

Oh yes, I found it: linear_map.compr₂.

Last updated: Aug 03 2023 at 10:10 UTC