Theorems · Theorem · category theory

LightCondensed.isoFinYonedaComponents_inv_comp

∀ (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [inst : CategoryTheory.Limits.PreservesFiniteProducts F]
  {X Y : LightProfinite} [inst_1 : Finite ↑X.toTop] [inst_2 : Finite ↑Y.toTop]
  (f : ↑Y.toTop → F.obj (Opposite.op (LightProfinite.of PUnit.{u + 1}))) (g : X ⟶ Y),
  (CategoryTheory.ConcreteCategory.hom (LightCondensed.isoFinYonedaComponents F X).inv)
      (f ∘ ⇑(CategoryTheory.ConcreteCategory.hom g)) =
    (CategoryTheory.ConcreteCategory.hom (F.map g.op))
      ((CategoryTheory.ConcreteCategory.hom (LightCondensed.isoFinYonedaComponents F Y).inv) f)

Defined in

Mathlib.Condensed.Discrete.Colimit

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Limits.PreservesFiniteProductsFiniteFinite