mkHomFromSingle_f — Mathlib

English

For φ : A ⟶ K.X_j and hφ ensuring relations, the j-th component of mkHomFromSingle φ hφ equals the canonical hom composed with φ.

Русский

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

LaTeX

$$$$ (\mathrm{mkHomFromSingle} \phi h\phi).f_j = (\mathrm{singleObjXSelf} \ c\ j\ A).hom \circ \phi $$$$

Lean4

@[simp]
theorem mkHomFromSingle_f {K : HomologicalComplex V c} {j : ι} {A : V} (φ : A ⟶ K.X j)
    (hφ : ∀ (k : ι), c.Rel j k → φ ≫ K.d j k = 0) : (mkHomFromSingle φ hφ).f j = (singleObjXSelf c j A).hom ≫ φ :=
  by
  dsimp [mkHomFromSingle]
  rw [dif_pos rfl, comp_id]
  rfl

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