Structure Induced on Set of All Mappings to Ordered Semigroup is Ordered Semigroup

From ProofWiki
Jump to navigation Jump to search

Theorem

Let $S$ be a set.

Let $\struct {T, \odot, \preccurlyeq}$ be an ordered semigroup.

Let $\struct {T^S, \otimes, \preccurlyeq}$ denote the algebraic structure on $T^S$ induced by $\odot$.


Then $\struct {T^S, \otimes, \preccurlyeq}$ is an ordered semigroup.


Proof

From Structure Induced by Semigroup Operation is Semigroup, $\struct {T^S, \otimes}$ is a semigroup

From Ordered Set of All Mappings is Ordered Set, $\struct {T^S, \preccurlyeq}$ is an ordered set.


It remains to be demonstrated that $\preccurlyeq$ is compatible with $\odot$.


Let $f, g \in T^S$ such that $f \preccurlyeq g$.

That is:

$\forall x \in S: \map f x \preccurlyeq \map g x$


We are given that $\struct {T, \odot, \preccurlyeq}$ be an ordered semigroup.

Hence a fortiori $\preccurlyeq$ is compatible with $\odot$.

Thus:

\(\ds \forall h \in T^S: \, \) \(\ds \map h x \odot \map f x\) \(\preccurlyeq\) \(\ds \map h x \odot \map g x\) Definition of Relation Compatible with Operation
\(\, \ds \land \, \) \(\ds \map f x \odot \map h x\) \(\preccurlyeq\) \(\ds \map g x \odot \map h x\)
\(\ds \leadsto \ \ \) \(\ds f \otimes h\) \(\preccurlyeq\) \(\ds g \otimes h\) Definition of Pointwise Operation
\(\, \ds \land \, \) \(\ds h \otimes f\) \(\preccurlyeq\) \(\ds h \otimes g\)

Hence the result.

$\blacksquare$


Sources

Retrieved from "https://proofwiki.org/w/index.php?title=Structure_Induced_on_Set_of_All_Mappings_to_Ordered_Semigroup_is_Ordered_Semigroup&oldid=568032"