Documentation

Mathlib.Order.Filter.FilterProduct

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.instGroupWithZero {α : Type u} {β : Type v} {φ : Ultrafilter α} [GroupWithZero β] :

GroupWithZero ((↑φ).Germ β)

Equations

Filter.Germ.instGroupWithZero = GroupWithZero.mk ⋯ DivInvMonoid.zpow ⋯ ⋯ ⋯ ⋯ ⋯

instance Filter.Germ.instDivisionSemiring {α : Type u} {β : Type v} {φ : Ultrafilter α} [DivisionSemiring β] :

DivisionSemiring ((↑φ).Germ β)

Equations

Filter.Germ.instDivisionSemiring = DivisionSemiring.mk ⋯ GroupWithZero.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ (fun (x : ℚ≥0) => HMul.hMul ↑x) ⋯

instance Filter.Germ.instDivisionRing {α : Type u} {β : Type v} {φ : Ultrafilter α} [DivisionRing β] :

DivisionRing ((↑φ).Germ β)

Equations

Filter.Germ.instDivisionRing = DivisionRing.mk ⋯ DivisionSemiring.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ DivisionSemiring.nnqsmul ⋯ ⋯ (fun (x : ℚ) => HMul.hMul ↑x) ⋯

instance Filter.Germ.instSemifield {α : Type u} {β : Type v} {φ : Ultrafilter α} [Semifield β] :

Semifield ((↑φ).Germ β)

Equations

Filter.Germ.instSemifield = Semifield.mk ⋯ DivisionSemiring.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ DivisionSemiring.nnqsmul ⋯

instance Filter.Germ.instField {α : Type u} {β : Type v} {φ : Ultrafilter α} [Field β] :

Field ((↑φ).Germ β)

Equations

Filter.Germ.instField = Field.mk ⋯ DivisionRing.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ DivisionRing.nnqsmul ⋯ ⋯ 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 (x1 x2 : (↑φ).Germ β) => x1 < x2) = LiftRel fun (x1 x2 : β) => x1 < x2

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

IsTotal ((↑φ).Germ β) fun (x1 x2 : (↑φ).Germ β) => x1 ≤ x2

noncomputable instance Filter.Germ.instLinearOrder {α : Type u} {β : Type v} {φ : Ultrafilter α} [LinearOrder β] :

LinearOrder ((↑φ).Germ β)

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

Equations

Filter.Germ.instLinearOrder = Lattice.toLinearOrder ((↑φ).Germ β)

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

LinearOrderedCommGroup ((↑φ).Germ β)

Equations

Filter.Germ.linearOrderedCommGroup = LinearOrderedCommGroup.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

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

LinearOrderedAddCommGroup ((↑φ).Germ β)

Equations

Filter.Germ.linearOrderedAddCommGroup = LinearOrderedAddCommGroup.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

instance Filter.Germ.instStrictOrderedSemiring {α : Type u} {β : Type v} {φ : Ultrafilter α} [StrictOrderedSemiring β] :

StrictOrderedSemiring ((↑φ).Germ β)

Equations

Filter.Germ.instStrictOrderedSemiring = StrictOrderedSemiring.mk ⋯ ⋯ ⋯ ⋯ ⋯

instance Filter.Germ.instStrictOrderedCommSemiring {α : Type u} {β : Type v} {φ : Ultrafilter α} [StrictOrderedCommSemiring β] :

StrictOrderedCommSemiring ((↑φ).Germ β)

Equations

Filter.Germ.instStrictOrderedCommSemiring = StrictOrderedCommSemiring.mk ⋯

instance Filter.Germ.instStrictOrderedRing {α : Type u} {β : Type v} {φ : Ultrafilter α} [StrictOrderedRing β] :

StrictOrderedRing ((↑φ).Germ β)

Equations

Filter.Germ.instStrictOrderedRing = StrictOrderedRing.mk ⋯ ⋯ ⋯

instance Filter.Germ.instStrictOrderedCommRing {α : Type u} {β : Type v} {φ : Ultrafilter α} [StrictOrderedCommRing β] :

StrictOrderedCommRing ((↑φ).Germ β)

Equations

Filter.Germ.instStrictOrderedCommRing = StrictOrderedCommRing.mk ⋯

noncomputable instance Filter.Germ.instLinearOrderedRing {α : Type u} {β : Type v} {φ : Ultrafilter α} [LinearOrderedRing β] :

LinearOrderedRing ((↑φ).Germ β)

Equations

Filter.Germ.instLinearOrderedRing = LinearOrderedRing.mk ⋯ LinearOrder.decidableLE LinearOrder.decidableEq LinearOrder.decidableLT ⋯ ⋯ ⋯

noncomputable instance Filter.Germ.instLinearOrderedField {α : Type u} {β : Type v} {φ : Ultrafilter α} [LinearOrderedField β] :

LinearOrderedField ((↑φ).Germ β)

Equations

Filter.Germ.instLinearOrderedField = LinearOrderedField.mk ⋯ Field.zpow ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ Field.nnqsmul ⋯ ⋯ Field.qsmul ⋯

noncomputable instance Filter.Germ.instLinearOrderedCommRing {α : Type u} {β : Type v} {φ : Ultrafilter α} [LinearOrderedCommRing β] :

LinearOrderedCommRing ((↑φ).Germ β)

Equations

Filter.Germ.instLinearOrderedCommRing = LinearOrderedCommRing.mk ⋯

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

x ⊔ y = map₂ max x y

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

x ⊓ y = map₂ min x y

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

|x| = map abs x

@[simp]

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

↑(x ⊔ y) = ↑x ⊔ ↑y

@[simp]

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

↑(x ⊓ y) = ↑x ⊓ ↑y

@[simp]

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

↑|x| = |↑x|