English
The Freyd–Mitchell embedding functor preserves finite colimits.
Русский
Функтор вложения Фрейда–Митчелла сохраняет конечные ко-отношения (кокелы).
LaTeX
$$$\mathrm{PreservesFiniteColimits}(\mathrm{FreydMitchell.functor}(C))$$$
Lean4
instance : PreservesFiniteColimits (functor C) := by
rw [functor]
have : PreservesFiniteColimits (F C) := by rw [F]; infer_instance
have : PreservesFiniteColimits (G C) := by rw [G]; apply preservesFiniteColimits_rightOp
have : PreservesFiniteColimits (H C) :=
IsGrothendieckAbelian.OppositeModuleEmbedding.preservesFiniteColimits_embedding _
infer_instance
