English
Let X,Y be light condensed objects and f: X → Y a morphism. Then for every S,T in LightProfinite^op and every g: S → T, and every x ∈ X(S), we have f_T(X(g)(x)) = Y(g)(f_S(x)).
Русский
Пусть X,Y — светло-конденсированные объекты и f: X → Y — морфизм. Тогда для любых S,T в LightProfinite^op и любого g: S → T, а также любого x ∈ X(S) выполняется f_T(X(g)(x)) = Y(g)(f_S(x)).
LaTeX
$$$\forall S,T \in \text{LightProfinite}^{op},\; g:S\to T,\; x\in X(S):\quad f_T\big(X(g)(x)\big) = Y(g)\big(f_S(x)\big).$$$
Lean4
@[simp]
theorem hom_naturality_apply {X Y : LightCondSet.{u}} (f : X ⟶ Y) {S T : LightProfiniteᵒᵖ} (g : S ⟶ T)
(x : X.val.obj S) : f.val.app T (X.val.map g x) = Y.val.map g (f.val.app S x) :=
NatTrans.naturality_apply f.val g x
