Theorems · Definition · category theory

Condensed.ofSheafForgetProfinite

{A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    [∀ (X : CompHausᵒᵖ),
          CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X profiniteToCompHaus.op) A] →
      {FA : A → A → Type u_2} →
        {CA : A → Type u_3} →
          [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] →
            [inst_3 : CategoryTheory.ConcreteCategory A FA] →
              [CategoryTheory.Limits.ReflectsFiniteLimits (CategoryTheory.forget A)] →
                (F : CategoryTheory.Functor Profiniteᵒᵖ A) →
                  [CategoryTheory.Limits.PreservesFiniteProducts (F.comp (CategoryTheory.forget A))] →
                    CategoryTheory.regularTopology.EqualizerCondition (F.comp (CategoryTheory.forget A)) → Condensed A

The condensed object associated to a presheaf on Profinite whose postcomposition with the forgetful functor 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.HasLimitsOfShapeFunLikeCategoryTheory.ConcreteCategoryCategoryTheory.Limits.ReflectsFiniteLimitsCategoryTheory.Limits.PreservesFiniteProducts