Theorems · Theorem · category theory

LightCondensed.ihomPoints_apply

∀ (R : Type u) [inst : CommRing R] (A B : LightCondMod R) (S : LightProfinite) (x : ↑((A ⟹ B).obj.obj (Opposite.op S))),
  (LightCondensed.ihomPoints R A B S) x =
    CategoryTheory.MonoidalClosed.uncurry
      (((LightCondensed.freeForgetAdjunction R).homEquiv ((CategoryTheory.coherentTopology LightProfinite).yoneda.obj S)
            (A ⟹ B)).symm
        ((CategoryTheory.coherentTopology LightProfinite).yonedaEquiv.symm x))

Defined in

Mathlib.Condensed.Light.InternallyProjective

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRing