Theorems · Theorem · category theory

LightCondensed.ihomPoints_symm_comp

∀ (R : Type u) [inst : CommRing R] (B P : LightCondMod R) (S S' : LightProfinite) (π : S ⟶ S')
  (f : CategoryTheory.MonoidalCategoryStruct.tensorObj P ((LightCondensed.free R).obj S'.toCondensed) ⟶ B),
  (LightCondensed.ihomPoints R P B S).symm
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P
          ((LightCondensed.free R).map (lightProfiniteToLightCondSet.map π)))
        f) =
    (CategoryTheory.ConcreteCategory.hom ((P ⟹ B).obj.map π.op)) ((LightCondensed.ihomPoints R P B S').symm f)

Defined in

Mathlib.Condensed.Light.InternallyProjective

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRing