Ultraproducts

If φ is an ultrafilter, then the space of germs of functions f : α → β at φ is called the ultraproduct. In this file we prove properties of ultraproducts that rely on φ being an ultrafilter. Definitions and properties that work for any filter should go to Order.Filter.Germ.

Tags

ultrafilter, ultraproduct

instance Filter.Germ.instGroupWithZero {α : Type u} {β : Type v} {φ : Ultrafilter α} [GroupWithZero β] : GroupWithZero ((↑φ).Germ β)

instance Filter.Germ.instDivisionSemiring {α : Type u} {β : Type v} {φ : Ultrafilter α} [DivisionSemiring β] : DivisionSemiring ((↑φ).Germ β)

instance Filter.Germ.instDivisionRing {α : Type u} {β : Type v} {φ : Ultrafilter α} [DivisionRing β] : DivisionRing ((↑φ).Germ β)

instance Filter.Germ.instSemifield {α : Type u} {β : Type v} {φ : Ultrafilter α} [Semifield β] : Semifield ((↑φ).Germ β)

instance Filter.Germ.instField {α : Type u} {β : Type v} {φ : Ultrafilter α} [Field β] : Field ((↑φ).Germ β)

theorem Filter.Germ.coe_lt {α : Type u} {β : Type v} {φ : Ultrafilter α} [Preorder β] {f g : α → β} : ↑f < ↑g ↔ ∀ᶠ (x : α) in ↑φ, f x < g x

theorem Filter.Germ.coe_pos {α : Type u} {β : Type v} {φ : Ultrafilter α} [Preorder β] [Zero β] {f : α → β} : 0 < ↑f ↔ ∀ᶠ (x : α) in ↑φ, 0 < f x

theorem Filter.Germ.const_lt {α : Type u} {β : Type v} {φ : Ultrafilter α} [Preorder β] {x y : β} : x < y → ↑x < ↑y

@[simp]

theorem Filter.Germ.const_lt_iff {α : Type u} {β : Type v} {φ : Ultrafilter α} [Preorder β] {x y : β} : ↑x < ↑y ↔ x < y

theorem Filter.Germ.lt_def {α : Type u} {β : Type v} {φ : Ultrafilter α} [Preorder β] : (fun (x1 x2 : (↑φ).Germ β) => x1 < x2) = LiftRel fun (x1 x2 : β) => x1 < x2

instance Filter.Germ.isTotal {α : Type u} {β : Type v} {φ : Ultrafilter α} [LE β] [IsTotal β fun (x1 x2 : β) => x1 ≤ x2] : IsTotal ((↑φ).Germ β) fun (x1 x2 : (↑φ).Germ β) => x1 ≤ x2

noncomputable instance Filter.Germ.instLinearOrder {α : Type u} {β : Type v} {φ : Ultrafilter α} [LinearOrder β] : LinearOrder ((↑φ).Germ β)

If φ is an ultrafilter then the ultraproduct is a linear order.

instance Filter.Germ.instIsStrictOrderedRing {α : Type u} {β : Type v} {φ : Ultrafilter α} [Semiring β] [PartialOrder β] [IsStrictOrderedRing β] : IsStrictOrderedRing ((↑φ).Germ β)

theorem Filter.Germ.max_def {α : Type u} {β : Type v} {φ : Ultrafilter α} [LinearOrder β] (x y : (↑φ).Germ β) : max x y = map₂ max x y

theorem Filter.Germ.min_def {α : Type u} {β : Type v} {φ : Ultrafilter α} [K : LinearOrder β] (x y : (↑φ).Germ β) : min x y = map₂ min x y

theorem Filter.Germ.abs_def {α : Type u} {β : Type v} {φ : Ultrafilter α} [AddCommGroup β] [LinearOrder β] (x : (↑φ).Germ β) : |x| = map abs x

@[simp]

theorem Filter.Germ.const_max {α : Type u} {β : Type v} {φ : Ultrafilter α} [LinearOrder β] (x y : β) : ↑(max x y) = max ↑x ↑y

@[simp]

theorem Filter.Germ.const_min {α : Type u} {β : Type v} {φ : Ultrafilter α} [LinearOrder β] (x y : β) : ↑(min x y) = min ↑x ↑y

@[simp]

theorem Filter.Germ.const_abs {α : Type u} {β : Type v} {φ : Ultrafilter α} [AddCommGroup β] [LinearOrder β] (x : β) : ↑|x| = |↑x|