Documentation

Mathlib.Order.Filter.FilterProduct

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 β)
Equations
  • Filter.Germ.instGroupWithZero = let __spread.0 := Filter.Germ.instDivInvMonoid; let __spread.1 := Filter.Germ.instMonoidWithZero; GroupWithZero.mk DivInvMonoid.zpow
instance Filter.Germ.instDivisionSemiring {α : Type u} {β : Type v} {φ : Ultrafilter α} [DivisionSemiring β] :
DivisionSemiring ((φ).Germ β)
Equations
  • Filter.Germ.instDivisionSemiring = let __spread.0 := Filter.Germ.instGroupWithZero; DivisionSemiring.mk GroupWithZero.zpow (fun (q : ℚ≥0) => HMul.hMul q)
instance Filter.Germ.instDivisionRing {α : Type u} {β : Type v} {φ : Ultrafilter α} [DivisionRing β] :
DivisionRing ((φ).Germ β)
Equations
  • One or more equations did not get rendered due to their size.
instance Filter.Germ.instSemifield {α : Type u} {β : Type v} {φ : Ultrafilter α} [Semifield β] :
Semifield ((φ).Germ β)
Equations
  • One or more equations did not get rendered due to their size.
instance Filter.Germ.instField {α : Type u} {β : Type v} {φ : Ultrafilter α} [Field β] :
Field ((φ).Germ β)
Equations
  • One or more equations did not get rendered due to their size.
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 < yx < 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 (x x_1 : (φ).Germ β) => x < x_1) = Filter.Germ.LiftRel fun (x x_1 : β) => x < x_1
instance Filter.Germ.isTotal {α : Type u} {β : Type v} {φ : Ultrafilter α} [LE β] [IsTotal β fun (x x_1 : β) => x x_1] :
IsTotal ((φ).Germ β) fun (x x_1 : (φ).Germ β) => x x_1
Equations
  • =
noncomputable instance Filter.Germ.instLinearOrder {α : Type u} {β : Type v} {φ : Ultrafilter α} [LinearOrder β] :
LinearOrder ((φ).Germ β)

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

Equations
theorem Filter.Germ.linearOrderedAddCommGroup.proof_2 {α : Type u_1} {β : Type u_2} {φ : Ultrafilter α} [LinearOrderedAddCommGroup β] (a : (φ).Germ β) (b : (φ).Germ β) :
min a b = if a b then a else b
theorem Filter.Germ.linearOrderedAddCommGroup.proof_3 {α : Type u_1} {β : Type u_2} {φ : Ultrafilter α} [LinearOrderedAddCommGroup β] (a : (φ).Germ β) (b : (φ).Germ β) :
max a b = if a b then b else a
theorem Filter.Germ.linearOrderedAddCommGroup.proof_1 {α : Type u_1} {β : Type u_2} {φ : Ultrafilter α} [LinearOrderedAddCommGroup β] (a : (φ).Germ β) (b : (φ).Germ β) :
a b b a
theorem Filter.Germ.linearOrderedAddCommGroup.proof_4 {α : Type u_1} {β : Type u_2} {φ : Ultrafilter α} [LinearOrderedAddCommGroup β] (a : (φ).Germ β) (b : (φ).Germ β) :
noncomputable instance Filter.Germ.linearOrderedAddCommGroup {α : Type u} {β : Type v} {φ : Ultrafilter α} [LinearOrderedAddCommGroup β] :
LinearOrderedAddCommGroup ((φ).Germ β)
Equations
  • One or more equations did not get rendered due to their size.
noncomputable instance Filter.Germ.linearOrderedCommGroup {α : Type u} {β : Type v} {φ : Ultrafilter α} [LinearOrderedCommGroup β] :
LinearOrderedCommGroup ((φ).Germ β)
Equations
  • One or more equations did not get rendered due to their size.
instance Filter.Germ.instStrictOrderedSemiring {α : Type u} {β : Type v} {φ : Ultrafilter α} [StrictOrderedSemiring β] :
StrictOrderedSemiring ((φ).Germ β)
Equations
  • Filter.Germ.instStrictOrderedSemiring = let __spread.0 := Filter.Germ.instOrderedSemiring; let __spread.1 := Filter.Germ.instOrderedAddCancelCommMonoid; StrictOrderedSemiring.mk
Equations
  • Filter.Germ.instStrictOrderedCommSemiring = let __spread.0 := Filter.Germ.instStrictOrderedSemiring; let __spread.1 := Filter.Germ.instOrderedCommSemiring; StrictOrderedCommSemiring.mk
instance Filter.Germ.instStrictOrderedRing {α : Type u} {β : Type v} {φ : Ultrafilter α} [StrictOrderedRing β] :
StrictOrderedRing ((φ).Germ β)
Equations
  • Filter.Germ.instStrictOrderedRing = let __spread.0 := Filter.Germ.instRing; let __spread.1 := Filter.Germ.instStrictOrderedSemiring; StrictOrderedRing.mk
instance Filter.Germ.instStrictOrderedCommRing {α : Type u} {β : Type v} {φ : Ultrafilter α} [StrictOrderedCommRing β] :
StrictOrderedCommRing ((φ).Germ β)
Equations
  • Filter.Germ.instStrictOrderedCommRing = let __spread.0 := Filter.Germ.instStrictOrderedRing; let __spread.1 := Filter.Germ.instOrderedCommRing; StrictOrderedCommRing.mk
noncomputable instance Filter.Germ.instLinearOrderedRing {α : Type u} {β : Type v} {φ : Ultrafilter α} [LinearOrderedRing β] :
LinearOrderedRing ((φ).Germ β)
Equations
  • One or more equations did not get rendered due to their size.
noncomputable instance Filter.Germ.instLinearOrderedField {α : Type u} {β : Type v} {φ : Ultrafilter α} [LinearOrderedField β] :
LinearOrderedField ((φ).Germ β)
Equations
  • One or more equations did not get rendered due to their size.
noncomputable instance Filter.Germ.instLinearOrderedCommRing {α : Type u} {β : Type v} {φ : Ultrafilter α} [LinearOrderedCommRing β] :
LinearOrderedCommRing ((φ).Germ β)
Equations
  • Filter.Germ.instLinearOrderedCommRing = let __spread.0 := Filter.Germ.instLinearOrderedRing; let __spread.1 := Filter.Germ.instCommMonoid; LinearOrderedCommRing.mk
theorem Filter.Germ.max_def {α : Type u} {β : Type v} {φ : Ultrafilter α} [LinearOrder β] (x : (φ).Germ β) (y : (φ).Germ β) :
theorem Filter.Germ.min_def {α : Type u} {β : Type v} {φ : Ultrafilter α} [K : LinearOrder β] (x : (φ).Germ β) (y : (φ).Germ β) :
theorem Filter.Germ.abs_def {α : Type u} {β : Type v} {φ : Ultrafilter α} [LinearOrderedAddCommGroup β] (x : (φ).Germ β) :
|x| = Filter.Germ.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 α} [LinearOrderedAddCommGroup β] (x : β) :
|x| = |x|