#
Homotopy Type Theory
bilinear function > history (changes)

Showing changes from revision #5 to #6:
Added | ~~Removed~~ | ~~Chan~~ged

## Definiton

< bilinear function

~~Let ~~

~~$A$~~~~, ~~~~$B$~~~~, and ~~~~$C$~~~~ be ~~~~abelian group~~~~s, and let ~~~~$f:A \times B \to C$~~~~ be a function from the product type of ~~~~$A$~~~~ and ~~~~$B$~~~~ to ~~~~$C$~~~~. Let us define the types~~~~
~~$isLeftDistributive(f) \coloneqq \prod_{a:A} \prod_{b:B} \prod_{c:B} f(a, b +_B c) = f(a, b) +_C f(a, c)$

$isRightDistributive(f) \coloneqq \prod_{a:A} \prod_{b:A} \prod_{c:B} f(a +_A b, c) = f(a, c) +_C f(b, c)$

$isBilinear(f) \coloneqq isLeftDistributive(f) \times isRightDistributive(f)$

~~
~~$f$ is a **bilinear function** if the type $isBilinear(f)$ has a term.

~~
~~We could define the type of all bilinear functions for abelian groups $A$, $B$, and $C$ as

~~
~~$BilinearFunc(A, B, C) \prod_{f:A \times B \to C} isBilinear(f)$

~~
~~## See also

~~
~~~~
~~
Last revised on June 17, 2022 at 20:35:01.
See the history of this page for a list of all contributions to it.