Conversation
`finDim_affineSpan_eq_pred_finrank_homogenize` is the ingredient I need in the next PR adding grading of the polytope face lattice by dimension of the affine span of the face.
| @@ -0,0 +1,62 @@ | |||
| /- | |||
There was a problem hiding this comment.
This file and the one below are leanprover-community/mathlib4#43910
| variable {k} | ||
|
|
||
| theorem AffineIndepOn.ncard_eq_succ_finDim_affineSpan {s : Set P} (hai : AffineIndepOn k id s) | ||
| [hf : FiniteDimensional k (vectorSpan k s)] : s.ncard = (affineSpan k s).finDim.succ := by |
There was a problem hiding this comment.
We should first define FiniteDimensional on affine spaces directly. Going via the vector span is a hack.
There was a problem hiding this comment.
This is a bigger mathlib refactor than just this change, as it stands this is the canonical way to spell it.
There was a problem hiding this comment.
Isn't it just defining an affine version of FiniteDimensional in the same way as you just defined range for AffineMap by copying LinearMap.range?
There was a problem hiding this comment.
I guess it depends, do you expect this to be a def or an abbrev? Either way, the difference is that this file upstream already uses this pattern, as do others, so it would make more sense to do a targetted refactor rather then try to fix it here.
There was a problem hiding this comment.
Yeah, I am not happy that it got to mathlib in this form. To some degree I am okay with leaving it with the hack here if we are really sure we get rid of it sometime soon (we should add plenty comments to highlight that this is temporary). On the other hand, looking into your other PR, this seems to have further implications for how we write lemmas, and we should not let this get out of hand.
There was a problem hiding this comment.
Wouldn't this force us to require that the ambient space is finite dimensional rather than just the subspace we are looking at?
There was a problem hiding this comment.
If you use it, yes. You don't have to use it :P You should use a "the set is finite dim" variant. This is the distinction between Module.Finite and PointedCone.FinRank.
There was a problem hiding this comment.
Now the (draft) PR contains Affine.FinDim for sets. What are your thoughts. Will this work? Codex actually implemented some of your lemmas to demonstrate that it works :D
There was a problem hiding this comment.
The definition seems fine, it's an abbrev which I think is good. There's a lot of unnecessary copy-and-paste slop that is hard to wade through. I'm not sure why the use of this typeclass was changed from a typeclass parameter to an explicit hypothesis and another thing I find odd is that AffineSubspace.FinDim is defined using AffineSubspace.direction but Affine.FinDim is defined using vectorSpan, maybe it should be defined using FinDim (affineSpan R s).direction instead to match?
There was a problem hiding this comment.
These are good points. Let's continue discussing over there.
| theorem finDim_affineSpan_homogenize | ||
| (K : ConvexSet R A) [Module.Finite R (vectorSpan R (K : Set A))] : | ||
| (affineSpan R (homogenize W K : Set W)).finDim = | ||
| Order.succ (affineSpan R (K : Set A)).finDim := by |
There was a problem hiding this comment.
Something feels off here. We are we taking an affine span on the linear side. Should't we take the linear span and its rank? And also, we should (and probably already have) a notion of rank for a cone, and don't need to go via span.
And maybe we should have a notion dimension for sets (or at least convex sets) rather than needing to go via affineSpan.
There was a problem hiding this comment.
Fair point, I've update the PR to use PointedCone.finrank here instead. We have a rank/finrank defined for arbitrary Set (Polyhedral/Mathlib/LinearAlgebra/AffineSpace/Defs.lean) which I think is the wrong definition for mathlib, but moving this definition for ConvexSet seems reasonable. Shall I make redefining it and adding some basic API a precursor change to this one?
There was a problem hiding this comment.
@ooovi is currently removing bundled ConvexSet (at least all its uses for now). The fundamental object on the affine side will be Set. Why do you think this is wrong for mathlib?
There was a problem hiding this comment.
I think it's wrong unless we have a different name or assumptions for it, otherwise the graph of y = x^2 in ℝ^2 has dimension 2
There was a problem hiding this comment.
That would be intentional (at least from my side). It is (or should be) called Affine.dim as opposed to Manifold.dim or so. There can be several notions of dimension.
There was a problem hiding this comment.
I think Affine.dim would be fine, just not Set.rank/Set.finrank as it is now.
There was a problem hiding this comment.
Oh yeah, Set.rank/Set.finrank would be bad.
3 participants
finDim_affineSpan_eq_pred_finrank_homogenizeis the ingredient I need in the next PR (#108) adding grading of the polytope face lattice by dimension of the affine span of the face.