Homotopy Type Theory trilinear function > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

Definiton

< multilinear function

Let

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

isLeftDistributive(f) a:A b:B c:C d:Cf(a,b,c+ Cd)=f(a,b,c)+ Df(a,b,d)isLeftDistributive(f) \coloneqq \prod_{a:A} \prod_{b:B} \prod_{c:C} \prod_{d:C} f(a, b, c +_C d) = f(a, b, c) +_D f(a, b, d)
isMiddleDistributive(f) a:A b:B c:B d:Cf(a,b+ Bc,d)=f(a,b,d)+ Df(a,c,d)isMiddleDistributive(f) \coloneqq \prod_{a:A} \prod_{b:B} \prod_{c:B} \prod_{d:C} f(a, b +_B c, d) = f(a, b, d) +_D f(a, c, d)
isRightDistributive(f) a:A b:A c:B d:Cf(a+ Ab,c,d)=f(a,c,d)+ Df(b,c,d)isRightDistributive(f) \coloneqq \prod_{a:A} \prod_{b:A} \prod_{c:B} \prod_{d:C} f(a +_A b, c, d) = f(a, c, d) +_D f(b, c, d)
isTrilinear(f)isLeftDistributive(f)×isMiddleDistributive(f)×isRightDistributive(f)isTrilinear(f) \coloneqq isLeftDistributive(f) \times isMiddleDistributive(f) \times isRightDistributive(f)

ff is a trilinear function if the type isTrilinear(f)isTrilinear(f) has a term.

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

TrilinearFunc(A,B,C,D) f:A×B×CDisTrilinear(f)TrilinearFunc(A, B, C, D) \prod_{f:A \times B \times C \to D} isTrilinear(f)

See also

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