Skip to content

Instantly share code, notes, and snippets.

@dwarn
Created April 30, 2020 11:14
Show Gist options
  • Save dwarn/35d168349a298d3312534fe622c7f56e to your computer and use it in GitHub Desktop.
Save dwarn/35d168349a298d3312534fe622c7f56e to your computer and use it in GitHub Desktop.
applicative ultrapower
import order.filter.filter_product
import category_theory.category.default -- for the `tidy` tactic
open filter filter.filter_product
noncomputable theory
/-- The ultrapower of a `Type`. -/
def upower (α : Type*) := filterprod α (@hyperfilter ℕ)
/-- We think of inhabitants of upower (α → β) as nonstandard functions internal
to the theory; this definition lets us use them as functions.
This is `<*>` but with two distinct universe parameters. -/
def upower.seq ⦃α β : Type*⦄ : upower (α → β) → upower α → upower β :=
λ fs as, quotient.lift_on₂' fs as (λ f a, of_seq $ λ i, (f i) (a i))
begin
intros f₁ as₁ f₂ as₂ hf has,
apply quotient.sound,
filter_upwards [hf, has],
intros i hif hias,
change _ = _ at hias,
change _ = _ at hif,
change _ = _,
simp only [hias, hif],
end
/-- This is `<$>` but with two distinct universe parameters. -/
def upower.map {α β : Type*} (f : α → β) : upower α → upower β := upower.seq (of f)
instance : applicative upower := { pure := λ _, of, seq := upower.seq }
instance : is_lawful_functor upower := by tidy
instance : is_lawful_applicative upower := by tidy
/-- We can now easily lift functions to ultraproducts.
But how do we prove things about the lifts? -/
example {α} [has_add α] : has_add (upower α) :=
{ add := λ a b, (+) <$> a <*> b }
/-- This is true, but does not follow from the applicative laws; it fails for `Option`. -/
example {α β} (b : β) (as : upower α) : (λ _, b) <$> as = pure b := sorry
/-- Ultrapowers don't give us any new `Prop`s. -/
lemma prop_equiv : upower Prop ≃ Prop :=
{ to_fun := λ ps, ps = pure true,
inv_fun := pure,
left_inv := sorry,
right_inv := sorry, }
/-- More generally, we don't get new elements in any fintype. -/
example {α} [fintype α] : function.bijective (pure : α → upower α) := sorry
/-- Equipped with `prop_equiv`, we can also lift relations. -/
example {α} [has_le α] : has_le (upower α) :=
{ le := λ x y, prop_equiv $ (≤) <$> x <*> y }
example {α} (x y : upower α) : x = y ↔ prop_equiv ((=) <$> x <*> y) := sorry
universes u v
/-- We can view an inhbaitant of `upower (Type u)` as a geniune type. -/
instance : has_coe_to_sort (upower $ Type u) :=
{ S := Type (u+1),
coe := λ as, { ps : upower (Σ α : Type u, α) // (λ p : (Σ α, α), p.fst) <$> ps = as } }
/-- There are two equivalent ways of turning a type into a nonstandard type.-/
def hyp_equiv {α : Type u} : upower α ≃ ↥(pure α : upower (Type u)) :=
{ to_fun := λ x, ⟨upower.map (λ a, ⟨α, a⟩) x, sorry⟩,
inv_fun := λ ⟨ps, h⟩, sorry, -- this should be some eq.rec nonsense
left_inv := sorry,
right_inv := sorry, }
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment