## Stream: maths

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

#### 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?

#### 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...

#### 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?

#### Ashwin Iyengar (Mar 24 2021 at 10:10):

Yes ok that works in this case

#### Johan Commelin (Mar 24 2021 at 10:13):

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

#### Ashwin Iyengar (Mar 24 2021 at 10:13):

How did you deal with this issue for complexes?

#### Johan Commelin (Mar 24 2021 at 10:13):

In a mathematically very ugly way.

#### Johan Commelin (Mar 24 2021 at 10:14):

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

#### Johan Commelin (Mar 24 2021 at 10:14):

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

#### Johan Commelin (Mar 24 2021 at 10:15):

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

#### Johan Commelin (Mar 24 2021 at 10:15):

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

#### 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.

#### Ashwin Iyengar (Mar 24 2021 at 10:17):

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

#### 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 $\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 (Mar 24 2021 at 10:24):

But does it work for n+1?

#### Johan Commelin (Mar 24 2021 at 10:24):

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

Ah good point

#### Ashwin Iyengar (Mar 24 2021 at 10:25):

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

#### 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.

#### 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...

#### 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 ?

#### 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

#### 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)

#### Ashwin Iyengar (Mar 24 2021 at 13:31):

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

#### 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

#### 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

#### Adam Topaz (Mar 24 2021 at 13:57):

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

#6809

#### 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