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.groupWithZero {α : Type u} {β : Type v} {φ : Ultrafilter α} [GroupWithZero β] : GroupWithZero (Filter.Germ (↑φ) β)

Equations

• Filter.Germ.groupWithZero = let __src := Filter.Germ.divInvMonoid; let __src_1 := Filter.Germ.monoidWithZero; GroupWithZero.mk ⋯ DivInvMonoid.zpow ⋯ ⋯ ⋯ ⋯ ⋯

instance Filter.Germ.divisionSemiring {α : Type u} {β : Type v} {φ : Ultrafilter α} [DivisionSemiring β] : DivisionSemiring (Filter.Germ (↑φ) β)

Equations

• Filter.Germ.divisionSemiring = let __spread.0 := Filter.Germ.groupWithZero; DivisionSemiring.mk ⋯ GroupWithZero.zpow ⋯ ⋯ ⋯ ⋯ ⋯

instance Filter.Germ.divisionRing {α : Type u} {β : Type v} {φ : Ultrafilter α} [DivisionRing β] : DivisionRing (Filter.Germ (↑φ) β)

Equations

• Filter.Germ.divisionRing = let __src := Filter.Germ.ring; let __src_1 := Filter.Germ.divisionSemiring; DivisionRing.mk ⋯ DivisionSemiring.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (qsmulRec Rat.cast) ⋯

instance Filter.Germ.semifield {α : Type u} {β : Type v} {φ : Ultrafilter α} [Semifield β] : Semifield (Filter.Germ (↑φ) β)

Equations

• Filter.Germ.semifield = let __src := Filter.Germ.commSemiring; let __src_1 := Filter.Germ.divisionSemiring; Semifield.mk ⋯ DivisionSemiring.zpow ⋯ ⋯ ⋯ ⋯ ⋯

instance Filter.Germ.field {α : Type u} {β : Type v} {φ : Ultrafilter α} [Field β] : Field (Filter.Germ (↑φ) β)

Equations

• Filter.Germ.field = let __src := Filter.Germ.commRing; let __src_1 := Filter.Germ.divisionRing; Field.mk ⋯ DivisionRing.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ DivisionRing.qsmul ⋯

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 β] [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

@[simp]

theorem Filter.Germ.const_lt_iff {α : Type u} {β : Type v} {φ : Ultrafilter α} [Preorder β] {x : β} {y : β} : ↑x < ↑y ↔ x < y

theorem Filter.Germ.lt_def {α : Type u} {β : Type v} {φ : Ultrafilter α} [Preorder β] : (fun (x x_1 : Filter.Germ (↑φ) β) => x < x_1) = Filter.Germ.LiftRel fun (x x_1 : β) => x < x_1

instance Filter.Germ.isTotal {α : Type u} {β : Type v} {φ : Ultrafilter α} [LE β] [IsTotal β fun (x x_1 : β) => x ≤ x_1] : IsTotal (Filter.Germ (↑φ) β) fun (x x_1 : Filter.Germ (↑φ) β) => x ≤ x_1

Equations

• ⋯ = ⋯

noncomputable instance Filter.Germ.linearOrder {α : Type u} {β : Type v} {φ : Ultrafilter α} [LinearOrder β] : LinearOrder (Filter.Germ (↑φ) β)

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

Equations

• Filter.Germ.linearOrder = Lattice.toLinearOrder (Filter.Germ (↑φ) β)

theorem Filter.Germ.linearOrderedAddCommGroup.proof_2 {α : Type u_2} {β : Type u_1} {φ : Ultrafilter α} [LinearOrderedAddCommGroup β] (a : Filter.Germ (↑φ) β) (b : Filter.Germ (↑φ) β) : min a b = if a ≤ b then a else b

theorem Filter.Germ.linearOrderedAddCommGroup.proof_1 {α : Type u_2} {β : Type u_1} {φ : Ultrafilter α} [LinearOrderedAddCommGroup β] (a : Filter.Germ (↑φ) β) (b : Filter.Germ (↑φ) β) : a ≤ b ∨ b ≤ a

theorem Filter.Germ.linearOrderedAddCommGroup.proof_3 {α : Type u_2} {β : Type u_1} {φ : Ultrafilter α} [LinearOrderedAddCommGroup β] (a : Filter.Germ (↑φ) β) (b : Filter.Germ (↑φ) β) : max a b = if a ≤ b then b else a

theorem Filter.Germ.linearOrderedAddCommGroup.proof_4 {α : Type u_2} {β : Type u_1} {φ : Ultrafilter α} [LinearOrderedAddCommGroup β] (a : Filter.Germ (↑φ) β) (b : Filter.Germ (↑φ) β) : compare a b = compareOfLessAndEq a b

noncomputable instance Filter.Germ.linearOrderedAddCommGroup {α : Type u} {β : Type v} {φ : Ultrafilter α} [LinearOrderedAddCommGroup β] : LinearOrderedAddCommGroup (Filter.Germ (↑φ) β)

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance Filter.Germ.linearOrderedCommGroup {α : Type u} {β : Type v} {φ : Ultrafilter α} [LinearOrderedCommGroup β] : LinearOrderedCommGroup (Filter.Germ (↑φ) β)

Equations

• One or more equations did not get rendered due to their size.

instance Filter.Germ.strictOrderedSemiring {α : Type u} {β : Type v} {φ : Ultrafilter α} [StrictOrderedSemiring β] : StrictOrderedSemiring (Filter.Germ (↑φ) β)

Equations

• Filter.Germ.strictOrderedSemiring = let __src := Filter.Germ.orderedSemiring; let __src_1 := Filter.Germ.orderedAddCancelCommMonoid; let __src_2 := ⋯; StrictOrderedSemiring.mk ⋯ ⋯ ⋯ ⋯ ⋯

instance Filter.Germ.strictOrderedCommSemiring {α : Type u} {β : Type v} {φ : Ultrafilter α} [StrictOrderedCommSemiring β] : StrictOrderedCommSemiring (Filter.Germ (↑φ) β)

Equations

• Filter.Germ.strictOrderedCommSemiring = let __src := Filter.Germ.strictOrderedSemiring; let __src_1 := Filter.Germ.orderedCommSemiring; StrictOrderedCommSemiring.mk ⋯

instance Filter.Germ.strictOrderedRing {α : Type u} {β : Type v} {φ : Ultrafilter α} [StrictOrderedRing β] : StrictOrderedRing (Filter.Germ (↑φ) β)

Equations

• Filter.Germ.strictOrderedRing = let __src := Filter.Germ.ring; let __src_1 := Filter.Germ.strictOrderedSemiring; StrictOrderedRing.mk ⋯ ⋯ ⋯

instance Filter.Germ.strictOrderedCommRing {α : Type u} {β : Type v} {φ : Ultrafilter α} [StrictOrderedCommRing β] : StrictOrderedCommRing (Filter.Germ (↑φ) β)

Equations

• Filter.Germ.strictOrderedCommRing = let __src := Filter.Germ.strictOrderedRing; let __src_1 := Filter.Germ.orderedCommRing; StrictOrderedCommRing.mk ⋯

noncomputable instance Filter.Germ.linearOrderedRing {α : Type u} {β : Type v} {φ : Ultrafilter α} [LinearOrderedRing β] : LinearOrderedRing (Filter.Germ (↑φ) β)

Equations

• One or more equations did not get rendered due to their size.

noncomputable instance Filter.Germ.linearOrderedField {α : Type u} {β : Type v} {φ : Ultrafilter α} [LinearOrderedField β] : LinearOrderedField (Filter.Germ (↑φ) β)

Equations

• Filter.Germ.linearOrderedField = let __src := Filter.Germ.linearOrderedRing; let __src_1 := Filter.Germ.field; LinearOrderedField.mk ⋯ Field.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ Field.qsmul ⋯

noncomputable instance Filter.Germ.linearOrderedCommRing {α : Type u} {β : Type v} {φ : Ultrafilter α} [LinearOrderedCommRing β] : LinearOrderedCommRing (Filter.Germ (↑φ) β)

Equations

• Filter.Germ.linearOrderedCommRing = let __src := Filter.Germ.linearOrderedRing; let __src_1 := Filter.Germ.commMonoid; LinearOrderedCommRing.mk ⋯

theorem Filter.Germ.max_def {α : Type u} {β : Type v} {φ : Ultrafilter α} [LinearOrder β] (x : Filter.Germ (↑φ) β) (y : Filter.Germ (↑φ) β) : max x y = Filter.Germ.map₂ max x y

theorem Filter.Germ.min_def {α : Type u} {β : Type v} {φ : Ultrafilter α} [K : LinearOrder β] (x : Filter.Germ (↑φ) β) (y : Filter.Germ (↑φ) β) : min x y = Filter.Germ.map₂ min x y

theorem Filter.Germ.abs_def {α : Type u} {β : Type v} {φ : Ultrafilter α} [LinearOrderedAddCommGroup β] (x : Filter.Germ (↑φ) β) : |x| = Filter.Germ.map abs x

@[simp]

theorem Filter.Germ.const_max {α : Type u} {β : Type v} {φ : Ultrafilter α} [LinearOrder β] (x : β) (y : β) : ↑(max x y) = max ↑x ↑y

@[simp]

theorem Filter.Germ.const_min {α : Type u} {β : Type v} {φ : Ultrafilter α} [LinearOrder β] (x : β) (y : β) : ↑(min x y) = min ↑x ↑y

@[simp]

theorem Filter.Germ.const_abs {α : Type u} {β : Type v} {φ : Ultrafilter α} [LinearOrderedAddCommGroup β] (x : β) : ↑|x| = |↑x|