Theorems · Theorem · category theory

Condensed.isoFinYonedaComponents_hom_apply

∀ (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [inst : CategoryTheory.Limits.PreservesFiniteProducts F]
  (X : Profinite) [inst_1 : Finite ↑X.toTop] (y : F.obj (Opposite.op X)) (x : ↑X.toTop),
  (CategoryTheory.ConcreteCategory.hom (Condensed.isoFinYonedaComponents F X).hom) y x =
    (CategoryTheory.ConcreteCategory.hom (F.map (CompHausLike.const (Profinite.of PUnit.{u + 1}) x).op)) y

Defined in

Mathlib.Condensed.Discrete.Colimit

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Limits.PreservesFiniteProductsFinite