English
The standardσ after inserting an index j into L equals the composition of standardσ on L and the corresponding σ at position j.
Русский
После вставки индекса j в L стандартное σ равняется композиции стандартσ на L и соответствующего σ на позиции j.
LaTeX
$$$\\\\text{standardσ}(\\text{simplicialInsert}(j,L)) = \\\\text{standardσ}(L) \\\\circ \\\\sigma( j )$$$
Lean4
/-- Performing a simplicial insertion in a list is the same as composition on the right by the
corresponding degeneracy operator. -/
theorem standardσ_simplicialInsert (hL : IsAdmissible (m + 1) L) (j : ℕ) (hj : j < m + 1) (m₁ : ℕ)
(hm₁ : m + L.length + 1 = m₁) :
standardσ (m₂ := m) (simplicialInsert j L) (m₁ := m₁) (by simpa only [simplicialInsert_length, add_assoc]) =
standardσ (m₂ := m + 1) L (by grind) ≫ σ (Fin.ofNat _ j) :=
by
induction L generalizing m j with
| nil => simp [standardσ, simplicialInsert]
| cons a L h_rec =>
simp only [simplicialInsert]
split_ifs
· simp
· have : ∀ (j k : ℕ) (h : j < (k + 1)), Fin.ofNat (k + 1) j = j := by
simp -- helps grind below
have : a < m + 2 := by
grind -- helps grind below
have : σ (Fin.ofNat (m + 2) a) ≫ σ (.ofNat _ j) = σ (.ofNat _ (j + 1)) ≫ σ (.ofNat _ a) := by
convert σ_comp_σ_nat (n := m) a j (by grind) (by grind) (by grind) <;> grind
simp only [standardσ_cons, Category.assoc, this, h_rec hL.tail (j + 1) (by grind) (by grind)]
