Zulip Chat Archive

Stream: maths

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


view this post on Zulip Ashwin Iyengar (Mar 24 2021 at 00:15):

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?

view this post on Zulip Johan Commelin (Mar 24 2021 at 06:38):

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

view this post on Zulip Johan Commelin (Mar 24 2021 at 06:39):

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

view this post on Zulip Ashwin Iyengar (Mar 24 2021 at 10:10):

Yes ok that works in this case

view this post on Zulip Johan Commelin (Mar 24 2021 at 10:13):

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

view this post on Zulip Ashwin Iyengar (Mar 24 2021 at 10:13):

How did you deal with this issue for complexes?

view this post on Zulip Johan Commelin (Mar 24 2021 at 10:13):

In a mathematically very ugly way.

view this post on Zulip Johan Commelin (Mar 24 2021 at 10:14):

We now have a map di,j ⁣:CiCjd_{i,j} \colon C_i \to C_j, for all pairs (i,j)(i,j).

view this post on Zulip Johan Commelin (Mar 24 2021 at 10:14):

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

view this post on Zulip Johan Commelin (Mar 24 2021 at 10:15):

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

view this post on Zulip Johan Commelin (Mar 24 2021 at 10:15):

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

view this post on Zulip Johan Commelin (Mar 24 2021 at 10:16):

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.

view this post on Zulip Ashwin Iyengar (Mar 24 2021 at 10:17):

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

view this post on Zulip Ashwin Iyengar (Mar 24 2021 at 10:21):

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 Λ[n,i]S\Lambda[n,i] \to S with an nn-tuple in Sn1S_{n-1} (which is useful in proofs (or maybe this is secretly a red herring?)) then things get weird

view this post on Zulip Johan Commelin (Mar 24 2021 at 10:24):

But does it work for n+1?

view this post on Zulip Johan Commelin (Mar 24 2021 at 10:24):

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

view this post on Zulip Ashwin Iyengar (Mar 24 2021 at 10:24):

Ah good point

view this post on Zulip Ashwin Iyengar (Mar 24 2021 at 10:25):

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

view this post on Zulip Kevin Buzzard (Mar 24 2021 at 11:53):

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.

view this post on Zulip Scott Morrison (Mar 24 2021 at 12:23):

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

view this post on Zulip Adam Topaz (Mar 24 2021 at 13:25):

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

view this post on Zulip Ashwin Iyengar (Mar 24 2021 at 13:27):

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

view this post on Zulip Adam Topaz (Mar 24 2021 at 13:28):

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)

view this post on Zulip Ashwin Iyengar (Mar 24 2021 at 13:31):

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

view this post on Zulip Ashwin Iyengar (Mar 24 2021 at 13:49):

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

view this post on Zulip Ashwin Iyengar (Mar 24 2021 at 13:49):

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

view this post on Zulip Adam Topaz (Mar 24 2021 at 13:57):

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

view this post on Zulip Bhavik Mehta (Mar 24 2021 at 16:02):

#6809

view this post on Zulip Scott Morrison (Mar 24 2021 at 21:45):

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


Last updated: May 18 2021 at 06:15 UTC