Isomorphisms of simplicial complexes

Stream: new members

[Garett Cunningham]

Hello! I'm orienting myself with Lean 4/mathlib this summer through a project on abstract simplicial complexes. Hoping for some pointers for a canonical way to solve the following issue:

I'm writing some additions to Geometry.SimplicialComplex. Specifically, I'm currently trying to get a plausibly correct notion of isomorphism between two simplicial complexes. We'd like to follow the usual textbook definition: some pair of simplicial maps that are mutually inverses. Intuitively, an isomorphism should be a relabeling of vertices.

It seems reasonable to want the relation to have type signature

Geometry.SimplicialComplex 𝕜 E -> Geometry.SimplicialComplex 𝕜 F -> Prop

This should also behave like an honest-to-God isomorphism/equivalence relation, wherein we ideally don't need to re-implement things that already exist. There are some practical reasons to want this for operations like joins. But, now we run into the issue of what structure to target:

• Equivalence is a no-go, since it requires a relation with type signature ⍺ -> ⍺ -> Prop.
  • One could likely use DirectSum to make this work on the level of inclusions, which seems painful.
• EquivLike is almost plausible, except it wants Geometry.SimplicialComplex to be a class, not a structure.
  • Simplicial isomorphism really only needs to satisfy the inverse conditions on the set of vertices. In general, a bijection between E and F might not exist. Take two finite abelian groups of different sizes as an artificial example.
  • So, extending E ⋍ F would seemingly require some additional axiom like total : ∀ x : E, {x} ∈ faces to make sense, given the above point. Attempting to write definitions of subdivisions seems difficult in this case, especially if the complex is finite.

This is where my lack of familiarity wrt mathlib4 comes in. Are there any existing features that one should target in this case? Any canonical/clever ways to (ab)use the above that I'm missing? Questions about or poking holes in the above logic is very much welcome. Thanks!

[Garett Cunningham]

Sorry to add to this, but would still love to hear some suggestions. Unfortunately, the whims of funding and day-to-day responsibilities demand that forward progress be made, so I've elected to circumvent mathlib for the moment, since it seems to be the path of least resistance. I'm willing to accept this as technical debt if a better solution is proposed and fix code off the clock.

I've defined a structure for simplicial maps and a collection of propositions to capture the same effect:

variable  {X : Geometry.SimplicialComplex 𝕜 E} {Y : Geometry.SimplicialComplex 𝕜 F}

structure SimplicialMap where
  mk ::
    map : E -> F
    is_simplicial : ∀ s ∈ X.faces, Finset.image f s ∈ Y.faces

def isSimplicialInverse (f : SimplicialMap X Y) (g : SimplicialMap Y X) : Prop :=
  Set.EqOn (g.map ∘ f.map) id X.vertices ∧ Set.EqOn (f.map ∘ g.map) id Y.vertices

def isSimpliciallyIso (X : Geometry.SimplicialComplex 𝕜 E) (Y : Geometry.SimplicialComplex 𝕜 F) : Prop :=
  ∃ (f : SimplicialMap X Y) (g : SimplicialMap Y X), isSimplicialInverse f g
infixr:50 " ≅ " => isSimpliciallyIso

This gives the desired type signature

Geometry.SimplicialComplex 𝕜 E -> Geometry.SimplicialComplex 𝕜 F -> Prop

at the cost of working somewhat independent of mathlib. It seems a shame to rely on a workaround like this, so I would still love to hear any suggestions. Thanks!