rightHomologyData_g' — Mathlib

English

The g'-field of the right-hand extension data is obtained by composing the original g' with the inverse of extendXIso.

Русский

Поле g' правой части данных расширения получается как композиция g' с обратной extendXIso.

LaTeX

$$g' = g' ∘ (extendXIso e hk'')^{-1}$$

Lean4

/-- Computation of the `g'` field of `extend.rightHomologyData`. -/
theorem rightHomologyData_g' (h : (K.sc' i j k).RightHomologyData) (hk'' : e.f k = k') :
    (rightHomologyData K e hj' hi hi' hk hk' h).g' = h.g' ≫ (K.extendXIso e hk'').inv :=
  by
  rw [← cancel_epi h.p, ← cancel_epi (extendXIso K e hj').hom]
  have := (rightHomologyData K e hj' hi hi' hk hk' h).p_g'
  dsimp at this
  rw [assoc] at this
  rw [this, K.extend_d_eq e hj' hk'', h.p_g'_assoc, shortComplexFunctor'_obj_g]

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