Theorems · Definition · category theory

Condensed.ofSheafProfinite

{A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    [∀ (X : CompHausᵒᵖ),
          CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X profiniteToCompHaus.op) A] →
      (F : CategoryTheory.Functor Profiniteᵒᵖ A) →
        [CategoryTheory.Limits.PreservesFiniteProducts F] →
          CategoryTheory.regularTopology.EqualizerCondition F → Condensed A

The condensed object associated to a presheaf on Profinite which preserves finite products and satisfies the equalizer condition.

Defined in

Mathlib.Condensed.Explicit

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasLimitsOfShapeCategoryTheory.Limits.PreservesFiniteProducts