Conversation
|
Could you coordinate this with @ooovi? Olivia is currently trying to remove bundled |
|
|
||
| variable {P : Set X} | ||
|
|
||
| theorem finite_vectorSpan (hP : IsPolytope R P) : Module.Finite R (vectorSpan R P) := by |
There was a problem hiding this comment.
I see here several useful intermediate/related results:
- the affine span of a polytope is finite dimensional.
- the vector span of the affine span of any set is the same as the vector span.
- the vector span of a finite dimensional affine space is finite dimensional.
| /-- The face lattice of a polytope as a graded order with grading given by the dimensions of | ||
| homogenization cones. | ||
| instance {P : Polytope R A} (F : Face (P : ConvexSet R A)) : | ||
| Module.Finite R (vectorSpan R (F.toConvexSet : Set A)) := |
There was a problem hiding this comment.
Okay, I read a bit more. I found it unnatural that there is vectorSpan all over the place. Why do you need that the vector span is finite dimensional? My guess is: because you use FiniteDimensional on the vectorSpan, because there is no analogue for affine spaces. Is this correct?
If so, this reinforced my believe the finite-dimensional issue needs to be solved first.
2 participants
No description provided.