English
A second variant of Ext vanishing in the injective scenario; the result persists under different indexing conventions.
Русский
Второй вариант исчезновения Ext в случае инъективности; вывод сохраняется при другой индексации.
LaTeX
$$Eq e 0 under injective indexing$$
Lean4
/-- If `C` is a locally `w`-small abelian category with enough injectives,
then `HasExt.{w} C` holds. We do not make this an instance though:
for a given category `C`, there may be different reasonable choices for
the universe `w`, and if we have two `HasExt.{w₁} C` and `HasExt.{w₂} C`
instances, we would have to specify the universe explicitly almost
everywhere, which would be an inconvenience. Then, we must be
very selective regarding `HasExt` instances. -/
theorem hasExt_of_enoughInjectives [LocallySmall.{w} C] [EnoughInjectives C] : HasExt.{w} C :=
by
letI := HasDerivedCategory.standard C
have := hasExt_of_hasDerivedCategory C
rw [hasExt_iff_small_ext.{w}]
intro X Y n
induction n generalizing X Y with
| zero =>
rw [small_congr Ext.homEquiv₀]
infer_instance
| succ n hn =>
let S := ShortComplex.mk _ _ (cokernel.condition (Injective.ι Y))
have hS : S.ShortExact := { exact := ShortComplex.exact_of_g_is_cokernel _ (cokernelIsCokernel S.f) }
have : Function.Surjective (Ext.postcomp hS.extClass X (rfl : n + 1 = _)) := fun y₁ ↦
Ext.covariant_sequence_exact₁ X hS y₁ (Ext.eq_zero_of_injective _) rfl
exact small_of_surjective.{w} this
