Theorems · Theorem · category theory

Condensed.hasExactLimitsOfShape

∀ (A : Type u_1) (J : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J] [CategoryTheory.Preadditive A]
  [∀ (X : CompHausᵒᵖ),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X Stonean.toCompHaus.op) A]
  [CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology CompHaus) A]
  [CategoryTheory.HasWeakSheafify (CategoryTheory.extensiveTopology Stonean) A]
  [inst_6 : CategoryTheory.Limits.HasLimitsOfShape J A] [CategoryTheory.HasExactLimitsOfShape J A]
  [CategoryTheory.Limits.HasFiniteColimits A], CategoryTheory.HasExactLimitsOfShape J (Condensed A)

Defined in

Mathlib.Condensed.AB

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.PreadditiveCategoryTheory.Limits.HasLimitsOfShapeCategoryTheory.HasWeakSheafifyCategoryTheory.HasWeakSheafifyCategoryTheory.Limits.HasLimitsOfShapeCategoryTheory.HasExactLimitsOfShapeCategoryTheory.Limits.HasFiniteColimits