# mathlibdocumentation

order.filter.filter_product

# 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

def filter.germ.division_ring {α : Type u} {β : Type v} {φ : filter α}  :

If φ is an ultrafilter then the ultraproduct is a division ring. This cannot be an instance, since it depends on φ being an ultrafilter.

Equations
def filter.germ.field {α : Type u} {β : Type v} {φ : filter α} [field β] :
φ.is_ultrafilterfield (φ.germ β)

If φ is an ultrafilter then the ultraproduct is a field. This cannot be an instance, since it depends on φ being an ultrafilter.

Equations
def filter.germ.linear_order {α : Type u} {β : Type v} {φ : filter α} [linear_order β] :

If φ is an ultrafilter then the ultraproduct is a linear order. This cannot be an instance, since it depends on φ being an ultrafilter.

Equations
@[simp]
theorem filter.germ.const_div {α : Type u} {β : Type v} {φ : filter α} (U : φ.is_ultrafilter) (x y : β) :
(x / y) = x / y

theorem filter.germ.coe_lt {α : Type u} {β : Type v} {φ : filter α} [preorder β] (U : φ.is_ultrafilter) {f g : α → β} :
f < g ∀ᶠ (x : α) in φ, f x < g x

theorem filter.germ.coe_pos {α : Type u} {β : Type v} {φ : filter α} [preorder β] [has_zero β] (U : φ.is_ultrafilter) {f : α → β} :
0 < f ∀ᶠ (x : α) in φ, 0 < f x

theorem filter.germ.const_lt {α : Type u} {β : Type v} {φ : filter α} [preorder β] (U : φ.is_ultrafilter) {x y : β} :
x < y x < y

theorem filter.germ.lt_def {α : Type u} {β : Type v} {φ : filter α} [preorder β] :

theorem filter.germ.le_def {α : Type u} {β : Type v} {φ : filter α} [preorder β] :

def filter.germ.ordered_ring {α : Type u} {β : Type v} {φ : filter α} [ordered_ring β] :

If φ is an ultrafilter then the ultraproduct is an ordered ring. This cannot be an instance, since it depends on φ being an ultrafilter.

Equations
def filter.germ.linear_ordered_ring {α : Type u} {β : Type v} {φ : filter α}  :

If φ is an ultrafilter then the ultraproduct is a linear ordered ring. This cannot be an instance, since it depends on φ being an ultrafilter.

Equations
def filter.germ.linear_ordered_field {α : Type u} {β : Type v} {φ : filter α}  :

If φ is an ultrafilter then the ultraproduct is a linear ordered field. This cannot be an instance, since it depends on φ being an ultrafilter.

Equations
def filter.germ.linear_ordered_comm_ring {α : Type u} {β : Type v} {φ : filter α}  :

If φ is an ultrafilter then the ultraproduct is a linear ordered commutative ring. This cannot be an instance, since it depends on φ being an ultrafilter.

Equations
def filter.germ.decidable_linear_order {α : Type u} {β : Type v} {φ : filter α}  :

If φ is an ultrafilter then the ultraproduct is a decidable linear order. This cannot be an instance, since it depends on φ being an ultrafilter.

Equations
def filter.germ.decidable_linear_ordered_add_comm_group {α : Type u} {β : Type v} {φ : filter α}  :

If φ is an ultrafilter then the ultraproduct is a decidable linear ordered commutative group. This cannot be an instance, since it depends on φ being an ultrafilter.

Equations
def filter.germ.decidable_linear_ordered_comm_ring {α : Type u} {β : Type v} {φ : filter α}  :

If φ is an ultrafilter then the ultraproduct is a decidable linear ordered commutative ring. This cannot be an instance, since it depends on φ being an ultrafilter.

Equations
def filter.germ.discrete_linear_ordered_field {α : Type u} {β : Type v} {φ : filter α}  :

If φ is an ultrafilter then the ultraproduct is a discrete linear ordered field. This cannot be an instance, since it depends on φ being an ultrafilter.

Equations
theorem filter.germ.max_def {α : Type u} {β : Type v} {φ : filter α} [K : decidable_linear_order β] (U : φ.is_ultrafilter) (x y : φ.germ β) :
max x y =

theorem filter.germ.min_def {α : Type u} {β : Type v} {φ : filter α} [K : decidable_linear_order β] (U : φ.is_ultrafilter) (x y : φ.germ β) :
min x y =

theorem filter.germ.abs_def {α : Type u} {β : Type v} {φ : filter α} (U : φ.is_ultrafilter) (x : φ.germ β) :

@[simp]
theorem filter.germ.const_max {α : Type u} {β : Type v} {φ : filter α} (U : φ.is_ultrafilter) (x y : β) :
(max x y) = max x y

@[simp]
theorem filter.germ.const_min {α : Type u} {β : Type v} {φ : filter α} (U : φ.is_ultrafilter) (x y : β) :
(min x y) = min x y

@[simp]
theorem filter.germ.const_abs {α : Type u} {β : Type v} {φ : filter α} (U : φ.is_ultrafilter) (x : β) :