hσ'_eq — Mathlib

English

If n = a + q, then hσ' q n m hnm equals (-1)^a times σ with index a, followed by a face map adjustment, yielding an explicit alternating sum component.

Русский

Если n = a + q, то hσ' q n m hnm равняется (-1)^a умноженному на σ с индексом a, за тем идёт корректировка карты лица, дающая явный антисимметричный элемент.

LaTeX

$$$$ hσ' q n m hnm = (-1)^a \cdot X.σ ⟨a, \text{idx}⟩ \circ \text{eqToHom} $$$$

Lean4

theorem hσ'_eq {q n a m : ℕ} (ha : n = a + q) (hnm : c.Rel m n) :
    (hσ' q n m hnm : X _⦋n⦌ ⟶ X _⦋m⦌) =
      ((-1 : ℤ) ^ a • X.σ ⟨a, Nat.lt_succ_iff.mpr (Nat.le.intro (Eq.symm ha))⟩) ≫ eqToHom (by congr) :=
  by grind [hσ', hσ]

Похожие утверждения