English
Let R be a ring and X,Y be LightCondMod_R. For any morphism f: X ⟶ Y and any S,T in LightProfiniteᵒᵖ with g:S ⟶ T and any x ∈ X(S), the equality f.val.app T (X.val.map g x) = Y.val.map g (f.val.app S x) holds; i.e., the naturality square commutes.
Русский
Пусть R — кольцо и X,Y — LightCondMod_R. Пусть f: X ⟶ Y и для любых S,T из LightProfiniteᵒᵖ с г : S ⟶ T и любого x ∈ X(S) выполняется равенство f.val.app T (X.val.map g x) = Y.val.map g (f.val.app S x). Это условие натуральности преобразования.
LaTeX
$$$ f_T(X.map(g)(x)) = Y.map(g)(f_S(x)) $$$
Lean4
theorem hom_naturality_apply {X Y : LightCondMod.{u} R} (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
