d_squared — Mathlib

English

For a Karoubi object P in the simplicial setting, the differential respects the Karoubi decomposition, i.e. the d-map commutes with the projection to P.

Русский

Для объекта Карауби в симпликсиальном контексте дифференциал совместим с разложением Карауби; отображение d commuting с проекциями.

LaTeX

$$$((AlternatingFaceMapComplex.obj (KaroubiFunctorCategoryEmbedding.obj P)).d (n+1) n).f = P.p.app (\mathrm{op}\,⟦n+1⟧) \; \circ\; (AlternatingFaceMapComplex.obj P.X).d (n+1) n$$$

Lean4

theorem d_squared (n : ℕ) : objD X (n + 1) ≫ objD X n = 0 := by
  -- we start by expanding d ≫ d as a double sum

  dsimp
  simp only [comp_sum, sum_comp, ← Finset.sum_product']
    -- then, we decompose the index set P into a subset S and its complement Sᶜ

  let P := Fin (n + 2) × Fin (n + 3)
  let S : Finset P := {ij : P | (ij.2 : ℕ) ≤ (ij.1 : ℕ)}
  rw [Finset.univ_product_univ, ← Finset.sum_add_sum_compl S, ← eq_neg_iff_add_eq_zero, ← Finset.sum_neg_distrib]
    /- we are reduced to showing that two sums are equal, and this is obtained
        by constructing a bijection φ : S -> Sᶜ, which maps (i,j) to (j,i+1),
        and by comparing the terms -/

  let φ : ∀ ij : P, ij ∈ S → P := fun ij hij =>
    (Fin.castLT ij.2 (lt_of_le_of_lt (Finset.mem_filter.mp hij).right (Fin.is_lt ij.1)), ij.1.succ)
  apply Finset.sum_bij φ
  · -- φ(S) is contained in Sᶜ

    intro ij hij
    simp_rw [S, φ, Finset.compl_filter, Finset.mem_filter_univ, Fin.val_succ, Fin.coe_castLT] at hij ⊢
    cutsat
  · -- φ : S → Sᶜ is injective

    rintro ⟨i, j⟩ hij ⟨i', j'⟩ hij' h
    rw [Prod.mk_inj]
    exact
      ⟨by simpa [φ] using congr_arg Prod.snd h, by
        simpa [φ, Fin.castSucc_castLT] using congr_arg Fin.castSucc (congr_arg Prod.fst h)⟩
  · -- φ : S → Sᶜ is surjective

    rintro ⟨i', j'⟩ hij'
    simp_rw [S, Finset.compl_filter, Finset.mem_filter_univ, not_le] at hij'
    refine ⟨(j'.pred <| ?_, Fin.castSucc i'), ?_, ?_⟩
    · rintro rfl
      simp only [Fin.val_zero, not_lt_zero'] at hij'
    · simpa [S] using Nat.le_sub_one_of_lt hij'
    · simp only [φ, Fin.castLT_castSucc, Fin.succ_pred]
  · -- identification of corresponding terms in both sums

    rintro ⟨i, j⟩ hij
    dsimp
    simp only [zsmul_comp, comp_zsmul, smul_smul, ← neg_smul]
    congr 1
    · simp only [φ, Fin.val_succ, pow_add, pow_one, mul_neg, neg_neg, mul_one]
      apply mul_comm
    · rw [CategoryTheory.SimplicialObject.δ_comp_δ'']
      simpa [S] using hij

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