groupHomology_induction_on — Mathlib

English

The nth group homology H_n(G,A) is canonically isomorphic to the Tor functor, i.e. to Tor^G_n(A,k) with k the trivial G-representation.

Русский

n-я групповая гомология H_n(G,A) канонически изоморфна тор-обобщению, то есть Tor^G_n(A,k) для тривиального представления k.

LaTeX

$$groupHomologyIsoTor(A,n) ≅ ((Tor k G n).obj A).obj (Rep.trivial k G k)$$

Lean4

@[elab_as_elim]
theorem groupHomology_induction_on {n : ℕ} {C : groupHomology A n → Prop} (x : groupHomology A n)
    (h : ∀ x : cycles A n, C (π A n x)) : C x :=
  by
  rcases (ModuleCat.epi_iff_surjective (π A n)).1 inferInstance x with ⟨y, rfl⟩
  exact h y

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