(ultra)product

Stream: general

[Kenny Lau]

import order.filter

universes u v

variables {α : Type u} (β : Type v) (f : filter α)

def bigly_equal : setoid (α → β) :=
⟨ λ a b, {n | a n = b n} ∈ f.sets,
  λ a, by simp only [eq_self_iff_true]; exact f.2,
  λ a b ab, by simpa only [eq_comm],
  λ a b c ab bc, by filter_upwards [ab, bc] λ n hn1 hn2, hn1.trans hn2⟩

def something := quotient $ bigly_equal β f

instance [add_semigroup β] : add_semigroup (something β f) :=
{ add := λ x y, quotient.lift_on₂' x y (λ a b, (quotient.mk' $ λ n, a n + b n : something β f)) $
    λ a₁ a₂ b₁ b₂ h1 h2, quotient.sound' $ show _ ∈ _,
    by filter_upwards [h1, h2] λ i hi1 hi2, congr (congr_arg _ hi1) hi2,
  add_assoc := λ x y z, quotient.induction_on₃' x y z $ λ a b c, quotient.sound' $
    show {n | _+_+_ = _+(_+_)} ∈ _, by simp only [add_assoc, eq_self_iff_true]; exact f.2 }

[Kenny Lau]

might this be useful / worth it to add to mathlib?

[Kenny Lau]

(credits for parts of the code go to @Abhimanyu Pallavi Sudhir)

[Abhimanyu Pallavi Sudhir]

Oh, is that useful on its own accord (besides just for defining the hyperreals)?

[Kenny Lau]

yes, it's the ultraproduct in model theory

[Abhimanyu Pallavi Sudhir]

Btw, I thought you didn't like tactics.

[Kevin Buzzard]

Can one formalise Los' theorem in Lean? It says something like a first order statement that's true in the factors is true in the ultraproduct

[Kevin Buzzard]

Maybe it says something stronger -- maybe something is true in the ultraproduct iff it's true in a "big" set of the factors. The problem is that IIRC it's only true for certain kinds of statements.

[Kenny Lau]

who said I didn't like tactic?

[Kenny Lau]

@Kevin Buzzard that would require... formalizing first order statements

[Kenny Lau]

I love filter_upwards btw, shoutout to @Johannes Hölzl

[Kevin Buzzard]

Oh here we go -- https://en.wikipedia.org/wiki/Ultraproduct#.C5.81o.C5.9B.27_theorem, it's mentioned in the wikipedia page on ultraproducts. Yeah, something's true in the ultraproduct iff it's true in a big set of factors.

[Kevin Buzzard]

Oh that's interesting, it mentions the "transfer principle" https://en.wikipedia.org/wiki/Transfer_principle . Is this related to rewriting isomorphisms of rings?

[Kenny Lau]

One of the first examples was the Lefschetz principle, which states that any sentence in the first-order language of fields that is true for the complex numbers is also true for any algebraically closed field of characteristic 0.

[Kenny Lau]

i.e. no

[Kevin Buzzard]

But we have this issue in Lean that any "reasonable mathematical statement" about rings is true for R iff it's true for any ring isomorphic to R, and the problem with formalising this is that the computer scientists can't seem to formalise the notion of "reasonable mathematical statement". E.g. the predicate "I am equal to R" is not such a statement.

[Kevin Buzzard]

So the underlying issue is the same -- we want to move statements from one structure to another but we can only move certain statements.

[Chris Hughes]

If I define cycle shape on finite permutations as a multiset nat, computably over an arbitrary fintype without a linear order assumption, is it "obvious" that conjugate permutations have the same cycle type, since conjugation is an isomorphism?

[Kevin Buzzard]

This is in the wrong thread. If you know that the map from permutations to cycle shapes factors through partitions (via the map sending a permutation to its orbits) and if you know that isomorphic partitions have the same cycle shape then it follows, because the conjugating element h maps orbits for g to orbits for hgh^-1

[Chris Hughes]

I know the proof, but does it count as obvious?

[Kevin Buzzard]

This is in the wrong thread. Can you fix it? One could imagine the category of pairs consisting of a finite set and a partition of that set into non-empty subsets. One would have to say what the morphisms were. One could say they were isomorphisms. Your construction of a multiset of nats is mathematically sensible, a notion which I do not know how to define in Lean. Because it is mathematically sensible it is constant on isomorphism classes. This is obvious to me but apparently not to Lean.

[Kevin Buzzard]

It's a transfer problem. At the minute we have to prove these ourselves

[Kevin Buzzard]

Maybe this isn't in the wrong thread after all

[Kevin Buzzard]

Abhi's original motivation for hyperreals was that they might give another approach to calculus, but if for every single first order lemma he has to explicitly prove that it's true in the reals iff it's true in the hyperreals then it will be slow going

[Kevin Buzzard]

One has to be really careful here. For example the hyperreals will be a ring so Lean will have access to a map from the integers into that ring, but you're not allowed to use that map in your theorems because it can't be made from the first order theory of reals alone

[Kevin Buzzard]

So you can't ask the question "does there exist something bigger than every nat?" which is true in one and false in the other

[Kenny Lau]

so my point stands, one would need to formalize first order logic

[Kevin Buzzard]

Right

[Kevin Buzzard]

It's a special case of the notion of being mathematically sensible

[Neil Strickland]

If f is the neighbourhood filter at a point xin a topological space, then the equivalence classes would normally be called germs at x. If f is an ultrafilter then you can think of the equivalence classes as germs at a point in the Stone-Cech compactification. So I would suggest naming things in a way that is compatible with that. Also, I think it would be better to do a dependent version with β : α → Type rather than β : Type.

[Jesse Michael Han]

Los' theorem is a (relatively low-priority) item on the Flypitch to-do list. It would be nice to have the hyperreals as a setting for nonstandard analysis in Lean.

There is a related statement for collapsing Boolean-valued models to 2-valued ones, but we won't need it.

This is related to a transfer principle in the sense that if the ultraproduct is an ultrapower, then the diagonal embedding is elementary and first-order statements can be transferred.

@Kenny Lau, I think proving Los' theorem would be a pleasant exercise in using Flypitch's FOL library, so feel free to PR it :^)