liftHomology_ι — Mathlib

English

Same universal lifting statement as LiftHomology_ι: for k: A → S.opcycles with k ≫ S.fromOpcycles = 0, the lift composed with homologyι equals k.

Русский

Та же формулировка подъёма гомологии: для k: A → S.opcycles с k ≫ S.fromOpcycles = 0, подъёмной отображение после homologyι равно k.

LaTeX

$$$S.liftHomology(k,hk) \;\;\; S.homologyι = k$$$

Lean4

@[reassoc (attr := simp)]
theorem liftHomology_ι (k : A ⟶ S.opcycles) (hk : k ≫ S.fromOpcycles = 0) : S.liftHomology k hk ≫ S.homologyι = k :=
  Fork.IsLimit.lift_ι S.homologyIsKernel

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