Just want to attempt to check if my understanding/intuition for the construction of the Hyperreal numbers via an ultraproduct is correct. Appreciate any corrections or help.
So Hyperreals are constructed by using a non-principal ultrafilter. Which is essentially a tool that obeys several properties the most important (for being non-prinipal) of which is no finite subsets are contained in the ultrafilter.
It can also be shown that a filter can be extended to an ultrafilter (via Zorn's lemma) and can therefore be turned into an non-principal ultrafilter if we simply take the filter consisting of all cofinite sets and extend that to be an ultrafilter.
using this non-prinicpal ultrafilter an equivalence relation is constructed on real-valued sequences. (The equivalence relation being the "size of two real-valued sequences agree and belong to the non-prinicpal ultrafilter"). This will essentially allow the set to be partitioned into pieces. Since we have an equivalence relation it is then easy to get the various equivalence classes.
Once we have the equivalence relation to get the Hypperreal numbers we take the quotient of the set of real-valued sequences with the equivalence relation. (is this similar to a quotient set, apart from the real-valued sequences form a ring, so it's a quotient ring; not sure on the name for it?).
Thanks for reading and pointing out any holes if there are any.