instIsIsoSigmaComparison — Mathlib

English

Let G: C → D be a functor and f: J → C a diagram indexed by J. If f has a coproduct in C and the diagram j ↦ G(f(j)) has a coproduct in D, and G preserves the coproduct of the discrete diagram f, then the canonical comparison map σ_{G,f} : ⨿_{j∈J} G(f(j)) → G(⨿_{j∈J} f(j)) is an isomorphism.

Русский

Пусть G: C → D — функтор, f: J → C — диаграмма, индексированная множеством J. Если в C существует копроизведение для f и в D существует копроизведение для диаграммы j ↦ G(f(j)), и G сохраняет копроизведение дискретной диаграммы f, то каноническое отображение σ_{G,f} : ⨿_{j∈J} G(f(j)) → G(⨿_{j∈J} f(j)) является изоморфизмом.

LaTeX

$$$IsIso(\\sigma_{G,f})$$$

Lean4

instance : IsIso (sigmaComparison G f) := by
  rw [← PreservesCoproduct.inv_hom]
  infer_instance

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