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
- One or more equations did not get rendered due to their size.
instance
Filter.Germ.instDivisionSemiring
{α : Type u}
{β : Type v}
{φ : Ultrafilter α}
[DivisionSemiring β]
:
DivisionSemiring ((↑φ).Germ β)
Equations
- One or more equations did not get rendered due to their size.
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.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
Filter.Germ.const_lt_iff
{α : Type u}
{β : Type v}
{φ : Ultrafilter α}
[Preorder β]
{x y : β}
:
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
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 β)
:
theorem
Filter.Germ.min_def
{α : Type u}
{β : Type v}
{φ : Ultrafilter α}
[K : LinearOrder β]
(x y : (↑φ).Germ β)
:
theorem
Filter.Germ.abs_def
{α : Type u}
{β : Type v}
{φ : Ultrafilter α}
[AddCommGroup β]
[LinearOrder β]
(x : (↑φ).Germ β)
:
@[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 α}
[AddCommGroup β]
[LinearOrder β]
(x : β)
: