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
If φ
is an ultrafilter then the ultraproduct is a division ring.
Equations
- filter.germ.division_ring = {add := ring.add filter.germ.ring, add_assoc := _, zero := ring.zero filter.germ.ring, zero_add := _, add_zero := _, nsmul := ring.nsmul filter.germ.ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg filter.germ.ring, sub := ring.sub filter.germ.ring, sub_eq_add_neg := _, zsmul := ring.zsmul filter.germ.ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast filter.germ.ring, nat_cast := ring.nat_cast filter.germ.ring, one := ring.one filter.germ.ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul filter.germ.ring, mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow filter.germ.ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, inv := div_inv_monoid.inv filter.germ.div_inv_monoid, div := div_inv_monoid.div filter.germ.div_inv_monoid, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow filter.germ.div_inv_monoid, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, rat_cast := rat.cast_rec (div_inv_monoid.to_has_inv (↑φ.germ β)), mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := qsmul_rec rat.cast_rec (distrib.to_has_mul (↑φ.germ β)), qsmul_eq_mul' := _}
If φ
is an ultrafilter then the ultraproduct is a field.
Equations
- filter.germ.field = {add := comm_ring.add filter.germ.comm_ring, add_assoc := _, zero := comm_ring.zero filter.germ.comm_ring, zero_add := _, add_zero := _, nsmul := comm_ring.nsmul filter.germ.comm_ring, nsmul_zero' := _, nsmul_succ' := _, neg := comm_ring.neg filter.germ.comm_ring, sub := comm_ring.sub filter.germ.comm_ring, sub_eq_add_neg := _, zsmul := comm_ring.zsmul filter.germ.comm_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := comm_ring.int_cast filter.germ.comm_ring, nat_cast := comm_ring.nat_cast filter.germ.comm_ring, one := comm_ring.one filter.germ.comm_ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := comm_ring.mul filter.germ.comm_ring, mul_assoc := _, one_mul := _, mul_one := _, npow := comm_ring.npow filter.germ.comm_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := division_ring.inv filter.germ.division_ring, div := division_ring.div filter.germ.division_ring, div_eq_mul_inv := _, zpow := division_ring.zpow filter.germ.division_ring, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, rat_cast := division_ring.rat_cast filter.germ.division_ring, mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := division_ring.qsmul filter.germ.division_ring, qsmul_eq_mul' := _}
If φ
is an ultrafilter then the ultraproduct is a linear order.
Equations
- filter.germ.linear_order = {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 := _, 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)), max := max_default (λ (a b : ↑φ.germ β), classical.prop_decidable (a ≤ b)), max_def := _, min := min_default (λ (a b : ↑φ.germ β), classical.prop_decidable (a ≤ b)), min_def := _}
If φ
is an ultrafilter then the ultraproduct is an ordered ring.
Equations
- filter.germ.ordered_ring = {add := ring.add filter.germ.ring, add_assoc := _, zero := ring.zero filter.germ.ring, zero_add := _, add_zero := _, nsmul := ring.nsmul filter.germ.ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg filter.germ.ring, sub := ring.sub filter.germ.ring, sub_eq_add_neg := _, zsmul := ring.zsmul filter.germ.ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast filter.germ.ring, nat_cast := ring.nat_cast filter.germ.ring, one := ring.one filter.germ.ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul filter.germ.ring, mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow filter.germ.ring, npow_zero' := _, npow_succ' := _, 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 := _}
If φ
is an ultrafilter then the ultraproduct is a linear ordered ring.
Equations
- filter.germ.linear_ordered_ring = {add := ordered_ring.add filter.germ.ordered_ring, add_assoc := _, zero := ordered_ring.zero filter.germ.ordered_ring, zero_add := _, add_zero := _, nsmul := ordered_ring.nsmul filter.germ.ordered_ring, nsmul_zero' := _, nsmul_succ' := _, neg := ordered_ring.neg filter.germ.ordered_ring, sub := ordered_ring.sub filter.germ.ordered_ring, sub_eq_add_neg := _, zsmul := ordered_ring.zsmul filter.germ.ordered_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ordered_ring.int_cast filter.germ.ordered_ring, nat_cast := ordered_ring.nat_cast filter.germ.ordered_ring, one := ordered_ring.one filter.germ.ordered_ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ordered_ring.mul filter.germ.ordered_ring, mul_assoc := _, one_mul := _, mul_one := _, npow := ordered_ring.npow filter.germ.ordered_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := ordered_ring.le filter.germ.ordered_ring, lt := ordered_ring.lt filter.germ.ordered_ring, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_pos := _, le_total := _, decidable_le := linear_order.decidable_le filter.germ.linear_order, decidable_eq := linear_order.decidable_eq filter.germ.linear_order, decidable_lt := linear_order.decidable_lt filter.germ.linear_order, max := linear_order.max filter.germ.linear_order, max_def := _, min := linear_order.min filter.germ.linear_order, min_def := _, exists_pair_ne := _}
If φ
is an ultrafilter then the ultraproduct is a linear ordered field.
Equations
- filter.germ.linear_ordered_field = {add := linear_ordered_ring.add filter.germ.linear_ordered_ring, add_assoc := _, zero := linear_ordered_ring.zero filter.germ.linear_ordered_ring, zero_add := _, add_zero := _, nsmul := linear_ordered_ring.nsmul filter.germ.linear_ordered_ring, nsmul_zero' := _, nsmul_succ' := _, neg := linear_ordered_ring.neg filter.germ.linear_ordered_ring, sub := linear_ordered_ring.sub filter.germ.linear_ordered_ring, sub_eq_add_neg := _, zsmul := linear_ordered_ring.zsmul filter.germ.linear_ordered_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := linear_ordered_ring.int_cast filter.germ.linear_ordered_ring, nat_cast := linear_ordered_ring.nat_cast filter.germ.linear_ordered_ring, one := linear_ordered_ring.one filter.germ.linear_ordered_ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := linear_ordered_ring.mul filter.germ.linear_ordered_ring, mul_assoc := _, one_mul := _, mul_one := _, npow := linear_ordered_ring.npow filter.germ.linear_ordered_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := linear_ordered_ring.le filter.germ.linear_ordered_ring, lt := linear_ordered_ring.lt filter.germ.linear_ordered_ring, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_pos := _, le_total := _, decidable_le := linear_ordered_ring.decidable_le filter.germ.linear_ordered_ring, decidable_eq := linear_ordered_ring.decidable_eq filter.germ.linear_ordered_ring, decidable_lt := linear_ordered_ring.decidable_lt filter.germ.linear_ordered_ring, max := linear_ordered_ring.max filter.germ.linear_ordered_ring, max_def := _, min := linear_ordered_ring.min filter.germ.linear_ordered_ring, min_def := _, exists_pair_ne := _, mul_comm := _, inv := field.inv filter.germ.field, div := field.div filter.germ.field, div_eq_mul_inv := _, zpow := field.zpow filter.germ.field, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, rat_cast := field.rat_cast filter.germ.field, mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := field.qsmul filter.germ.field, qsmul_eq_mul' := _}
If φ
is an ultrafilter then the ultraproduct is a linear ordered commutative ring.
Equations
- filter.germ.linear_ordered_comm_ring = {add := linear_ordered_ring.add filter.germ.linear_ordered_ring, add_assoc := _, zero := linear_ordered_ring.zero filter.germ.linear_ordered_ring, zero_add := _, add_zero := _, nsmul := linear_ordered_ring.nsmul filter.germ.linear_ordered_ring, nsmul_zero' := _, nsmul_succ' := _, neg := linear_ordered_ring.neg filter.germ.linear_ordered_ring, sub := linear_ordered_ring.sub filter.germ.linear_ordered_ring, sub_eq_add_neg := _, zsmul := linear_ordered_ring.zsmul filter.germ.linear_ordered_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := linear_ordered_ring.int_cast filter.germ.linear_ordered_ring, nat_cast := linear_ordered_ring.nat_cast filter.germ.linear_ordered_ring, one := linear_ordered_ring.one filter.germ.linear_ordered_ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := linear_ordered_ring.mul filter.germ.linear_ordered_ring, mul_assoc := _, one_mul := _, mul_one := _, npow := linear_ordered_ring.npow filter.germ.linear_ordered_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := linear_ordered_ring.le filter.germ.linear_ordered_ring, lt := linear_ordered_ring.lt filter.germ.linear_ordered_ring, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, zero_le_one := _, mul_pos := _, le_total := _, decidable_le := linear_ordered_ring.decidable_le filter.germ.linear_ordered_ring, decidable_eq := linear_ordered_ring.decidable_eq filter.germ.linear_ordered_ring, decidable_lt := linear_ordered_ring.decidable_lt filter.germ.linear_ordered_ring, max := linear_ordered_ring.max filter.germ.linear_ordered_ring, max_def := _, min := linear_ordered_ring.min filter.germ.linear_ordered_ring, min_def := _, exists_pair_ne := _, mul_comm := _}
If φ
is an ultrafilter then the ultraproduct is a decidable linear ordered commutative
group.
Equations
- filter.germ.linear_ordered_add_comm_group = {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 := _, nsmul := ordered_add_comm_group.nsmul filter.germ.ordered_add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := ordered_add_comm_group.neg filter.germ.ordered_add_comm_group, sub := ordered_add_comm_group.sub filter.germ.ordered_add_comm_group, sub_eq_add_neg := _, zsmul := ordered_add_comm_group.zsmul filter.germ.ordered_add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, 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 := _, add_le_add_left := _, le_total := _, decidable_le := linear_order.decidable_le filter.germ.linear_order, decidable_eq := linear_order.decidable_eq filter.germ.linear_order, decidable_lt := linear_order.decidable_lt filter.germ.linear_order, max := linear_order.max filter.germ.linear_order, max_def := _, min := linear_order.min filter.germ.linear_order, min_def := _}