d — Mathlib · SciLib

English

Recasting H2_induction_on: a uniform induction principle for elements of H2 via cocycles.

Русский

Переформулировка H2_induction_on: единый принцип индукции по элементам H2 через кокциклes.

LaTeX

$$H2Induction_on : {C : H2(A) → Prop} → ∀ x ∈ (groupCohomology.H2 A).carrier, (∀ y ∈ cocycles₂ A, C(H2π A y)) → C x$$

Lean4

/-- The differential in the complex of inhomogeneous chains used to calculate group homology. -/
def d : ModuleCat.of k ((Fin (n + 1) → G) →₀ A) ⟶ ModuleCat.of k ((Fin n → G) →₀ A) :=
  ModuleCat.ofHom <|
    lsum (R := k) k fun g =>
      lsingle (fun i => g i.succ) ∘ₗ A.ρ (g 0)⁻¹ +
        Finset.univ.sum fun j : Fin (n + 1) => (-1 : k) ^ ((j : ℕ) + 1) • lsingle (Fin.contractNth j (· * ·) g)

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