Theorems · Theorem · category theory

LightCondensed.ihom_map_val_app

∀ (R : Type u) [inst : CommRing R] (A B P : LightCondMod R) (S : LightProfinite) (e : A ⟶ B)
  (x : ↑((P ⟹ A).obj.obj (Opposite.op S))),
  (CategoryTheory.ConcreteCategory.hom (((CategoryTheory.ihom P).map e).hom.app (Opposite.op S))) x =
    (LightCondensed.ihomPoints R P B S).symm
      (CategoryTheory.CategoryStruct.comp ((LightCondensed.ihomPoints R P A S) x) e)

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