What would synthetic linear algebra look like?
up vote
2
down vote
favorite
I'm aware of synthetic mathematical fields like synthetic differential geometry and synthetic topology where the area is developed axiomatically rather than deriving everything analytically from a foundation of sets.
So I'm wondering if a synthetic linear algebra would make sense or if that's trivial. Is linear type theory essentially the same thing?
linear-algebra category-theory type-theory synthetic-differential-geometry
asked Nov 23 at 21:01
Brandon Brown
1887
add a comment |
up vote
2
down vote
favorite
I'm aware of synthetic mathematical fields like synthetic differential geometry and synthetic topology where the area is developed axiomatically rather than deriving everything analytically from a foundation of sets.
So I'm wondering if a synthetic linear algebra would make sense or if that's trivial. Is linear type theory essentially the same thing?
linear-algebra category-theory type-theory synthetic-differential-geometry
asked Nov 23 at 21:01
Brandon Brown
1887
1
= working in an abelian category with a bunch of nice properties?
– darij grinberg
Nov 23 at 21:15
@darij: that captures "additive" behavior but not "multiplicative" behavior (e.g. determinants). We really want to be working in a symmetric monoidal abelian category. See mathoverflow.net/a/243534/290 for more details.
– Qiaochu Yuan
Nov 24 at 11:59
add a comment |
up vote
2
down vote
favorite
up vote
2
down vote
favorite
I'm aware of synthetic mathematical fields like synthetic differential geometry and synthetic topology where the area is developed axiomatically rather than deriving everything analytically from a foundation of sets.
So I'm wondering if a synthetic linear algebra would make sense or if that's trivial. Is linear type theory essentially the same thing?
linear-algebra category-theory type-theory synthetic-differential-geometry
asked Nov 23 at 21:01
Brandon Brown
1887
I'm aware of synthetic mathematical fields like synthetic differential geometry and synthetic topology where the area is developed axiomatically rather than deriving everything analytically from a foundation of sets.
So I'm wondering if a synthetic linear algebra would make sense or if that's trivial. Is linear type theory essentially the same thing?
linear-algebra category-theory type-theory synthetic-differential-geometry
linear-algebra category-theory type-theory synthetic-differential-geometry
asked Nov 23 at 21:01
Brandon Brown
1887
asked Nov 23 at 21:01
Brandon Brown
1887
asked Nov 23 at 21:01
Brandon Brown
1887
asked Nov 23 at 21:01
Brandon Brown
1887
asked Nov 23 at 21:01
Brandon Brown
1887
1887
1
= working in an abelian category with a bunch of nice properties?
– darij grinberg
Nov 23 at 21:15
@darij: that captures "additive" behavior but not "multiplicative" behavior (e.g. determinants). We really want to be working in a symmetric monoidal abelian category. See mathoverflow.net/a/243534/290 for more details.
– Qiaochu Yuan
Nov 24 at 11:59
add a comment |
1
= working in an abelian category with a bunch of nice properties?
– darij grinberg
Nov 23 at 21:15
@darij: that captures "additive" behavior but not "multiplicative" behavior (e.g. determinants). We really want to be working in a symmetric monoidal abelian category. See mathoverflow.net/a/243534/290 for more details.
– Qiaochu Yuan
Nov 24 at 11:59
1
1
= working in an abelian category with a bunch of nice properties?
– darij grinberg
Nov 23 at 21:15
= working in an abelian category with a bunch of nice properties?
– darij grinberg
Nov 23 at 21:15
@darij: that captures "additive" behavior but not "multiplicative" behavior (e.g. determinants). We really want to be working in a symmetric monoidal abelian category. See mathoverflow.net/a/243534/290 for more details.
– Qiaochu Yuan
Nov 24 at 11:59
@darij: that captures "additive" behavior but not "multiplicative" behavior (e.g. determinants). We really want to be working in a symmetric monoidal abelian category. See mathoverflow.net/a/243534/290 for more details.
– Qiaochu Yuan
Nov 24 at 11:59
add a comment |
1 Answer
1
active
oldest
votes
up vote
3
down vote
accepted
J.N. Oliveira and friends have a number of papers that give an axiomatisation of linear algebra.
The important observation is that matrices cannot be arbitrarily multiplied and as such do not form monoids, so the traditional mathematical approach of using monoids, groups, rings, fields does not easily apply here.
Matrices have types, or dimensions, that specify when they can be multiplied.
Slogan: Categories are Typed Monoids!
One rather accessible paper might well be Matrices As Arrows! A Biproduct Approach to Typed Linear Algebra, or see http://www4.di.uminho.pt/~jno/html/jnopub.html for more similar such papers.
The abstract of the mentioned paper includes:
Motivated by the need to formalize generation of fast running code for linear algebra applications, we show how an index-free, calculational approach to matrix algebra can be developed by regarding matrices as morphisms of a category with biproducts. This shifts the traditional view of matrices as indexed structures to a type-level perspective [...]
From errant attempts to learn how particular products and coproducts emerge from biproducts, we not only rediscovered block-wise matrix combinators but also found a way of addressing other operations calculationally such as e.g. Gaussian elimination. A strategy for addressing vectorization along the same lines is also given.
answered Nov 24 at 11:44
Musa Al-hassy
1,2971711
add a comment |
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
3
down vote
accepted
J.N. Oliveira and friends have a number of papers that give an axiomatisation of linear algebra.
The important observation is that matrices cannot be arbitrarily multiplied and as such do not form monoids, so the traditional mathematical approach of using monoids, groups, rings, fields does not easily apply here.
Matrices have types, or dimensions, that specify when they can be multiplied.
Slogan: Categories are Typed Monoids!
One rather accessible paper might well be Matrices As Arrows! A Biproduct Approach to Typed Linear Algebra, or see http://www4.di.uminho.pt/~jno/html/jnopub.html for more similar such papers.
The abstract of the mentioned paper includes:
Motivated by the need to formalize generation of fast running code for linear algebra applications, we show how an index-free, calculational approach to matrix algebra can be developed by regarding matrices as morphisms of a category with biproducts. This shifts the traditional view of matrices as indexed structures to a type-level perspective [...]
From errant attempts to learn how particular products and coproducts emerge from biproducts, we not only rediscovered block-wise matrix combinators but also found a way of addressing other operations calculationally such as e.g. Gaussian elimination. A strategy for addressing vectorization along the same lines is also given.
answered Nov 24 at 11:44
Musa Al-hassy
1,2971711
add a comment |
up vote
3
down vote
accepted
J.N. Oliveira and friends have a number of papers that give an axiomatisation of linear algebra.
The important observation is that matrices cannot be arbitrarily multiplied and as such do not form monoids, so the traditional mathematical approach of using monoids, groups, rings, fields does not easily apply here.
Matrices have types, or dimensions, that specify when they can be multiplied.
Slogan: Categories are Typed Monoids!
One rather accessible paper might well be Matrices As Arrows! A Biproduct Approach to Typed Linear Algebra, or see http://www4.di.uminho.pt/~jno/html/jnopub.html for more similar such papers.
The abstract of the mentioned paper includes:
Motivated by the need to formalize generation of fast running code for linear algebra applications, we show how an index-free, calculational approach to matrix algebra can be developed by regarding matrices as morphisms of a category with biproducts. This shifts the traditional view of matrices as indexed structures to a type-level perspective [...]
From errant attempts to learn how particular products and coproducts emerge from biproducts, we not only rediscovered block-wise matrix combinators but also found a way of addressing other operations calculationally such as e.g. Gaussian elimination. A strategy for addressing vectorization along the same lines is also given.
answered Nov 24 at 11:44
Musa Al-hassy
1,2971711
add a comment |
up vote
3
down vote
accepted
up vote
3
down vote
accepted
J.N. Oliveira and friends have a number of papers that give an axiomatisation of linear algebra.
The important observation is that matrices cannot be arbitrarily multiplied and as such do not form monoids, so the traditional mathematical approach of using monoids, groups, rings, fields does not easily apply here.
Matrices have types, or dimensions, that specify when they can be multiplied.
Slogan: Categories are Typed Monoids!
One rather accessible paper might well be Matrices As Arrows! A Biproduct Approach to Typed Linear Algebra, or see http://www4.di.uminho.pt/~jno/html/jnopub.html for more similar such papers.
The abstract of the mentioned paper includes:
Motivated by the need to formalize generation of fast running code for linear algebra applications, we show how an index-free, calculational approach to matrix algebra can be developed by regarding matrices as morphisms of a category with biproducts. This shifts the traditional view of matrices as indexed structures to a type-level perspective [...]
From errant attempts to learn how particular products and coproducts emerge from biproducts, we not only rediscovered block-wise matrix combinators but also found a way of addressing other operations calculationally such as e.g. Gaussian elimination. A strategy for addressing vectorization along the same lines is also given.
answered Nov 24 at 11:44
Musa Al-hassy
1,2971711
J.N. Oliveira and friends have a number of papers that give an axiomatisation of linear algebra.
The important observation is that matrices cannot be arbitrarily multiplied and as such do not form monoids, so the traditional mathematical approach of using monoids, groups, rings, fields does not easily apply here.
Matrices have types, or dimensions, that specify when they can be multiplied.
Slogan: Categories are Typed Monoids!
One rather accessible paper might well be Matrices As Arrows! A Biproduct Approach to Typed Linear Algebra, or see http://www4.di.uminho.pt/~jno/html/jnopub.html for more similar such papers.
The abstract of the mentioned paper includes:
Motivated by the need to formalize generation of fast running code for linear algebra applications, we show how an index-free, calculational approach to matrix algebra can be developed by regarding matrices as morphisms of a category with biproducts. This shifts the traditional view of matrices as indexed structures to a type-level perspective [...]
From errant attempts to learn how particular products and coproducts emerge from biproducts, we not only rediscovered block-wise matrix combinators but also found a way of addressing other operations calculationally such as e.g. Gaussian elimination. A strategy for addressing vectorization along the same lines is also given.
answered Nov 24 at 11:44
Musa Al-hassy
1,2971711
answered Nov 24 at 11:44
Musa Al-hassy
1,2971711
answered Nov 24 at 11:44
Musa Al-hassy
1,2971711
answered Nov 24 at 11:44
Musa Al-hassy
1,2971711
1,2971711
add a comment |
add a comment |
Thanks for contributing an answer to Mathematics Stack Exchange!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
Use MathJax to format equations. MathJax reference.
To learn more, see our tips on writing great answers.
Some of your past answers have not been well-received, and you're in danger of being blocked from answering.
Please pay close attention to the following guidance:
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3010832%2fwhat-would-synthetic-linear-algebra-look-like%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
1
= working in an abelian category with a bunch of nice properties?
– darij grinberg
Nov 23 at 21:15
@darij: that captures "additive" behavior but not "multiplicative" behavior (e.g. determinants). We really want to be working in a symmetric monoidal abelian category. See mathoverflow.net/a/243534/290 for more details.
– Qiaochu Yuan
Nov 24 at 11:59