Theorems · Theorem · category theory

LightCondensed.forget_map_hom_app_hom_apply

∀ (R : Type u) [inst : Ring R] {X Y : LightCondMod R} (f : X ⟶ Y) (S : LightProfiniteᵒᵖ)
  (a :
    ↑(((CategoryTheory.sheafToPresheaf (CategoryTheory.coherentTopology LightProfinite) (ModuleCat R)).obj X).obj S)),
  (CategoryTheory.ConcreteCategory.hom (((LightCondensed.forget R).map f).hom.app S)) a =
    (CategoryTheory.ConcreteCategory.hom (f.hom.app S)) a

Defined in

Mathlib.Condensed.Light.Module

Cited by

0 results in Mathlib

Foundations

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

Assumes

Ring