Homotopy Type Theory bilinear function > history (Rev #5)


Let AA, BB, and CC be abelian groups, and let f:A×BCf:A \times B \to C be a function from the product type of AA and BB to CC. Let us define the types

isLeftDistributive(f) a:A b:B c:Bf(a,b+ Bc)=f(a,b)+ Cf(a,c)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) a:A b:A c:Bf(a+ Ab,c)=f(a,c)+ Cf(b,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)isLeftDistributive(f)×isRightDistributive(f)isBilinear(f) \coloneqq isLeftDistributive(f) \times isRightDistributive(f)

ff is a bilinear function if the type isBilinear(f)isBilinear(f) has a term.

We could define the type of all bilinear functions for abelian groups AA, BB, and CC as

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

See also

Revision on June 15, 2022 at 22:29:01 by Anonymous?. See the history of this page for a list of all contributions to it.