English
The short complex generated by Fun(G, A) → Fun(G×G, A) → Fun(G×G×G, A) is isomorphic to the second short complex associated to the inhomogeneous cochain complex of A. This establishes a canonical equivalence between the two descriptions of the second level of cohomology.
Русский
Короткий комплекс, состоящий из функций G→A, G×G→A и G×G×G→A, изоморфен второму короткому комплексу, построенному на неоднородных кокозиальных соотношениях A. Образует каноническое эквивалентное описание второго уровня когомологий.
LaTeX
$$$\text{isoShortComplexH2}(A) : (inhomogeneousCochains(A)).sc\ 2 \cong shortComplexH2(A)$$$
Lean4
/-- The short complex `Fun(G, A) --d₁₂--> Fun(G × G, A) --dTwo--> Fun(G × G × G, A)` is
isomorphic to the 2nd short complex associated to the complex of inhomogeneous cochains of `A`. -/
@[simps! hom inv]
def isoShortComplexH2 : (inhomogeneousCochains A).sc 2 ≅ shortComplexH2 A :=
(inhomogeneousCochains A).isoSc' 1 2 3 (by simp) (by simp) ≪≫
isoMk (cochainsIso₁ A) (cochainsIso₂ A) (cochainsIso₃ A) (comp_d₁₂_eq A) (comp_d₂₃_eq A)
