H2_induction_on — Mathlib

English

Let C be a property on H2(A). If for every 2-cycle x the property holds for its image H2π A x, then the property holds for every element of H2(A).

Русский

Пусть C — свойство на H2(A). Если для всякого 2-цикла x верно C(H2π A x), то верно C для каждого элемента H2(A).

LaTeX

$$If C : H2(A) → Prop and ∀ x ∈ cycles₂(A), C(H2π(A)(x)) then ∀ y ∈ H2(A), C(y).$$

Lean4

@[elab_as_elim]
theorem H2_induction_on {C : H2 A → Prop} (x : H2 A) (h : ∀ x : cycles₂ A, C (H2π A x)) : C x :=
  groupHomology_induction_on x (fun y => by simpa [H2π] using h ((isoCycles₂ A).hom y))

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