Skip to content

Commit 3444d0d

Browse files
arienmalecarienmalec
committed
feat: Port/Order.Filter.FilterProduct (#2366)
also names instances in `Order.Filter.Germ`
1 parent 963a074 commit 3444d0d

File tree

3 files changed

+277
-19
lines changed

3 files changed

+277
-19
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -890,6 +890,7 @@ import Mathlib.Order.Filter.Cofinite
890890
import Mathlib.Order.Filter.CountableInter
891891
import Mathlib.Order.Filter.Curry
892892
import Mathlib.Order.Filter.Extr
893+
import Mathlib.Order.Filter.FilterProduct
893894
import Mathlib.Order.Filter.Germ
894895
import Mathlib.Order.Filter.IndicatorFunction
895896
import Mathlib.Order.Filter.Interval

‎Mathlib/Order/Filter/FilterProduct.lean‎

Lines changed: 257 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,257 @@
1+
/-
2+
Copyright (c) 2019 Abhimanyu Pallavi Sudhir. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Abhimanyu Pallavi Sudhir, Yury Kudryashov
5+
6+
! This file was ported from Lean 3 source module order.filter.filter_product
7+
! leanprover-community/mathlib commit 2738d2ca56cbc63be80c3bd48e9ed90ad94e947d
8+
! Please do not edit these lines, except to modify the commit id
9+
! if you have ported upstream changes.
10+
-/
11+
import Mathlib.Order.Filter.Ultrafilter
12+
import Mathlib.Order.Filter.Germ
13+
14+
/-!
15+
# Ultraproducts
16+
17+
If `φ` is an ultrafilter, then the space of germs of functions `f : α → β` at `φ` is called
18+
the *ultraproduct*. In this file we prove properties of ultraproducts that rely on `φ` being an
19+
ultrafilter. Definitions and properties that work for any filter should go to `Order.Filter.Germ`.
20+
21+
## Tags
22+
23+
ultrafilter, ultraproduct
24+
-/
25+
26+
27+
universe u v
28+
29+
variable {α : Type u} {β : Type v} {φ : Ultrafilter α}
30+
31+
open Classical
32+
33+
namespace Filter
34+
35+
local notation3"∀* "(...)", "r:(scoped p => Filter.Eventually p φ) => r
36+
37+
namespace Germ
38+
39+
open Ultrafilter
40+
41+
local notation "β*" => Germ (φ : Filter α) β
42+
43+
instance divisionSemiring [DivisionSemiring β] : DivisionSemiring β* :=
44+
{ Germ.semiring, Germ.divInvMonoid,
45+
Germ.nontrivial with
46+
mul_inv_cancel := fun f =>
47+
inductionOn f fun f hf =>
48+
coe_eq.2 <|
49+
(φ.em fun y => f y = 0).elim (fun H => (hf <| coe_eq.2 H).elim) fun H =>
50+
H.mono fun x => mul_inv_cancel
51+
inv_zero := coe_eq.2 <| by
52+
simp only [Function.comp, inv_zero]
53+
exact EventuallyEq.refl _ fun _ => 0}
54+
55+
instance divisionRing [DivisionRing β] : DivisionRing β* :=
56+
{ Germ.ring, Germ.divisionSemiring with }
57+
58+
instance semifield [Semifield β] : Semifield β* :=
59+
{ Germ.commSemiring, Germ.divisionSemiring with }
60+
61+
instance field [Field β] : Field β* :=
62+
{ Germ.commRing, Germ.divisionRing with }
63+
64+
theorem coe_lt [Preorder β] {f g : α → β} : (f : β*) < g ↔ ∀* x, f x < g x := by
65+
simp only [lt_iff_le_not_le, eventually_and, coe_le, eventually_not, EventuallyLe]
66+
#align filter.germ.coe_lt Filter.Germ.coe_lt
67+
68+
theorem coe_pos [Preorder β] [Zero β] {f : α → β} : 0 < (f : β*) ↔ ∀* x, 0 < f x :=
69+
coe_lt
70+
#align filter.germ.coe_pos Filter.Germ.coe_pos
71+
72+
theorem const_lt [Preorder β] {x y : β} : x < y → (↑x : β*) < ↑y :=
73+
coe_lt.mpr ∘ liftRel_const
74+
#align filter.germ.const_lt Filter.Germ.const_lt
75+
76+
@[simp, norm_cast]
77+
theorem const_lt_iff [Preorder β] {x y : β} : (↑x : β*) < ↑y ↔ x < y :=
78+
coe_lt.trans liftRel_const_iff
79+
#align filter.germ.const_lt_iff Filter.Germ.const_lt_iff
80+
81+
theorem lt_def [Preorder β] : ((· < ·) : β* → β* → Prop) = LiftRel (· < ·) := by
82+
ext (⟨f⟩⟨g⟩)
83+
exact coe_lt
84+
#align filter.germ.lt_def Filter.Germ.lt_def
85+
86+
instance hasSup [HasSup β] : HasSup β* :=
87+
⟨map₂ (· ⊔ ·)⟩
88+
89+
instance hasInf [HasInf β] : HasInf β* :=
90+
⟨map₂ (· ⊓ ·)⟩
91+
92+
@[simp, norm_cast]
93+
theorem const_sup [HasSup β] (a b : β) : ↑(a ⊔ b) = (↑a ⊔ ↑b : β*) :=
94+
rfl
95+
#align filter.germ.const_sup Filter.Germ.const_sup
96+
97+
@[simp, norm_cast]
98+
theorem const_inf [HasInf β] (a b : β) : ↑(a ⊓ b) = (↑a ⊓ ↑b : β*) :=
99+
rfl
100+
#align filter.germ.const_inf Filter.Germ.const_inf
101+
102+
instance semilatticeSup [SemilatticeSup β] : SemilatticeSup β* :=
103+
{ Germ.partialOrder with
104+
sup := (· ⊔ ·)
105+
le_sup_left := fun f g =>
106+
inductionOn₂ f g fun _f _g => eventually_of_forall fun _x => le_sup_left
107+
le_sup_right := fun f g =>
108+
inductionOn₂ f g fun _f _g => eventually_of_forall fun _x => le_sup_right
109+
sup_le := fun f₁ f₂ g =>
110+
inductionOn₃ f₁ f₂ g fun _f₁ _f₂ _g h₁ h₂ => h₂.mp <| h₁.mono fun _x => sup_le }
111+
112+
instance semilatticeInf [SemilatticeInf β] : SemilatticeInf β* :=
113+
{ Germ.partialOrder with
114+
inf := (· ⊓ ·)
115+
inf_le_left := fun f g =>
116+
inductionOn₂ f g fun _f _g => eventually_of_forall fun _x => inf_le_left
117+
inf_le_right := fun f g =>
118+
inductionOn₂ f g fun _f _g => eventually_of_forall fun _x => inf_le_right
119+
le_inf := fun f₁ f₂ g =>
120+
inductionOn₃ f₁ f₂ g fun _f₁ _f₂ _g h₁ h₂ => h₂.mp <| h₁.mono fun _x => le_inf }
121+
122+
instance lattice [Lattice β] : Lattice β* :=
123+
{ Germ.semilatticeSup, Germ.semilatticeInf with }
124+
125+
instance distribLattice [DistribLattice β] : DistribLattice β* :=
126+
{ Germ.semilatticeSup, Germ.semilatticeInf with
127+
le_sup_inf := fun f g h =>
128+
inductionOn₃ f g h fun _f _g _h => eventually_of_forall fun _ => le_sup_inf }
129+
130+
instance isTotal [LE β] [IsTotal β (· ≤ ·)] : IsTotal β* (· ≤ ·) :=
131+
⟨fun f g =>
132+
inductionOn₂ f g fun _f _g => eventually_or.1 <| eventually_of_forall fun _x => total_of _ _ _⟩
133+
134+
/-- If `φ` is an ultrafilter then the ultraproduct is a linear order. -/
135+
noncomputable instance linearOrder [LinearOrder β] : LinearOrder β* :=
136+
Lattice.toLinearOrder _
137+
138+
@[to_additive]
139+
instance orderedCommMonoid [OrderedCommMonoid β] : OrderedCommMonoid β* :=
140+
{ Germ.partialOrder, Germ.commMonoid with
141+
mul_le_mul_left := fun f g =>
142+
inductionOn₂ f g fun _f _g H h =>
143+
inductionOn h fun _h => H.mono fun _x H => mul_le_mul_left' H _ }
144+
145+
@[to_additive]
146+
instance orderedCancelCommMonoid [OrderedCancelCommMonoid β] :
147+
OrderedCancelCommMonoid β* :=
148+
{ Germ.orderedCommMonoid with
149+
le_of_mul_le_mul_left := fun f g h =>
150+
inductionOn₃ f g h fun _f _g _h H => H.mono fun _x => le_of_mul_le_mul_left' }
151+
152+
@[to_additive]
153+
instance orderedCommGroup [OrderedCommGroup β] : OrderedCommGroup β* :=
154+
{ Germ.orderedCancelCommMonoid, Germ.commGroup with }
155+
156+
@[to_additive]
157+
noncomputable instance linearOrderedCommGroup [LinearOrderedCommGroup β] :
158+
LinearOrderedCommGroup β* :=
159+
{ Germ.orderedCommGroup, Germ.linearOrder with }
160+
161+
instance orderedSemiring [OrderedSemiring β] : OrderedSemiring β* :=
162+
{ Germ.semiring,
163+
Germ.orderedAddCommMonoid with
164+
zero_le_one := const_le zero_le_one
165+
mul_le_mul_of_nonneg_left := fun x y z =>
166+
inductionOn₃ x y z fun _f _g _h hfg hh =>
167+
hh.mp <| hfg.mono fun _a => mul_le_mul_of_nonneg_left
168+
mul_le_mul_of_nonneg_right := fun x y z =>
169+
inductionOn₃ x y z fun _f _g _h hfg hh =>
170+
hh.mp <| hfg.mono fun _a => mul_le_mul_of_nonneg_right }
171+
172+
instance orderedCommSemiring [OrderedCommSemiring β] : OrderedCommSemiring β* :=
173+
{ Germ.orderedSemiring, Germ.commSemiring with }
174+
175+
instance orderedRing [OrderedRing β] : OrderedRing β* :=
176+
{ Germ.ring,
177+
Germ.orderedAddCommGroup with
178+
zero_le_one := const_le zero_le_one
179+
mul_nonneg := fun x y =>
180+
inductionOn₂ x y fun _f _g hf hg => hg.mp <| hf.mono fun _a => mul_nonneg }
181+
182+
instance orderedCommRing [OrderedCommRing β] : OrderedCommRing β* :=
183+
{ Germ.orderedRing, Germ.orderedCommSemiring with }
184+
185+
instance strictOrderedSemiring [StrictOrderedSemiring β] : StrictOrderedSemiring β* :=
186+
{ Germ.orderedSemiring, Germ.orderedAddCancelCommMonoid,
187+
Germ.nontrivial with
188+
mul_lt_mul_of_pos_left := fun x y z =>
189+
inductionOn₃ x y z fun _f _g _h hfg hh =>
190+
coe_lt.2 <| (coe_lt.1 hh).mp <| (coe_lt.1 hfg).mono fun _a => mul_lt_mul_of_pos_left
191+
mul_lt_mul_of_pos_right := fun x y z =>
192+
inductionOn₃ x y z fun _f _g _h hfg hh =>
193+
coe_lt.2 <| (coe_lt.1 hh).mp <| (coe_lt.1 hfg).mono fun _a => mul_lt_mul_of_pos_right }
194+
195+
instance strictOrderedCommSemiring [StrictOrderedCommSemiring β] : StrictOrderedCommSemiring β* :=
196+
{ Germ.strictOrderedSemiring, Germ.orderedCommSemiring with }
197+
198+
instance strictOrderedRing [StrictOrderedRing β] : StrictOrderedRing β* :=
199+
{ Germ.ring,
200+
Germ.strictOrderedSemiring with
201+
zero_le_one := const_le zero_le_one
202+
mul_pos := fun x y =>
203+
inductionOn₂ x y fun _f _g hf hg =>
204+
coe_pos.2 <| (coe_pos.1 hg).mp <| (coe_pos.1 hf).mono fun _x => mul_pos }
205+
206+
instance strictOrderedCommRing [StrictOrderedCommRing β] : StrictOrderedCommRing β* :=
207+
{ Germ.strictOrderedRing, Germ.orderedCommRing with }
208+
209+
noncomputable instance linearOrderedRing [LinearOrderedRing β] : LinearOrderedRing β* :=
210+
{ Germ.strictOrderedRing, Germ.linearOrder with }
211+
212+
noncomputable instance linearOrderedField [LinearOrderedField β] : LinearOrderedField β* :=
213+
{ Germ.linearOrderedRing, Germ.field with }
214+
215+
noncomputable instance linearOrderedCommRing [LinearOrderedCommRing β] : LinearOrderedCommRing β* :=
216+
{ Germ.linearOrderedRing, Germ.commMonoid with }
217+
218+
theorem max_def [LinearOrder β] (x y : β*) : max x y = map₂ max x y :=
219+
inductionOn₂ x y fun a b => by
220+
cases' le_total (a : β*) b with h h
221+
· rw [max_eq_right h, map₂_coe, coe_eq]
222+
exact h.mono fun i hi => (max_eq_right hi).symm
223+
· rw [max_eq_left h, map₂_coe, coe_eq]
224+
exact h.mono fun i hi => (max_eq_left hi).symm
225+
#align filter.germ.max_def Filter.Germ.max_def
226+
227+
theorem min_def [K : LinearOrder β] (x y : β*) : min x y = map₂ min x y :=
228+
inductionOn₂ x y fun a b => by
229+
cases' le_total (a : β*) b with h h
230+
· rw [min_eq_left h, map₂_coe, coe_eq]
231+
exact h.mono fun i hi => (min_eq_left hi).symm
232+
· rw [min_eq_right h, map₂_coe, coe_eq]
233+
exact h.mono fun i hi => (min_eq_right hi).symm
234+
#align filter.germ.min_def Filter.Germ.min_def
235+
236+
theorem abs_def [LinearOrderedAddCommGroup β] (x : β*) : |x| = map abs x :=
237+
inductionOn x fun _a => rfl
238+
#align filter.germ.abs_def Filter.Germ.abs_def
239+
240+
@[simp]
241+
theorem const_max [LinearOrder β] (x y : β) : (↑(max x y : β) : β*) = max ↑x ↑y := by
242+
rw [max_def, map₂_const]
243+
#align filter.germ.const_max Filter.Germ.const_max
244+
245+
@[simp]
246+
theorem const_min [LinearOrder β] (x y : β) : (↑(min x y : β) : β*) = min ↑x ↑y := by
247+
rw [min_def, map₂_const]
248+
#align filter.germ.const_min Filter.Germ.const_min
249+
250+
@[simp]
251+
theorem const_abs [LinearOrderedAddCommGroup β] (x : β) : (↑(|x|) : β*) = |↑x| := by
252+
rw [abs_def, map_const]
253+
#align filter.germ.const_abs Filter.Germ.const_abs
254+
255+
end Germ
256+
257+
end Filter

‎Mathlib/Order/Filter/Germ.lean‎

Lines changed: 19 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -103,10 +103,10 @@ namespace Product
103103

104104
variable {ε : α → Type _}
105105

106-
instance : CoeTC ((a : _) → ε a) (l.Product ε) :=
106+
instance coeTC : CoeTC ((a : _) → ε a) (l.Product ε) :=
107107
⟨@Quotient.mk' _ (productSetoid _ ε)⟩
108108

109-
instance [(a : _) → Inhabited (ε a)] : Inhabited (l.Product ε) :=
109+
instance inhabited [(a : _) → Inhabited (ε a)] : Inhabited (l.Product ε) :=
110110
⟨(↑fun a => (default : ε a) : l.Product ε)⟩
111111

112112
end Product
@@ -123,7 +123,7 @@ instance : CoeTC (α → β) (Germ l β) :=
123123
@[coe] -- Porting note: removed `HasLiftT` instance
124124
def const {l : Filter α} (b : β) : (Germ l β) := ofFun fun _ => b
125125

126-
instance : CoeTC β (Germ l β) :=
126+
instance coeTC : CoeTC β (Germ l β) :=
127127
⟨const⟩
128128

129129
@[simp]
@@ -331,7 +331,7 @@ theorem liftRel_const_iff [NeBot l] {r : β → γ → Prop} {x : β} {y : γ} :
331331
@eventually_const _ _ _ (r x y)
332332
#align filter.germ.lift_rel_const_iff Filter.Germ.liftRel_const_iff
333333

334-
instance [Inhabited β] : Inhabited (Germ l β) :=
334+
instance inhabited [Inhabited β] : Inhabited (Germ l β) :=
335335
⟨↑(default : β)⟩
336336

337337
section Monoid
@@ -382,15 +382,15 @@ instance rightCancelSemigroup [RightCancelSemigroup M] : RightCancelSemigroup (G
382382
inductionOn₃ f₁ f₂ f₃ fun _f₁ _f₂ _f₃ H =>
383383
coe_eq.2 <| (coe_eq.1 H).mono fun _x => mul_right_cancel }
384384

385-
instance [VAdd M G] : VAdd M (Germ l G) :=
385+
instance vAdd [VAdd M G] : VAdd M (Germ l G) :=
386386
⟨fun n => map ((· +ᵥ ·) n)⟩
387387

388388
@[to_additive]
389-
instance [SMul M G] : SMul M (Germ l G) :=
389+
instance sMul [SMul M G] : SMul M (Germ l G) :=
390390
⟨fun n => map (n • ·)⟩
391391

392-
@[to_additive instSMulGerm]
393-
instance [Pow G M] : Pow (Germ l G) M :=
392+
@[to_additive sMul]
393+
instance pow [Pow G M] : Pow (Germ l G) M :=
394394
⟨fun f n => map (· ^ n) f⟩
395395

396396
@[to_additive (attr := simp, norm_cast)]
@@ -449,7 +449,7 @@ instance addMonoidWithOne [AddMonoidWithOne M] : AddMonoidWithOne (Germ l M) :=
449449
natCast_succ := fun _ => congr_arg ((↑) : M → Germ l M) (Nat.cast_succ _) }
450450

451451
@[to_additive]
452-
instance [Inv G] : Inv (Germ l G) :=
452+
instance inv [Inv G] : Inv (Germ l G) :=
453453
⟨map Inv.inv⟩
454454

455455
@[to_additive (attr := simp, norm_cast)]
@@ -582,7 +582,7 @@ theorem coe_smul' [SMul M β] (c : α → M) (f : α → β) : ↑(c • f) = (c
582582
#align filter.germ.coe_vadd' Filter.Germ.coe_vadd'
583583

584584
@[to_additive]
585-
instance [Monoid M] [MulAction M β] : MulAction M (Germ l β) where
585+
instance mulAction [Monoid M] [MulAction M β] : MulAction M (Germ l β) where
586586
-- Porting note: `rfl` required.
587587
one_smul f :=
588588
inductionOn f fun f => by
@@ -653,7 +653,7 @@ instance module' [Semiring R] [AddCommMonoid M] [Module R M] : Module (Germ l R)
653653

654654
end Module
655655

656-
instance [LE β] : LE (Germ l β) :=
656+
instance le [LE β] : LE (Germ l β) :=
657657
⟨LiftRel (· ≤ ·)⟩
658658

659659
theorem le_def [LE β] : ((· ≤ ·) : Germ l β → Germ l β → Prop) = LiftRel (· ≤ ·) :=
@@ -678,22 +678,22 @@ theorem const_le_iff [LE β] [NeBot l] {x y : β} : (↑x : Germ l β) ≤ ↑y
678678
liftRel_const_iff
679679
#align filter.germ.const_le_iff Filter.Germ.const_le_iff
680680

681-
instance [Preorder β] : Preorder (Germ l β)
681+
instance preorder [Preorder β] : Preorder (Germ l β)
682682
where
683683
le := (· ≤ ·)
684684
le_refl f := inductionOn f <| EventuallyLe.refl l
685685
le_trans f₁ f₂ f₃ := inductionOn₃ f₁ f₂ f₃ fun f₁ f₂ f₃ => EventuallyLe.trans
686686

687-
instance [PartialOrder β] : PartialOrder (Germ l β) :=
688-
{ Filter.Germ.instPreorderGerm with
687+
instance partialOrder [PartialOrder β] : PartialOrder (Germ l β) :=
688+
{ Filter.Germ.preorder with
689689
le := (· ≤ ·)
690690
le_antisymm := fun f g =>
691691
inductionOn₂ f g fun _ _ h₁ h₂ => (EventuallyLe.antisymm h₁ h₂).germ_eq }
692692

693-
instance [Bot β] : Bot (Germ l β) :=
693+
instance bot [Bot β] : Bot (Germ l β) :=
694694
⟨↑(⊥ : β)⟩
695695

696-
instance [Top β] : Top (Germ l β) :=
696+
instance top [Top β] : Top (Germ l β) :=
697697
⟨↑(⊤ : β)⟩
698698

699699
@[simp, norm_cast]
@@ -706,18 +706,18 @@ theorem const_top [Top β] : (↑(⊤ : β) : Germ l β) = ⊤ :=
706706
rfl
707707
#align filter.germ.const_top Filter.Germ.const_top
708708

709-
instance [LE β] [OrderBot β] : OrderBot (Germ l β)
709+
instance orderBot [LE β] [OrderBot β] : OrderBot (Germ l β)
710710
where
711711
bot := ⊥
712712
bot_le f := inductionOn f fun _ => eventually_of_forall fun _ => bot_le
713713

714-
instance [LE β] [OrderTop β] : OrderTop (Germ l β)
714+
instance orderTop [LE β] [OrderTop β] : OrderTop (Germ l β)
715715
where
716716
top := ⊤
717717
le_top f := inductionOn f fun _ => eventually_of_forall fun _ => le_top
718718

719719
instance [LE β] [BoundedOrder β] : BoundedOrder (Germ l β) :=
720-
{ Filter.Germ.instOrderBotGermInstLEGerm, Filter.Germ.instOrderTopGermInstLEGerm with }
720+
{ Filter.Germ.orderBot, Filter.Germ.orderTop with }
721721

722722
end Germ
723723

0 commit comments

Comments
 (0)