Theorems · Definition · category theory

LightCondensed.ofSheafForgetLightProfinite

{A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {FA : A → A → Type u_2} →
      {CA : A → Type u_3} →
        [inst_1 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory A FA] →
            [CategoryTheory.Limits.ReflectsFiniteLimits (CategoryTheory.forget A)] →
              (F : CategoryTheory.Functor LightProfiniteᵒᵖ A) →
                [CategoryTheory.Limits.PreservesFiniteProducts (F.comp (CategoryTheory.forget A))] →
                  CategoryTheory.regularTopology.EqualizerCondition (F.comp (CategoryTheory.forget A)) →
                    LightCondensed A

The light condensed object associated to a presheaf on LightProfinite whose postcomposition with the forgetful functor preserves finite products and satisfies the equalizer condition.

Defined in

Mathlib.Condensed.Light.Explicit

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryFunLikeCategoryTheory.ConcreteCategoryCategoryTheory.Limits.ReflectsFiniteLimitsCategoryTheory.Limits.PreservesFiniteProducts