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.groupWithZero
{α : Type u}
{β : Type v}
{φ : Ultrafilter α}
[GroupWithZero β]
:
GroupWithZero (Filter.Germ (↑φ) β)
instance
Filter.Germ.divisionSemiring
{α : Type u}
{β : Type v}
{φ : Ultrafilter α}
[DivisionSemiring β]
:
DivisionSemiring (Filter.Germ (↑φ) β)
instance
Filter.Germ.divisionRing
{α : Type u}
{β : Type v}
{φ : Ultrafilter α}
[DivisionRing β]
:
DivisionRing (Filter.Germ (↑φ) β)
instance
Filter.Germ.semifield
{α : Type u}
{β : Type v}
{φ : Ultrafilter α}
[Semifield β]
:
Semifield (Filter.Germ (↑φ) β)
instance
Filter.Germ.field
{α : Type u}
{β : Type v}
{φ : Ultrafilter α}
[Field β]
:
Field (Filter.Germ (↑φ) β)
theorem
Filter.Germ.coe_lt
{α : Type u}
{β : Type v}
{φ : Ultrafilter α}
[Preorder β]
{f : α → β}
{g : α → β}
:
theorem
Filter.Germ.coe_pos
{α : Type u}
{β : Type v}
{φ : Ultrafilter α}
[Preorder β]
[Zero β]
{f : α → β}
:
theorem
Filter.Germ.const_lt
{α : Type u}
{β : Type v}
{φ : Ultrafilter α}
[Preorder β]
{x : β}
{y : β}
:
@[simp]
theorem
Filter.Germ.const_lt_iff
{α : Type u}
{β : Type v}
{φ : Ultrafilter α}
[Preorder β]
{x : β}
{y : β}
:
theorem
Filter.Germ.lt_def
{α : Type u}
{β : Type v}
{φ : Ultrafilter α}
[Preorder β]
:
(fun x x_1 => 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 (Filter.Germ (↑φ) β) fun x x_1 => x ≤ x_1
noncomputable instance
Filter.Germ.linearOrder
{α : Type u}
{β : Type v}
{φ : Ultrafilter α}
[LinearOrder β]
:
LinearOrder (Filter.Germ (↑φ) β)
If φ
is an ultrafilter then the ultraproduct is a linear order.
theorem
Filter.Germ.linearOrderedAddCommGroup.proof_2
{α : Type u_2}
{β : Type u_1}
{φ : Ultrafilter α}
[LinearOrderedAddCommGroup β]
(a : Filter.Germ (↑φ) β)
(b : Filter.Germ (↑φ) β)
:
theorem
Filter.Germ.linearOrderedAddCommGroup.proof_3
{α : Type u_2}
{β : Type u_1}
{φ : Ultrafilter α}
[LinearOrderedAddCommGroup β]
(a : Filter.Germ (↑φ) β)
(b : Filter.Germ (↑φ) β)
:
noncomputable instance
Filter.Germ.linearOrderedAddCommGroup
{α : Type u}
{β : Type v}
{φ : Ultrafilter α}
[LinearOrderedAddCommGroup β]
:
LinearOrderedAddCommGroup (Filter.Germ (↑φ) β)
theorem
Filter.Germ.linearOrderedAddCommGroup.proof_1
{α : Type u_2}
{β : Type u_1}
{φ : Ultrafilter α}
[LinearOrderedAddCommGroup β]
(a : Filter.Germ (↑φ) β)
(b : Filter.Germ (↑φ) β)
:
a ≤ b → ∀ (c : Filter.Germ (↑φ) β), c + a ≤ c + b
theorem
Filter.Germ.linearOrderedAddCommGroup.proof_4
{α : Type u_2}
{β : Type u_1}
{φ : Ultrafilter α}
[LinearOrderedAddCommGroup β]
(a : Filter.Germ (↑φ) β)
(b : Filter.Germ (↑φ) β)
:
theorem
Filter.Germ.linearOrderedAddCommGroup.proof_5
{α : Type u_2}
{β : Type u_1}
{φ : Ultrafilter α}
[LinearOrderedAddCommGroup β]
(a : Filter.Germ (↑φ) β)
(b : Filter.Germ (↑φ) β)
:
compare a b = compareOfLessAndEq a b
noncomputable instance
Filter.Germ.linearOrderedCommGroup
{α : Type u}
{β : Type v}
{φ : Ultrafilter α}
[LinearOrderedCommGroup β]
:
LinearOrderedCommGroup (Filter.Germ (↑φ) β)
instance
Filter.Germ.strictOrderedSemiring
{α : Type u}
{β : Type v}
{φ : Ultrafilter α}
[StrictOrderedSemiring β]
:
StrictOrderedSemiring (Filter.Germ (↑φ) β)
instance
Filter.Germ.strictOrderedCommSemiring
{α : Type u}
{β : Type v}
{φ : Ultrafilter α}
[StrictOrderedCommSemiring β]
:
StrictOrderedCommSemiring (Filter.Germ (↑φ) β)
instance
Filter.Germ.strictOrderedRing
{α : Type u}
{β : Type v}
{φ : Ultrafilter α}
[StrictOrderedRing β]
:
StrictOrderedRing (Filter.Germ (↑φ) β)
instance
Filter.Germ.strictOrderedCommRing
{α : Type u}
{β : Type v}
{φ : Ultrafilter α}
[StrictOrderedCommRing β]
:
StrictOrderedCommRing (Filter.Germ (↑φ) β)
noncomputable instance
Filter.Germ.linearOrderedRing
{α : Type u}
{β : Type v}
{φ : Ultrafilter α}
[LinearOrderedRing β]
:
LinearOrderedRing (Filter.Germ (↑φ) β)
noncomputable instance
Filter.Germ.linearOrderedField
{α : Type u}
{β : Type v}
{φ : Ultrafilter α}
[LinearOrderedField β]
:
LinearOrderedField (Filter.Germ (↑φ) β)
noncomputable instance
Filter.Germ.linearOrderedCommRing
{α : Type u}
{β : Type v}
{φ : Ultrafilter α}
[LinearOrderedCommRing β]
:
LinearOrderedCommRing (Filter.Germ (↑φ) β)
theorem
Filter.Germ.max_def
{α : Type u}
{β : Type v}
{φ : Ultrafilter α}
[LinearOrder β]
(x : Filter.Germ (↑φ) β)
(y : Filter.Germ (↑φ) β)
:
max x y = Filter.Germ.map₂ max x y
theorem
Filter.Germ.min_def
{α : Type u}
{β : Type v}
{φ : Ultrafilter α}
[K : LinearOrder β]
(x : Filter.Germ (↑φ) β)
(y : Filter.Germ (↑φ) β)
:
min x y = Filter.Germ.map₂ min x y
theorem
Filter.Germ.abs_def
{α : Type u}
{β : Type v}
{φ : Ultrafilter α}
[LinearOrderedAddCommGroup β]
(x : Filter.Germ (↑φ) β)
:
|x| = Filter.Germ.map abs x
@[simp]
theorem
Filter.Germ.const_max
{α : Type u}
{β : Type v}
{φ : Ultrafilter α}
[LinearOrder β]
(x : β)
(y : β)
:
@[simp]
theorem
Filter.Germ.const_min
{α : Type u}
{β : Type v}
{φ : Ultrafilter α}
[LinearOrder β]
(x : β)
(y : β)
:
@[simp]
theorem
Filter.Germ.const_abs
{α : Type u}
{β : Type v}
{φ : Ultrafilter α}
[LinearOrderedAddCommGroup β]
(x : β)
:
↑|x| = |↑x|