Stratified topological spaces

Stream: Is there code for X?

[Matthew Ballard]

What are people’s opinions about

import Mathlib.Topology.Order.UpperLowerSetTopology

/-!
# Basic theory of stratified topological spaces.

-/

universe u v

open Topology

namespace Topology

/-- For a stratification on a topological space we bundle a poset `I` with a continuous function to
the upper set topology on `I` indexing the strata. -/
structure Stratification (X : Type u) [TopologicalSpace X] where
  I : Type v
  [order : Preorder I]
  strata : C(X, WithUpperSet I)

instance instPreOrder {X : Type u}  [TopologicalSpace X] (S : Stratification X) : Preorder S.I := S.order

end Topology

namespace Stratification

open Set WithUpperSet

variable {X : Type u} [TopologicalSpace X] (S : Stratification X)

/-- The stratum of a corresponding to the upper set of `v` in indexing set `I`. -/
def stratum (v : S.I) : Set X := S.strata ⁻¹' (ofUpperSet ⁻¹' (Ici v))

end Stratification

[Adam Topaz]

docs#WithUpperSet

[Adam Topaz]

Is this related to how Barwick-Glasman-Haine define stratified homotopy types?

[Adam Topaz]

Yes, see def 1.2.1 in Exodromy

[Johan Commelin]

Does it make sense to have the poset as parameter?

[Johan Commelin]

Instead of as field

[Johan Commelin]

Also, I conjecture that hard-coding WithUpperSet in the defn will cause issues down the road. I suggest replacing the preorder with an Alexandrov topological space instead

[Adam Topaz]

It may be cumbersome to talk about morphisms between stratified spaces if the poset/alexandrov space unbundled.

[Adam Topaz]

But if you ever need to talk about morphisms of stratified spaces over the same poset, then this is essentially the only way

[Johan Commelin]

Adam Topaz said:

It may be cumbersome to talk about morphisms between stratified spaces if the poset/alexandrov space unbundled.

Can't we follow the semilinear-map approach? That works quite smoothly after the initial setup

[Matthew Ballard]

Ok, I think that makes sense. I’ll see if it is as straightforward as it seems. The other issue was whether to used bundled or unbundled continuous functions.

[Adam Topaz]

Note that setting up semilinear maps properly was quite a significant project all in itself.

[Adam Topaz]

https://arxiv.org/abs/2202.05360

[Johan Commelin]

Yes, indeed! But I'm hoping that copying that approach to an analogous setting will be quite a bit easier.

[Adam Topaz]

I agree. I don''t think it would require any new ideas per se, but rather that one has to set up the typeclasses carefully.

[Johan Commelin]

Also, in this case we don't have to worry about refactoring a large existing library.

[Adam Topaz]

yeah good point