mapCocycles₁_one — Mathlib

English

Inflation and restriction yield an exact three-term complex relating invariants under S and the whole group.

Русский

Инфляция и ограничение образуют точный трёхчленный комплекс между инвариантами по S и по всей группе.

LaTeX

$$$ H^1(G/S, A^S) \xrightarrow{f} H^1(G,A) \xrightarrow{g} H^1(S,A) $$$

Lean4

@[simp]
theorem mapCocycles₁_one (φ : (Action.res _ 1).obj A ⟶ B) : mapCocycles₁ 1 φ = 0 :=
  by
  rw [← cancel_mono (moduleCatLeftHomologyData (shortComplexH1 B)).i, cyclesMap'_i]
  refine ModuleCat.hom_ext (LinearMap.ext fun _ ↦ funext fun y => ?_)
  simp [mapShortComplexH1, shortComplexH1, Pi.zero_apply y]

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