inhomogeneousChains — Mathlib

English

Compatibility of Shapiro's coindIso with the Yoneda-type res-projection in the Shapiro diagram.

Русский

Совместимость коиндИзоморфизма Шапиро с резольв saud Yoneda-подобной связью.

LaTeX

$$groupCohomology.coindIso A n ≅ groupCohomology A n := ...$$

Lean4

/-- Given a `k`-linear `G`-representation `A`, this is the complex of inhomogeneous chains
$$\dots \to \bigoplus_{G^1} A \to \bigoplus_{G^0} A \to 0$$
which calculates the group homology of `A`. -/
noncomputable abbrev inhomogeneousChains : ChainComplex (ModuleCat k) ℕ :=
  ChainComplex.of (fun n => ModuleCat.of k ((Fin n → G) →₀ A)) (fun n => inhomogeneousChains.d A n) fun n => by
    classical
    simp only [inhomogeneousChains.d_eq]
    slice_lhs 3 4 => {rw [Iso.hom_inv_id]}
    slice_lhs 2 4 => {rw [Category.id_comp, ((barComplex k G).coinvariantsTensorObj A).d_comp_d]}
    simp

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