mathlib documentation

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

@[protected, instance]
def filter.germ.division_ring {α : Type u} {β : Type v} {φ : ultrafilter α} [division_ring β] :

If φ is an ultrafilter then the ultraproduct is a division ring.

Equations
@[protected, instance]
def filter.germ.field {α : Type u} {β : Type v} {φ : ultrafilter α} [field β] :
field (φ.germ β)

If φ is an ultrafilter then the ultraproduct is a field.

Equations
@[protected, instance]
noncomputable def filter.germ.linear_order {α : Type u} {β : Type v} {φ : ultrafilter α} [linear_order β] :

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

Equations
@[simp, norm_cast]
theorem filter.germ.const_div {α : Type u} {β : Type v} {φ : ultrafilter α} [division_ring β] (x y : β) :
(x / y) = x / y
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 β] [has_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
theorem filter.germ.lt_def {α : Type u} {β : Type v} {φ : ultrafilter α} [preorder β] :
@[protected, instance]
noncomputable def filter.germ.linear_ordered_ring {α : Type u} {β : Type v} {φ : ultrafilter α} [linear_ordered_ring β] :

If φ is an ultrafilter then the ultraproduct is a linear ordered ring.

Equations
@[protected, instance]
noncomputable def filter.germ.linear_ordered_field {α : Type u} {β : Type v} {φ : ultrafilter α} [linear_ordered_field β] :

If φ is an ultrafilter then the ultraproduct is a linear ordered field.

Equations
@[protected, instance]
noncomputable def filter.germ.linear_ordered_comm_ring {α : Type u} {β : Type v} {φ : ultrafilter α} [linear_ordered_comm_ring β] :

If φ is an ultrafilter then the ultraproduct is a linear ordered commutative ring.

Equations
@[protected, instance]
noncomputable def filter.germ.linear_ordered_add_comm_group {α : Type u} {β : Type v} {φ : ultrafilter α} [linear_ordered_add_comm_group β] :

If φ is an ultrafilter then the ultraproduct is a decidable linear ordered commutative group.

Equations
theorem filter.germ.max_def {α : Type u} {β : Type v} {φ : ultrafilter α} [linear_order β] (x y : φ.germ β) :
theorem filter.germ.min_def {α : Type u} {β : Type v} {φ : ultrafilter α} [K : linear_order β] (x y : φ.germ β) :
theorem filter.germ.abs_def {α : Type u} {β : Type v} {φ : ultrafilter α} [linear_ordered_add_comm_group β] (x : φ.germ β) :
@[simp]
theorem filter.germ.const_max {α : Type u} {β : Type v} {φ : ultrafilter α} [linear_order β] (x y : β) :
@[simp]
theorem filter.germ.const_min {α : Type u} {β : Type v} {φ : ultrafilter α} [linear_order β] (x y : β) :
@[simp]
theorem filter.germ.const_abs {α : Type u} {β : Type v} {φ : ultrafilter α} [linear_ordered_add_comm_group β] (x : β) :