mkHomToSingle_f — Mathlib

English

For φ : K.X_j ⟶ A and hφ ensuring relations, the j-th component of mkHomToSingle φ hφ equals φ followed by the inverse of the canonical isomorphism.

Русский

Для φ: K.X_j ⟶ A и hφ, задающего отношения, j-я компонента mkHomToSingle φ hφ равна произведению φ с обратной стороной канонического изоморфизма.

LaTeX

$$$$ (\mathrm{mkHomToSingle} \phi h\phi).f_j = \phi \circ (\mathrm{singleObjXSelf} \, c\ j\ A)^{-1} $$$$

Lean4

@[simp]
theorem mkHomToSingle_f {K : HomologicalComplex V c} {j : ι} {A : V} (φ : K.X j ⟶ A)
    (hφ : ∀ (i : ι), c.Rel i j → K.d i j ≫ φ = 0) : (mkHomToSingle φ hφ).f j = φ ≫ (singleObjXSelf c j A).inv :=
  by
  dsimp [mkHomToSingle]
  rw [dif_pos rfl, id_comp]
  rfl

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