Theorems · Theorem · category theory

LightCondensed.isoFinYoneda_inv_app_hom_apply

∀ (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [inst : CategoryTheory.Limits.PreservesFiniteProducts F]
  (X : FintypeCatᵒᵖ)
  (a :
    (CategoryTheory.Limits.Types.productLimitCone fun x =>
          F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))).cone.pt),
  (CategoryTheory.ConcreteCategory.hom ((LightCondensed.isoFinYoneda F).inv.app X)) a =
    (CategoryTheory.CategoryStruct.id
          (F.obj (Opposite.op (LightCondensed.fintypeCatAsCofan (LightProfinite.of (Opposite.unop X).obj)).pt))).hom'
      ((((CategoryTheory.Limits.IsLimit.postcomposeHomEquiv
                    (CategoryTheory.Discrete.natIso fun j =>
                      CategoryTheory.Iso.refl (F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))))
                    (F.mapCone
                      (CategoryTheory.Limits.Fan.mk
                        (Opposite.op (LightCondensed.fintypeCatAsCofan (LightProfinite.of (Opposite.unop X).obj)).pt)
                        fun a =>
                        ((LightCondensed.fintypeCatAsCofan (LightProfinite.of (Opposite.unop X).obj)).inj a).op))).symm
                (CategoryTheory.Limits.isLimitOfPreserves F
                  (CategoryTheory.Limits.Cofan.IsColimit.op
                    (LightCondensed.fintypeCatAsCofanIsColimit (LightProfinite.of (Opposite.unop X).obj))))).lift
            (CategoryTheory.Limits.Types.productLimitCone fun x =>
                F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))).cone).hom'
        a)

Defined in

Mathlib.Condensed.Discrete.Colimit

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Limits.PreservesFiniteProducts