liftH_ι — Mathlib

English

In the right homology data, the liftH map composed with ι yields the identity on the target when hk is satisfied.

Русский

В данных правой гомологии отображение liftH, сочетающееся с ι, даёт тождественный переход к целевому объекту при выполнении условия hk.

LaTeX

$$$h.liftH k hk \circ h.ι = k$ for appropriate k and hk$$

Lean4

@[reassoc (attr := simp)]
theorem liftH_ι (k : A ⟶ h.Q) (hk : k ≫ h.g' = 0) : h.liftH k hk ≫ h.ι = k :=
  h.hι.fac (KernelFork.ofι k hk) WalkingParallelPair.zero

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