homOf — Mathlib

English

The homOf construction is compatible with the underlying hom complex as a morphism.

Русский

Конструкция homOf совместима с соответствующим гомоморфизмом в гом-комплексе.

LaTeX

$$homOf (z) : F ⟶ G is a morphism and preserves the cocycle structure$$

Lean4

/-- The morphism in `CochainComplex C ℤ` associated to a `0`-cocycle. -/
@[simps]
def homOf (z : Cocycle F G 0) : F ⟶ G
    where
  f i := (z : Cochain _ _ _).v i i (add_zero i)
  comm' := by
    rintro i j rfl
    rcases z with ⟨z, hz⟩
    dsimp
    rw [mem_iff 0 1 (zero_add 1)] at hz
    simpa only [δ_zero_cochain_v, Cochain.zero_v, sub_eq_zero] using Cochain.congr_v hz i (i + 1) rfl

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