fin n combinatorics

Stream: Is there code for X?

[Kevin Buzzard]

I find fin n combinatorics much easier if I do maps from fin i to fin j assuming h : j = i + 1 rather than going to fin (i+1) directly. Here is a definition and some lemmas about a function called "delta^p" in Riehl-Verity. I can use it to define group cohomology. Do we have it already in mathlib? If not, where does it go?

import data.fin -- yes all 1800 lines of it
import tactic

namespace fin

/-- The function dsending enoted `δᵖ` by Riehl-Verity, sending`t` to `t` if `t<p` and
  `t.succ` otherwise.`-/
def delta {i j : ℕ} (hj : j = i + 1) (p : ℕ) (t : fin i) : fin j :=
-- fin.succ_above expects p : fin i.succ for some reason
⟨if (t : ℕ) < p then t else (t : ℕ).succ, begin
  subst hj,
  cases t with t ht,
  split_ifs,
  { exact ht.trans (nat.lt_succ_self _) },
  { exact nat.succ_lt_succ ht },
end⟩

lemma delta_eval {i j : ℕ} (hj : j = i + 1) (p : ℕ) (t : fin i) :
  (delta hj p t : ℕ) = if (t : ℕ) < p then t else (t : ℕ).succ := rfl

theorem delta_comm_apply  {i j k : ℕ} (hj : j = i.succ) (hk : k = j.succ) {p q : ℕ}
  (hpq : p ≤ q) (t : fin i) : delta hk q.succ (delta hj p t) = delta hk p (delta hj q t) :=
begin
  subst hk,
  subst hj,
  ext,
  cases t with t ht,
  simp only [delta_eval],
  dsimp,
  split_ifs;
  try {rw nat.succ_eq_add_one at *};
  try {push_neg at *};
  try {rw nat.succ_eq_add_one at *};
  try {linarith},
end

theorem delta_comm_apply.symm {i j k : ℕ} (hj : j = i.succ) (hk : k = j.succ) {p q_succ : ℕ}
  (hpq : q_succ ≤ p) (t : fin i) :
  delta hk p.succ (delta hj q_succ t) = delta hk q_succ (delta hj p t) :=
delta_comm_apply hj hk hpq t

end fin

[Adam Topaz]

We have the simplicial identities in src#algebraic_topology.simplex_category

[Adam Topaz]

Ok I don't know how to use the file linkifier

[Adam Topaz]

Anyway, your first def looks like docs#fin.succ_above maybe?

[Adam Topaz]

Except that uses fin (n+1) which seems like you don't like.

[Reid Barton]

so, it's that combined with docs#fin.cast

[Kevin Buzzard]

The simplex category work is not general enough because it ignores the case n=0!

[Kevin Buzzard]

Is this evidence I'm doing something wrong? The abstract delta-ism and sigma-ism works fine for it

[Johan Commelin]

Are you doing augmented simplicial objects?

[Kevin Buzzard]

I'm just copying the definition of group cohomology from Cassels-Froehlich

[Kevin Buzzard]

It's on the group-cohomology branch. Right now i am not at all sure if I want to use the simplex category at all -- why obfuscate?

[Reid Barton]

Kevin Buzzard said:

Is this evidence I'm doing something wrong? The abstract delta-ism and sigma-ism works fine for it

Yes I think so

[Reid Barton]

Well actually no because as far as I can see you don't actually use the case n=0

[Reid Barton]

def std_resn_complex : chain_complex (Module (group_ring G)) ℕ :=
chain_complex.of (λ n, Module.of (group_ring G) (group_ring (fin (n + 1) → G)))
(λ n, d G rfl) (λ n, by ext1; exact d_squared _ _ _ _)

[Kevin Buzzard]

Somehow I thought it would be useful. The concrete model for group cohomology H^n is cocycles over coboundaries. When n=0 you want it to be 0-cocycles over 0-coboundaries, but to have 0-coboundaries you need $-1$-cochains

[Reid Barton]

Your chain complex is indexed by ℕ though right? so you don't have (-1)-anything

[Adam Topaz]

@Kevin Buzzard you can use a Nat-indexed complex,

[Adam Topaz]

Besides, if you define something like this at $-1$, you will probably get annoyed later on if and when you go to work with Tate cohomology (which can be defined using a specific $\mathbb{Z}$-indexed complex)