ofIsLimitKernelFork_g' — Mathlib

English

Let S be a ShortComplex in a category with zero morphisms, and suppose S.f = 0. Let c be a kernel fork of S.g which is universal (IsLimit). Then the g'-component of the right-homology data obtained from this limit equals S.g.

Русский

Пусть S — короткий комплекс в категории с нулевыми морфизмами, и пусть S.f = 0. Пусть c — ядро-ветвление (KernelFork) для S.g, являющееся пределом. Тогда компонент g' правой гомологии, полученной из этой данных, равен g.

LaTeX

$$$ (\mathrm{ofIsLimitKernelFork} S hf c hc).g' = S.g $$$

Lean4

@[simp]
theorem ofIsLimitKernelFork_g' (hf : S.f = 0) (c : KernelFork S.g) (hc : IsLimit c) :
    (ofIsLimitKernelFork S hf c hc).g' = S.g := by
  rw [← cancel_epi (ofIsLimitKernelFork S hf c hc).p, p_g', ofIsLimitKernelFork_p, id_comp]

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