English
Let X, Y be condensed R-modules and f: X → Y a morphism. For any S → T in the opposite of CompHaus and any x ∈ X(S), the equality f_T (X.map g x) = Y.map g (f_S x) holds, expressing naturality of f with respect to base maps.
Русский
Пусть X, Y — конденсированные R-модули, f: X → Y — морфизм. Для любого g: S → T в противоположном CompHaus и любого x ∈ X(S) выполняется равенство f_T(X.map g(x)) = Y.map g(f_S(x)), т.е. естественность f по отношению к базовым отображениям.
LaTeX
$$$\forall f: X \to Y, \; \forall g: S \to T, \; x \in X(S),\; f_T\big(X.map\,g\,x\big) = Y.map\,g\big(f_S\,x\big)$$$
Lean4
theorem hom_naturality_apply {X Y : CondensedMod.{u} R} (f : X ⟶ Y) {S T : CompHausᵒᵖ} (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
