[ooovi]

attempting to remove bundled convex sets. wip, some renaming and moving of lemmas needs to be done. wdyt?

• IsFaceOf is just extreme subsets
• the lattice Face requires both face and faced set to be convex (otherwise its not very interesting and we'd need to define this lattice anyways for homogenization)
• homogenize and dehomognize are both defined on general sets. in particular, we need the assumption of convexity for dehomogenize ℋ (homogenize ℋ P) = P. the order equivalence becomes

  {s : Set A // IsConvexSet R s} ≃o Set.Iic ℋ.weight.positive
  

[martinwintermath]

Suggested change

	structure Face {p : Set M} (P : IsConvexSet R p) where
	structure Face {p : Set M} where

This seems unneccesary.

[ooovi]

we don't get reflexivity if p is not convex

[martinwintermath]

Then we need to assume convexity in the reflexivity lemma

[ooovi]

we do assume it for IsFaceOf.refl, but to define the lattice structure i think we don't want to carry the assumption separately. otherwise we'd need stuff like

instance (h : IsConvexSet R P) : OrderTop (Face P) where

and everything gets non-inferrable

[ooovi]

sorry i didnt see my own response below ^^

[martinwintermath]

Suggested change

	/-- A face of a convex set `P`. Represents the face lattice of `P`. -/
	/-- A face of a set `P`. This type also represents the face lattice of `P`. -/

[ooovi]

well we are, but how will we define the lattice on `Face` if top and sinf have an additional assumption?

…

On 22 October 2026 12:26:58 CEST, "M. Winter" ***@***.***> wrote: @martinwintermath commented on this pull request. > /-- A face of a convex set `P`. Represents the face lattice of `P`. -/ -structure Face (P : ConvexSet R M) extends toConvexSet : ConvexSet R M where - isFaceOf : IsFaceOf toConvexSet P ***@***.*** +structure Face {p : Set M} (P : IsConvexSet R p) where Then we need to assume convexity in the reflexivity lemma -- Reply to this email directly or view it on GitHub: #112 (comment) You are receiving this because you authored the thread. Message ID: ***@***.***>

[martinwintermath]

well we are, but how will we define the lattice on Face if top and sinf have an additional assumption?

I don't know. This is a good question and a challenge. Maybe this indicates that bundled objects should be built on other bundled objects, that is, IsFaceOf can be on Set, but Face should be on ConvexSet. I have no idea. Let's maybe focus on IsFaceOf for now and lets see how far we get with it?

@YaelDillies Any ideas? It seems we can't do with bundles and we can't do without.

[martinwintermath]

Here is a stupid solution: we define IsFaceOf R F C so that F is a face of C if either F=C or F is a face of C in the usual sense. Feels hacked though.

Update. here is a less hacked way: we know how to define faces if C is convex. For non-convex sets C we can define faces as intersections of C with faces of the convex hull of C. And the more I think about this, I feel that the current definition as another a shortcoming: think of a U shaped set. Let a and b be the two end points of the U. With the current definition a and b would be faces, but (a union b) is not, even though it is the natural join (note that I do not say that in general unions are faces, but here it should be).

[ooovi]

Here is a stupid solution: we define IsFaceOf R F C so that F is a face of C if either F=C or F is a face of C in the usual sense. Feels hacked though.

Update. here is a less hacked way: we know how to define faces if C is convex. For non-convex sets C we can define faces as intersections of C with faces of the convex hull of C. And the more I think about this, I feel that the current definition as another a shortcoming: think of a U shaped set. Let a and b be the two end points of the U. With the current definition a and b would be faces, but (a union b) is not, even though it is the natural join (note that I do not say that in general unions are faces, but here it should be).

i think your new definition also has oddities. for instance, one might expect the straight line inside the U to be a face. like the black line in this plot which i got from this stackexchange question.

i thought we decided somewhere to not try and define faces for non-convex sets?

what do you mean by "Let's maybe focus on IsFaceOf for now and lets see how far we get with it?"? we will need the bundled face for the iso to pointed cone faces, so i think we should keep it.

what is the problem you see with assuming convexity for the bundled type?

[martinwintermath]

i think your new definition also has oddities. for instance, one might expect the straight line inside the U to be a face. like the black line in this plot which i got from this stackexchange question.

This was already a problem for the current definition. And I do not consider this line as a face in the convex sets anyway.

i thought we decided somewhere to not try and define faces for non-convex sets?

Yes, we don't. We try to find a definition on all sets that behaves as expected on convex sets.
Forget the example with the U, let's not think about faces of non-convex sets.
Priority is something that works well on convex sets while the definition does not assume it.

what do you mean by "Let's maybe focus on IsFaceOf for now and lets see how far we get with it?"? we will need the bundled face for the iso to pointed cone faces, so i think we should keep it.

Do we though? We have lemmas that transfer IsFaceOf back and forth, right? Let's talk on Zulip about the next steps, because I might just not know what your plan is.

what is the problem you see with assuming convexity for the bundled type?

• It is counterintuitive: IsFaceOf assumes no convexity but Face does even though it is supposed to be just an encapsulation of the former.
• it seems not quite so nice to use.
• the only (really urgent) problem that we have when we do not assume convexity is the top face, which is easy to solve
• the "lets take faces of the convex hull" definition appears to me now as the more correct one without me having a better argument at this time.

But again, we need to be open for the possibility that Face might actually need ConvexSet. We can't know until we try.

[martinwintermath]

We have at least the following options how to proceed:

• we redefine IsFaceOf in a way so that the full set is always a face of itself. I already gave above my favorite way to do this: faces of sets are faces of the convex hull intersected with the set. Then defining Face on this notion of IsFaceOf gives the correct lattice structure.
• Let Face be defined on ConvexSet instead of Face. This is not entirely unreasonable because then bundled objects are defined on bundled objects, and on the linear side we also have IsFaceOf defined on the convex cone object.
• revive bundled ConvexSet as the main player in convex geometry instead of Set. Then IsFaceOf too is defined on ConvexSet (and likewise all notions we define in future, such as tangent cones, recession cones, interior, etc). I previously disliked this because it brought us into "coercion hell", but maybe this is a problem because we did not have the right ideas yet, or did the setup wrong. Hard to tell.

I cannot foresee the ramifications of either choice and therefore think we need to pick one for now and see what happens (and be willing to adjust when it turns out necessary).

The redefinition of IsFaceOf is probably a good idea independent of what we do with Face. And if we do so, we may as well pick option 1 above.

[YaelDillies]

Option 1 looks most sensible to me right now