eq_zero_of_projective — Mathlib

English

If C is locally small and has enough projectives, HasExt C holds; Ext exists in all degrees with appropriate functorial behavior.

Русский

Если C локально малое и имеет достаточно проектных объектов, тогда HasExt C существует; Ext имеет требуемое функториальное поведение во всех степенях.

LaTeX

$$HasExt C holds given locally small and enough projectives$$

Lean4

theorem eq_zero_of_projective [HasExt.{w} C] {P Y : C} {n : ℕ} [Projective P] (e : Ext P Y (n + 1)) : e = 0 :=
  by
  letI := HasDerivedCategory.standard C
  apply homEquiv.injective
  simp only [← cancel_mono (((singleFunctors C).shiftIso (n + 1) (-(n + 1)) 0 (by cutsat)).hom.app _), zero_hom,
    Limits.zero_comp]
  apply
    from_singleFunctor_obj_eq_zero_of_projective (L := (CochainComplex.singleFunctor C (-(n + 1))).obj Y) (n :=
      -(n + 1)) _ (by cutsat)

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