lift_d_comp_eq_zero_iff — Mathlib

English

In the left-homology data, lifting along an extension induces a zero map under the specified conditions.

Русский

В левой гомологической структуре подъем вдоль расширения порождает нулевой отображение при заданных условиях.

LaTeX

$$$lift\\_d\\_comp\\_eq\\_zero'\\;\\text{(предикаты)}$$$

Lean4

theorem lift_d_comp_eq_zero_iff ⦃W : C⦄ (φ : cone.pt ⟶ W) :
    hcone.lift (KernelFork.ofι (K.d i j) (K.d_comp_d i j k)) ≫ φ = 0 ↔
      ((isLimitKernelFork K e hj' hk hk' cone hcone).lift (KernelFork.ofι ((K.extend e).d i' j') (d_comp_d _ _ _ _))) ≫
          φ =
        0 :=
  lift_d_comp_eq_zero_iff' K e hj' hi hi' cone hcone _ (hcone.fac _ _) _ (IsLimit.fac _ _ WalkingParallelPair.zero) _

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