Zulip Chat Archive
Stream: maths
Topic: Ultraproducts
Aaron Anderson (Mar 08 2022 at 00:10):
I have just defined and proved things about ultraproducts in model theory at branch#homebrew_ultraproduct.
Aaron Anderson (Mar 08 2022 at 00:12):
The branch has that title because rather than using filter.germ, which is what @Abhimanyu Pallavi Sudhir and @Yury G. Kudryashov used for constructing the hyperreals, because I need the definition to be dependent. https://leanprover-community.github.io/mathlib_docs/order/filter/filter_product.html
Aaron Anderson (Mar 08 2022 at 00:13):
I would love to unite my definition more with the rest of the filter library, but modifying the definition of filter.eventually_eq to fit my purposes (unsurprisingly) led me into some trouble with a bunch of scattered topology files.
Aaron Anderson (Mar 08 2022 at 00:14):
People with more experience with filters outside of the order folder: Where should these definitions live, and at what generality should they be defined?
Adam Topaz (Mar 08 2022 at 00:41):
Los's theorem and compactess!?!?! Great job! :tada:
Adam Topaz (Mar 08 2022 at 00:44):
(Unfortunately I don't know how to typeset the Polish "L" on mobile)
Aaron Anderson (Mar 08 2022 at 00:50):
Since we're breaking out the :tada:, I should note that Compactness was proved in Flypitch (although I don't think Łoś's Theorem was - they went through Completeness)
Aaron Anderson (Mar 08 2022 at 16:31):
For now I have renamed my ultraproduct construction filter.product and placed it in filter/germ next to the non-dependent germ (ultrapower) construction. I'll PR it like that for now.
Aaron Anderson (Mar 08 2022 at 16:38):
Last updated: Dec 20 2023 at 11:08 UTC