The simplex category

Stream: Is there code for X?

[Kevin Buzzard]

def simplicial_sigma {i j : ℕ} (hij : j = i + 1) (k : ℕ) (t : fin i) : fin j :=
⟨if htk : t.1 < k then t.1 else t.1.succ, sorry⟩

Do we have this function in Lean already? I need to know some API for it for an experimental version of group cohomology, which I am trying to make a concrete model of in Lean 3 to see just how far we can get nowadays. I think it would be interesting to pit Lean 4 against Lean 3 for a definition of group cohomology. We mathematicians seem to be getting a good understanding of how to encode our ideas in your type theory and a Lean 3 definition of group cohomology could be regarded as a blueprint for a port to Lean 4.

[Adam Topaz]

This is docs#fin.succ_above (I think)

[Kevin Buzzard]

What tools do we need in Lean 4 to get a spectral sequence for group cohomology?

[Adam Topaz]

Adam Topaz said:

This is docs#fin.succ_above (I think)

maybe upto composition with a cast

[Kevin Buzzard]

Why the heck is there an assumption p \le n in docs#fin.succ_above ? Why can't p just be a nat?

/-- `succ_above' rfl p` is the embedding `fin i ↪o fin i.succ` with a hole around `min p i`.
In other words, it sends t to t if t < p and t.succ otherwise. -/
def fin.succ_above' {i j : ℕ} (hij : j = i.succ) (p : ℕ) : fin i ↪o fin j :=
let this : fin i ↪o fin i.succ := fin.succ_above (if hp : p ≤ i
  then ⟨p, nat.lt_succ_iff.mpr hp⟩
  else ⟨i, lt_add_one i⟩) in begin
  subst hij,
  exact this,
end

Isn't my variant a more flexible object? What is all this cast_succ nonsense?

[Kevin Buzzard]

We are imagining that this will range through the i+1 inclusions "leave a hole at p : fin i.succ but if we model the map as "if you pass the _ < p test I will leave you alone, otherwise I will apply succ" then there is no clear reason to me why the fact that all these tests give the same answer the moment $p\geq i$ is relevant.

[Adam Topaz]

Kevin, is your goal to define group cohomology with homogeneous cocycles? If so, you could write down the classifying space of a group as a simplicial set, and use the existing simplicial machinery... (This is all talking about lean 3 with current mathlib, of course)

[Adam Topaz]

We'll port the alternating coface complex from LTE to mathlib soon, and then you can get group cohomology "for free"

[Adam Topaz]

If you make the classifying space construction functorial as well, then you get the change of group operations easily as well

[Adam Topaz]

(well, except for corestriction)

[Adam Topaz]

One of the major annoyances I had with the simplicial stuff in lean 3 is the fact that fin n is not universe polymorphic. I wonder if we can have a universe polymorphic fin n right from the start in lean 4 without ulift nonsense