instPreservesFiniteLimitsModuleCatEmbeddingRingFunctor

English

The Freyd–Mitchell embedding functor preserves finite limits.

Русский

Функтор вложения Фрейда–Митчелла сохраняет конечные пределы.

LaTeX

$$$\mathrm{PreservesFiniteLimits}(\mathrm{FreydMitchell.functor}(C))$$$

Lean4

instance : PreservesFiniteLimits (functor C) := by
  rw [functor]
  have : PreservesFiniteLimits (F C) := by rw [F]; infer_instance
  have : PreservesFiniteLimits (G C) := by rw [G]; apply preservesFiniteLimits_rightOp
  have : PreservesFiniteLimits (H C) := IsGrothendieckAbelian.OppositeModuleEmbedding.preservesFiniteLimits_embedding _
  infer_instance

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