Zulip Chat Archive
Stream: Is there code for X?
Topic: Dimension of an affine space
Yaël Dillies (Jun 09 2022 at 23:08):
There doesn't seem to be anything about the dimension of an affine space. Is it missing or are we meant to use docs#finite_dimensional.finrank?
Hanting Zhang (Jun 09 2022 at 23:13):
Right now, we just refer to the dimension of the underlying space. Not sure if we should consider adding dimension for affine spaces
Yaël Dillies (Jun 09 2022 at 23:15):
Okay, but how do I talk about the dimension of an affine subspace then? Do I talk about the dimension of its docs#affine_subspace.direction?
Eric Wieser (Jun 09 2022 at 23:15):
That sounds very reasonable to me
Yaël Dillies (Jun 09 2022 at 23:16):
Is there a precedent or am I the first one caring about the dimension of an affine subspace?
Hanting Zhang (Jun 09 2022 at 23:17):
(Looking through his code) I'm guessing @Joseph Myers thought about this a bit and chose to go with just using the dimension of the underlying space
Hanting Zhang (Jun 09 2022 at 23:20):
It's not too awkward the way it is right now. If we were to add affine space dimensions then all the API would have to be ported over, and most results are really just results about the underlying spaces
Joseph Myers (Jun 09 2022 at 23:34):
Yes, using dimensions of underlying spaces (and direction in the subspace case) avoids the need for extra API by allowing all the API for dimension and finrank to be used directly. Strictly there is an argument for a definition of dimension for affine subspaces in order to give the empty affine subspace dimension (using the dimension of the direction gives it dimension 0, like affine subspaces with a single point), but I doubt that would be particularly useful in practice.
Joseph Myers (Jun 09 2022 at 23:39):
Also everything we currently have about dimensions in affine spaces is for the finite-dimensional case only (finrank instead of rank), but no doubt some of it could be generalized to infinite dimensions if desired.
Adam Topaz (Jun 10 2022 at 02:32):
It's time to add an abstract notion of dimension using matroids and/or combinatorial geometries.
Yaël Dillies (Jun 10 2022 at 07:16):
I would certainly be interested in this! We had an external matroid project, by @Peter Nelson if I remember correctly?
Adam Topaz (Jun 10 2022 at 14:23):
What's the status on closure operators?
Yaël Dillies (Jun 10 2022 at 22:00):
I'm quite unhappy with the current API, and I think we should have interior operators to help dualize results.
Yaël Dillies (Jun 10 2022 at 22:05):
I would like closure operators to be galois connections in the special case of β = subtype p where p : α → Prop.
Last updated: Dec 20 2023 at 11:08 UTC