sigmaSigmaIso

Mathlib.CategoryTheory.Limits.Shapes.Products

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.sigmaSigmaIso

Lean4

/-- An iterated coproduct is a coproduct over a sigma type. -/
@[simps]
def sigmaSigmaIso {ι : Type*} (f : ι → Type*) (g : (i : ι) → (f i) → C) [∀ i, HasCoproduct (g i)]
    [HasCoproduct fun i => ∐ g i] : (∐ fun i => ∐ g i) ≅ (∐ fun p : Σ i, f i => g p.1 p.2)
    where
  hom := Sigma.desc fun i => Sigma.desc fun x => Sigma.ι (fun p : Σ i, f i => g p.1 p.2) ⟨i, x⟩
  inv := Sigma.desc fun ⟨i, x⟩ => Sigma.ι (g i) x ≫ Sigma.ι (fun i => ∐ g i) i

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru