H2_induction_on — Mathlib

English

There is an induction principle for H2: to prove a property C on H2(A), it suffices to prove it on the images H2π(A) of cocycles.

Русский

Существует принцип индукции для H2: чтобы доказать свойство C на H2(A), достаточно доказать его на обображениях H2π(A) из cocycles.

LaTeX

$$$\forall C:\; H2(A)\to \mathrm{Prop},\; (\forall x\in cocycles_2(A), C(H2\pi_A(x)) ) \Rightarrow C\big|_{H2(A)}$$$

Lean4

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

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