Theorems · Theorem · category theory

CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi_inv_comp_pi

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasTerminal C] (ι : Type w)
  [inst_2 : CategoryTheory.Limits.HasFiniteProducts C] [inst_3 : Finite ι] (X : C) (j : ι),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CechNerveTerminalFrom.wideCospan.limitIsoPi ι X).inv
      (CategoryTheory.Limits.WidePullback.π (fun x => CategoryTheory.Limits.terminal.from X) j) =
    CategoryTheory.Limits.Pi.π (fun x => X) j

Defined in

Mathlib.AlgebraicTopology.CechNerve

Cited by

2 results in Mathlib

Foundations

Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasTerminalCategoryTheory.Limits.HasFiniteProductsFinite