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 α}
[division_ring β] :
φ.is_ultrafilter → division_ring (φ.germ β)
If φ is an ultrafilter then the ultraproduct is a division ring.
This cannot be an instance, since it depends on φ being an ultrafilter.
Equations
- filter.germ.division_ring U = {add := ring.add filter.germ.ring, add_assoc := _, zero := ring.zero filter.germ.ring, zero_add := _, add_zero := _, neg := ring.neg filter.germ.ring, add_left_neg := _, add_comm := _, mul := ring.mul filter.germ.ring, mul_assoc := _, one := ring.one filter.germ.ring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, inv := has_inv.inv filter.germ.has_inv, exists_pair_ne := _, mul_inv_cancel := _, inv_mul_cancel := _, inv_zero := _}
def
filter.germ.field
{α : Type u}
{β : Type v}
{φ : filter α}
[field β] :
φ.is_ultrafilter → field (φ.germ β)
If φ is an ultrafilter then the ultraproduct is a field.
This cannot be an instance, since it depends on φ being an ultrafilter.
Equations
- filter.germ.field U = {add := comm_ring.add filter.germ.comm_ring, add_assoc := _, zero := comm_ring.zero filter.germ.comm_ring, zero_add := _, add_zero := _, neg := comm_ring.neg filter.germ.comm_ring, add_left_neg := _, add_comm := _, mul := comm_ring.mul filter.germ.comm_ring, mul_assoc := _, one := comm_ring.one filter.germ.comm_ring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := division_ring.inv (filter.germ.division_ring U), exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}
def
filter.germ.linear_order
{α : Type u}
{β : Type v}
{φ : filter α}
[linear_order β] :
φ.is_ultrafilter → linear_order (φ.germ β)
If φ is an ultrafilter then the ultraproduct is a linear order.
This cannot be an instance, since it depends on φ being an ultrafilter.
Equations
- filter.germ.linear_order U = {le := partial_order.le filter.germ.partial_order, lt := partial_order.lt filter.germ.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _}
@[simp]
theorem
filter.germ.const_div
{α : Type u}
{β : Type v}
{φ : filter α}
[division_ring β]
(U : φ.is_ultrafilter)
(x y : β) :
theorem
filter.germ.coe_lt
{α : Type u}
{β : Type v}
{φ : filter α}
[preorder β]
(U : φ.is_ultrafilter)
{f g : α → β} :
theorem
filter.germ.coe_pos
{α : Type u}
{β : Type v}
{φ : filter α}
[preorder β]
[has_zero β]
(U : φ.is_ultrafilter)
{f : α → β} :
theorem
filter.germ.const_lt
{α : Type u}
{β : Type v}
{φ : filter α}
[preorder β]
(U : φ.is_ultrafilter)
{x y : β} :
def
filter.germ.ordered_ring
{α : Type u}
{β : Type v}
{φ : filter α}
[ordered_ring β] :
φ.is_ultrafilter → ordered_ring (φ.germ β)
If φ is an ultrafilter then the ultraproduct is an ordered ring.
This cannot be an instance, since it depends on φ being an ultrafilter.
Equations
- filter.germ.ordered_ring U = {add := ring.add filter.germ.ring, add_assoc := _, zero := ring.zero filter.germ.ring, zero_add := _, add_zero := _, neg := ring.neg filter.germ.ring, add_left_neg := _, add_comm := _, mul := ring.mul filter.germ.ring, mul_assoc := _, one := ring.one filter.germ.ring, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, le := ordered_add_comm_group.le filter.germ.ordered_add_comm_group, lt := ordered_add_comm_group.lt filter.germ.ordered_add_comm_group, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_pos := _}
def
filter.germ.linear_ordered_ring
{α : Type u}
{β : Type v}
{φ : filter α}
[linear_ordered_ring β] :
φ.is_ultrafilter → linear_ordered_ring (φ.germ β)
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
- filter.germ.linear_ordered_ring U = {add := ordered_ring.add (filter.germ.ordered_ring U), add_assoc := _, zero := ordered_ring.zero (filter.germ.ordered_ring U), zero_add := _, add_zero := _, neg := ordered_ring.neg (filter.germ.ordered_ring U), add_left_neg := _, add_comm := _, mul := ordered_ring.mul (filter.germ.ordered_ring U), mul_assoc := _, one := ordered_ring.one (filter.germ.ordered_ring U), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, le := ordered_ring.le (filter.germ.ordered_ring U), lt := ordered_ring.lt (filter.germ.ordered_ring U), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_pos := _, le_total := _, exists_pair_ne := _}
def
filter.germ.linear_ordered_field
{α : Type u}
{β : Type v}
{φ : filter α}
[linear_ordered_field β] :
φ.is_ultrafilter → linear_ordered_field (φ.germ β)
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
- filter.germ.linear_ordered_field U = {add := linear_ordered_ring.add (filter.germ.linear_ordered_ring U), add_assoc := _, zero := linear_ordered_ring.zero (filter.germ.linear_ordered_ring U), zero_add := _, add_zero := _, neg := linear_ordered_ring.neg (filter.germ.linear_ordered_ring U), add_left_neg := _, add_comm := _, mul := linear_ordered_ring.mul (filter.germ.linear_ordered_ring U), mul_assoc := _, one := linear_ordered_ring.one (filter.germ.linear_ordered_ring U), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, le := linear_ordered_ring.le (filter.germ.linear_ordered_ring U), lt := linear_ordered_ring.lt (filter.germ.linear_ordered_ring U), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_pos := _, le_total := _, exists_pair_ne := _, mul_comm := _, inv := field.inv (filter.germ.field U), mul_inv_cancel := _, inv_zero := _}
def
filter.germ.linear_ordered_comm_ring
{α : Type u}
{β : Type v}
{φ : filter α}
[linear_ordered_comm_ring β] :
φ.is_ultrafilter → linear_ordered_comm_ring (φ.germ β)
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
- filter.germ.linear_ordered_comm_ring U = {add := linear_ordered_ring.add (filter.germ.linear_ordered_ring U), add_assoc := _, zero := linear_ordered_ring.zero (filter.germ.linear_ordered_ring U), zero_add := _, add_zero := _, neg := linear_ordered_ring.neg (filter.germ.linear_ordered_ring U), add_left_neg := _, add_comm := _, mul := linear_ordered_ring.mul (filter.germ.linear_ordered_ring U), mul_assoc := _, one := linear_ordered_ring.one (filter.germ.linear_ordered_ring U), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, le := linear_ordered_ring.le (filter.germ.linear_ordered_ring U), lt := linear_ordered_ring.lt (filter.germ.linear_ordered_ring U), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_pos := _, le_total := _, exists_pair_ne := _, mul_comm := _}
def
filter.germ.decidable_linear_order
{α : Type u}
{β : Type v}
{φ : filter α}
[decidable_linear_order β] :
φ.is_ultrafilter → decidable_linear_order (φ.germ β)
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
- filter.germ.decidable_linear_order U = {le := linear_order.le (filter.germ.linear_order U), lt := linear_order.lt (filter.germ.linear_order U), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := λ (a b : φ.germ β), classical.prop_decidable (a ≤ b), decidable_eq := decidable_eq_of_decidable_le (λ (a b : φ.germ β), classical.prop_decidable (a ≤ b)), decidable_lt := decidable_lt_of_decidable_le (λ (a b : φ.germ β), classical.prop_decidable (a ≤ b))}
def
filter.germ.decidable_linear_ordered_add_comm_group
{α : Type u}
{β : Type v}
{φ : filter α}
[decidable_linear_ordered_add_comm_group β] :
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
- filter.germ.decidable_linear_ordered_add_comm_group U = {add := ordered_add_comm_group.add filter.germ.ordered_add_comm_group, add_assoc := _, zero := ordered_add_comm_group.zero filter.germ.ordered_add_comm_group, zero_add := _, add_zero := _, neg := ordered_add_comm_group.neg filter.germ.ordered_add_comm_group, add_left_neg := _, add_comm := _, le := ordered_add_comm_group.le filter.germ.ordered_add_comm_group, lt := ordered_add_comm_group.lt filter.germ.ordered_add_comm_group, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := decidable_linear_order.decidable_le (filter.germ.decidable_linear_order U), decidable_eq := decidable_linear_order.decidable_eq (filter.germ.decidable_linear_order U), decidable_lt := decidable_linear_order.decidable_lt (filter.germ.decidable_linear_order U), add_le_add_left := _}
def
filter.germ.decidable_linear_ordered_comm_ring
{α : Type u}
{β : Type v}
{φ : filter α}
[decidable_linear_ordered_comm_ring β] :
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
- filter.germ.decidable_linear_ordered_comm_ring U = {add := linear_ordered_comm_ring.add (filter.germ.linear_ordered_comm_ring U), add_assoc := _, zero := linear_ordered_comm_ring.zero (filter.germ.linear_ordered_comm_ring U), zero_add := _, add_zero := _, neg := linear_ordered_comm_ring.neg (filter.germ.linear_ordered_comm_ring U), add_left_neg := _, add_comm := _, mul := linear_ordered_comm_ring.mul (filter.germ.linear_ordered_comm_ring U), mul_assoc := _, one := linear_ordered_comm_ring.one (filter.germ.linear_ordered_comm_ring U), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, le := linear_ordered_comm_ring.le (filter.germ.linear_ordered_comm_ring U), lt := linear_ordered_comm_ring.lt (filter.germ.linear_ordered_comm_ring U), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_pos := _, le_total := _, exists_pair_ne := _, mul_comm := _, decidable_le := decidable_linear_ordered_add_comm_group.decidable_le (filter.germ.decidable_linear_ordered_add_comm_group U), decidable_eq := decidable_linear_ordered_add_comm_group.decidable_eq (filter.germ.decidable_linear_ordered_add_comm_group U), decidable_lt := decidable_linear_ordered_add_comm_group.decidable_lt (filter.germ.decidable_linear_ordered_add_comm_group U)}
def
filter.germ.discrete_linear_ordered_field
{α : Type u}
{β : Type v}
{φ : filter α}
[discrete_linear_ordered_field β] :
φ.is_ultrafilter → discrete_linear_ordered_field (φ.germ β)
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
- filter.germ.discrete_linear_ordered_field U = {add := linear_ordered_field.add (filter.germ.linear_ordered_field U), add_assoc := _, zero := linear_ordered_field.zero (filter.germ.linear_ordered_field U), zero_add := _, add_zero := _, neg := linear_ordered_field.neg (filter.germ.linear_ordered_field U), add_left_neg := _, add_comm := _, mul := linear_ordered_field.mul (filter.germ.linear_ordered_field U), mul_assoc := _, one := linear_ordered_field.one (filter.germ.linear_ordered_field U), one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, le := linear_ordered_field.le (filter.germ.linear_ordered_field U), lt := linear_ordered_field.lt (filter.germ.linear_ordered_field U), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_pos := _, le_total := _, exists_pair_ne := _, mul_comm := _, inv := linear_ordered_field.inv (filter.germ.linear_ordered_field U), mul_inv_cancel := _, inv_zero := _, decidable_le := decidable_linear_ordered_comm_ring.decidable_le (filter.germ.decidable_linear_ordered_comm_ring U), decidable_eq := decidable_linear_ordered_comm_ring.decidable_eq (filter.germ.decidable_linear_ordered_comm_ring U), decidable_lt := decidable_linear_ordered_comm_ring.decidable_lt (filter.germ.decidable_linear_ordered_comm_ring U)}
theorem
filter.germ.max_def
{α : Type u}
{β : Type v}
{φ : filter α}
[K : decidable_linear_order β]
(U : φ.is_ultrafilter)
(x y : φ.germ β) :
max x y = filter.germ.map₂ 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 = filter.germ.map₂ min x y
theorem
filter.germ.abs_def
{α : Type u}
{β : Type v}
{φ : filter α}
[decidable_linear_ordered_add_comm_group β]
(U : φ.is_ultrafilter)
(x : φ.germ β) :
abs x = filter.germ.map abs x
@[simp]
theorem
filter.germ.const_max
{α : Type u}
{β : Type v}
{φ : filter α}
[decidable_linear_order β]
(U : φ.is_ultrafilter)
(x y : β) :
@[simp]
theorem
filter.germ.const_min
{α : Type u}
{β : Type v}
{φ : filter α}
[decidable_linear_order β]
(U : φ.is_ultrafilter)
(x y : β) :
@[simp]
theorem
filter.germ.const_abs
{α : Type u}
{β : Type v}
{φ : filter α}
[decidable_linear_ordered_add_comm_group β]
(U : φ.is_ultrafilter)
(x : β) :