English
If C has enough projectives, then Ext computations can be reduced to projective resolutions and have the expected exactness properties.
Русский
Если в C достаточно проектных объектов, то вычисления Ext сводимы к резолюциям по проектным объектам и удовлетворяют ожидаемым точным свойствам.
LaTeX
$$HasExt C from EnoughProjectives$$
Lean4
/-- If `C` is a locally `w`-small abelian category with enough projectives,
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_enoughProjectives [LocallySmall.{w} C] [EnoughProjectives 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 _ _ (kernel.condition (Projective.π X))
have hS : S.ShortExact := { exact := ShortComplex.exact_of_f_is_kernel _ (kernelIsKernel S.g) }
have : Function.Surjective (Ext.precomp hS.extClass Y (add_comm 1 n)) := fun x₃ ↦
Ext.contravariant_sequence_exact₃ hS Y x₃ (Ext.eq_zero_of_projective _) (by cutsat)
exact small_of_surjective.{w} this
