H1_induction_on — Mathlib

English

An induction principle for elements of H1 A: to prove a property for any element of H1 A it suffices to prove it for representatives coming from cocycles via H1π.

Русский

Принцип индукции по элементам H1 A: чтобы доказать свойство для любого элемента H1 A достаточно доказать его для представителей, приходящих из кокцикла через H1π.

LaTeX

$$theorem H1_induction_on {C : H1 A → Prop} (x : H1 A) (h : ∀ x : cocycles₁ A, C (H1π A x)) : C x$$

Lean4

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

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