Unifying `fin (n+2)` and `fin (n+1)`

Stream: maths

[Ashwin Iyengar]

This doesn't quite work:

import algebraic_topology.simplicial_set
-- next 2 lines will be unnecessary once #6838 is merged
open sSet
open category_theory

open_locale simplicial

def horn_face (n : ℕ) (i j : fin (n+1)) (h: i ≠ j) : Λ[n,i].obj (opposite.op [n-1]) :=
⟨simplex_category.δ j, sorry⟩

and I think the reason is that I have j : fin (n+1) and the lemma simplex_category.δ is of the form def δ {m} (i : fin (m+2)): [m] ⟶ [m+1], but it won't unify m with n-1. I can't quite say simplex_category.δ (j : fin ((n-1)+2)) because this requires 1 ≤ n, which I don't want to assume (plus writing it that way seems awkward). Is there some simple way to deal with this sort of thing?

[Johan Commelin]

@Ashwin Iyengar This looks a lot like all the trouble that we had with (co)chain complexes...

[Johan Commelin]

In this case, can you assume i j : fin (n+2) instead, and write [n] in the conclusion?

[Ashwin Iyengar]

Yes ok that works in this case

[Johan Commelin]

I agree that this doesn't bode well...

[Ashwin Iyengar]

How did you deal with this issue for complexes?

[Johan Commelin]

In a mathematically very ugly way.

[Johan Commelin]

We now have a map $d_{i,j} \colon C_i \to C_j$, for all pairs $(i,j)$.

[Johan Commelin]

Plus an axiom that the map is zero if $j \ne i + 1$.

[Johan Commelin]

The benefit is that you now have a map $d_{i-1+1,i+1}$

[Johan Commelin]

And you can compose it with $d_{i-1,i-1+1}$ and get zero.

[Johan Commelin]

It took me a long time to cross the psychological barrier in front of this approach. But once I started playing with it, it worked very well.

[Ashwin Iyengar]

Hm the point being that $d_{i-1+1,i+1}$ is not definitionally equal to $d_{i,i+1}$?

[Ashwin Iyengar]

For simplicial sets it seems that the issue is that if you work with all morphisms in the simplex category then you have plenty of maps, but if you try to identify, say, maps from $\Lambda[n,i] \to S$ with an $n$-tuple in $S_{n-1}$ (which is useful in proofs (or maybe this is secretly a red herring?)) then things get weird

[Johan Commelin]

But does it work for n+1?

[Johan Commelin]

Because, if n = 0, what is $S_{-1}$?

[Ashwin Iyengar]

Ah good point

[Ashwin Iyengar]

Yes ok I'll carry on with $n+1$ and see if I get any more problems

[Kevin Buzzard]

It is difficult to parse the question about d_{i-1+1} because the two maps are terms of function types which are obviously equal to a mathematician but it's not so clear in lean. A proof that i=j gives you a map from A(i) to A(j), not an equality. If you try a rewrite then depending on the alignment of the stars it will either work or give a terrifying "motive is not type correct" error.

[Scott Morrison]

My hope, until it gets dashed, is actually that dependent typing will be our friend, not our enemy, for purely simplicial stuff...

[Adam Topaz]

Did this get resolved @Ashwin Iyengar ? Perhaps we need to redefine the horns and boundaries as certain colimits @Johan Commelin @Scott Morrison ?

[Ashwin Iyengar]

at the moment this compiles

@[simp]
lemma preorder_hom_of_mk_hom_of_preorder_hom {n m} {f : (fin (n+1)) →ₘ (fin (m+1))} :
  as_preorder_hom m (opposite.op [n]) (simplex_category.mk_hom f) = f := rfl

def horn_face (n : ℕ) (i j : fin (n+2)) (h: i ≠ j) : Λ[n+1,i].obj (opposite.op [n]) :=
⟨simplex_category.δ j,
  begin
    erw preorder_hom_of_mk_hom_of_preorder_hom,
    simp only [order_embedding.to_preorder_hom_coe, ne.def, set.union_singleton],
    rw [fin.range_succ_above j, set.eq_univ_iff_forall, not_forall],
    use j,
    rw set.mem_insert_iff,
    apply not_or,
    { exact (ne.symm h).elim },
    { simp }
  end ⟩

and I was going to try to do

def simplices_of_horn_hom {S : sSet} {n : ℕ} {i : fin (n+2)} (f : Λ[n+1,i] ⟶ S) :
  set.range (fin.succ_above i) → S _[n] :=

next, so I'll see if there are any issues here

[Adam Topaz]

TBH I only glanced as the definition of the horns we have in mathlib. Defining it as a colimit seems much more natural to me, and the faces then become first class citizens (as they're part of the diagram for the colimit)

[Ashwin Iyengar]

Oh right that seems like a good idea, I'll try writing that down

[Ashwin Iyengar]

I could also define it as "the smallest subsimplicial set containing the faces", which is morally the same thing, but might be a bit less cumbersome than explicitly constructing the diagram that the colimit is taken over

[Ashwin Iyengar]

but idk I've never worked with colimits in Lean so maybe these would take a similar amount of code

[Adam Topaz]

I'm not sure how easy it is to take a sup of some subobjects.

[Bhavik Mehta]

#6809

[Scott Morrison]

It's a finset.sup, isn't it? That's already in mathlib for subobject.