Skip to content

Commit 46d3115

Browse files
wwylelewwylele
committed
feat: ArchimedeanSubgroup
1 parent c670d28 commit 46d3115

File tree

5 files changed

+1304
-0
lines changed

5 files changed

+1304
-0
lines changed

‎Mathlib.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -870,9 +870,11 @@ import Mathlib.Algebra.Order.Interval.Set.SuccPred
870870
import Mathlib.Algebra.Order.Invertible
871871
import Mathlib.Algebra.Order.Kleene
872872
import Mathlib.Algebra.Order.Module.Algebra
873+
import Mathlib.Algebra.Order.Module.Archimedean
873874
import Mathlib.Algebra.Order.Module.Basic
874875
import Mathlib.Algebra.Order.Module.Defs
875876
import Mathlib.Algebra.Order.Module.Field
877+
import Mathlib.Algebra.Order.Module.HahnEmbedding
876878
import Mathlib.Algebra.Order.Module.OrderedSMul
877879
import Mathlib.Algebra.Order.Module.Pointwise
878880
import Mathlib.Algebra.Order.Module.PositiveLinearMap

‎Mathlib/Algebra/Order/Archimedean/Class.lean‎

Lines changed: 109 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,10 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Weiyi Wang
55
-/
66
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
7+
import Mathlib.Algebra.Group.Subgroup.Lattice
78
import Mathlib.Algebra.Order.Archimedean.Basic
89
import Mathlib.Algebra.Order.Hom.Monoid
910
import Mathlib.Data.Finset.Max
1011
import Mathlib.Order.Antisymmetrization
12+
import Mathlib.Order.UpperLower.CompleteLattice
13+
import Mathlib.Order.UpperLower.Principal
1114

1215
/-!
1316
# Archimedean classes of a linearly ordered group
@@ -576,3 +579,109 @@ theorem withTopOrderIso_symm_apply {a : M} (h : a ≠ 1) :
576579
rfl
577580

578581
end MulArchimedeanClass₁
582+
583+
/-- Given a non-empty `UpperSet` of archimedean classes,
584+
all group elements belonging to these classes form a subgroup. -/
585+
@[to_additive ArchimedeanSubgroup.of_ne_top "Given a non-empty `UpperSet` of archimedean classes,
586+
all group elements belonging to these classes form a subgroup."]
587+
noncomputable
588+
def MulArchimedeanSubgroup.of_ne_top {s : UpperSet (MulArchimedeanClass M)} (hs : s ≠ ⊤) :
589+
Subgroup M where
590+
carrier := MulArchimedeanClass.mk ⁻¹' s
591+
mul_mem' {a b} ha hb := by
592+
rw [Set.mem_preimage] at ha hb ⊢
593+
obtain h | h := min_le_iff.mp (MulArchimedeanClass.min_le_mk_mul a b)
594+
· exact s.upper h ha
595+
· exact s.upper h hb
596+
one_mem' := by
597+
rw [Set.mem_preimage]
598+
obtain ⟨u, hu⟩ := UpperSet.coe_nonempty.mpr hs
599+
simpa using s.upper (by simp) hu
600+
inv_mem' {a} h := by simpa using h
601+
602+
open Classical in
603+
/-- Generalize `MulArchimedeanSubgroup.of_ne_top` to any `UpperSet`
604+
with a junk value `⊥` given for the empty set. -/
605+
@[to_additive ArchimedeanSubgroup "Generalize `ArchimedeanSubgroup.of_ne_top` to any `UpperSet`
606+
with a junk value `⊥` given for the empty set."]
607+
noncomputable
608+
def MulArchimedeanSubgroup (s : UpperSet (MulArchimedeanClass M)) : Subgroup M :=
609+
if hs : s = ⊤ then
610+
⊥
611+
else
612+
MulArchimedeanSubgroup.of_ne_top hs
613+
614+
namespace MulArchimedeanSubgroup
615+
variable {s t : UpperSet (MulArchimedeanClass M)}
616+
617+
@[to_additive]
618+
theorem eq_of_ne_top (hs : s ≠ ⊤) :
619+
MulArchimedeanSubgroup s = MulArchimedeanSubgroup.of_ne_top hs := by
620+
unfold MulArchimedeanSubgroup
621+
simp [hs]
622+
623+
variable (M) in
624+
@[to_additive (attr := simp)]
625+
theorem eq_bot : MulArchimedeanSubgroup (M := M) ⊤ = ⊥ := by
626+
unfold MulArchimedeanSubgroup
627+
simp
628+
629+
@[to_additive]
630+
theorem mem_iff_of_ne_top (hs : s ≠ ⊤) :
631+
a ∈ MulArchimedeanSubgroup s ↔ MulArchimedeanClass.mk a ∈ s := by
632+
rw [eq_of_ne_top hs]
633+
exact Set.mem_preimage
634+
635+
omit s in
636+
@[to_additive]
637+
theorem mem_Ioi_iff_of_ne_top {A : MulArchimedeanClass M} (hA : A ≠ ⊤) :
638+
a ∈ MulArchimedeanSubgroup (UpperSet.Ioi A) ↔ A < MulArchimedeanClass.mk a := by
639+
have : UpperSet.Ioi A ≠ ⊤ := by
640+
by_contra!
641+
rw [UpperSet.ext_iff] at this
642+
have : A = ⊤ := by simpa using this
643+
exact hA this
644+
simp [mem_iff_of_ne_top this]
645+
646+
omit s in
647+
@[to_additive (attr := simp)]
648+
theorem mem_Ici_iff {A : MulArchimedeanClass M} :
649+
a ∈ MulArchimedeanSubgroup (UpperSet.Ici A) ↔ A ≤ MulArchimedeanClass.mk a := by
650+
have : UpperSet.Ici A ≠ ⊤ := by simp
651+
simp [mem_iff_of_ne_top this]
652+
653+
variable (M) in
654+
@[to_additive (attr := simp)]
655+
theorem eq_bot_of_Ici_top : MulArchimedeanSubgroup (M := M) (UpperSet.Ici ⊤) = ⊥ := by
656+
rw [Subgroup.eq_bot_iff_forall]
657+
intro x hx
658+
rw [mem_iff_of_ne_top (by simp)] at hx
659+
simpa using hx
660+
661+
variable (M) in
662+
@[to_additive]
663+
theorem strictAntiOn : StrictAntiOn (MulArchimedeanSubgroup (M := M)) (Set.Iio ⊤) := by
664+
intro s hs t ht hst
665+
rw [eq_of_ne_top (Set.mem_Iio.mp hs).ne_top, eq_of_ne_top (Set.mem_Iio.mp ht).ne_top]
666+
apply lt_of_le_of_ne
667+
· rw [Subgroup.mk_le_mk]
668+
refine (Set.preimage_subset_preimage_iff (by simp)).mpr ?_
669+
simpa using hst.le
670+
· contrapose! hst with heq
671+
apply le_of_eq
672+
unfold MulArchimedeanSubgroup.of_ne_top at heq
673+
simpa [MulArchimedeanClass.mk_surjective] using heq
674+
675+
variable (M) in
676+
@[to_additive]
677+
theorem antitone : Antitone (MulArchimedeanSubgroup (M := M)) := by
678+
intro s t hst
679+
obtain hs | rfl := ne_or_eq s ⊤
680+
· obtain ht | rfl := ne_or_eq t ⊤
681+
· exact
682+
((strictAntiOn M).le_iff_le (Set.mem_Iio.mpr ht.lt_top) (Set.mem_Iio.mpr hs.lt_top)).mpr hst
683+
· simp
684+
· have : t = ⊤ := eq_top_iff.mpr hst
685+
rw [this]
686+
687+
end MulArchimedeanSubgroup

‎Mathlib/Algebra/Order/Module/Archimedean.lean‎

Lines changed: 191 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,191 @@
1+
/-
2+
Copyright (c) 2025 Weiyi Wang. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Weiyi Wang
5+
-/
6+
7+
import Mathlib.Algebra.Module.Submodule.Order
8+
import Mathlib.Algebra.Order.Archimedean.Class
9+
import Mathlib.Algebra.Order.Module.Basic
10+
import Mathlib.LinearAlgebra.DFinsupp
11+
12+
/-!
13+
# Further lemmas related to Archimedean classes for ordered module.
14+
15+
## Main definitions
16+
* `ArchimedeanSubgroup.submodule`: `ArchimedeanSubgroup` as a submodule.
17+
* `IsArchimedeanGrade`: a submodule `G` is called an Archimedean grade at
18+
`A : ArchimedeanClass M` iff $ Submodule[A, \top] = G \oplus Submodule(A, \top] $.
19+
-/
20+
21+
variable {M : Type*}
22+
variable [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M]
23+
24+
variable (K : Type*) [Ring K] [LinearOrder K] [IsOrderedRing K] [Archimedean K]
25+
variable [Module K M] [PosSMulMono K M]
26+
27+
/-- For a ordered module over an `Archimedean` ring, `ArchimedeanSubgroup` is a submodule. -/
28+
noncomputable
29+
def ArchimedeanSubgroup.submodule (s : UpperSet (ArchimedeanClass M)) : Submodule K M where
30+
__ := ArchimedeanSubgroup s
31+
smul_mem' k {a} := by
32+
obtain rfl | hs := eq_or_ne s ⊤
33+
· suffices a = 0 → k • a = 0 by simpa using this
34+
intro ha
35+
simp [ha]
36+
· change a ∈ ArchimedeanSubgroup s → k • a ∈ ArchimedeanSubgroup s
37+
simp_rw [mem_iff_of_ne_top hs]
38+
intro ha
39+
by_cases htrivial : Nontrivial K
40+
· obtain ⟨n, hn⟩ := Archimedean.arch |k| (show 0 < 1 by simp)
41+
refine s.upper (ArchimedeanClass.mk_le_mk.mpr ⟨n, ?_⟩) ha
42+
have : n • |a| = (n • (1 : K)) • |a| := by rw [smul_assoc, one_smul]
43+
rw [this, abs_smul]
44+
exact smul_le_smul_of_nonneg_right hn (by simp)
45+
· have : Subsingleton K := not_nontrivial_iff_subsingleton.mp htrivial
46+
rw [Subsingleton.eq_zero k]
47+
simpa using (IsUpperSet.top_mem s.upper).mpr <| UpperSet.coe_nonempty.mpr hs
48+
49+
theorem ArchimedeanSubgroup.mem_submodule_iff_of_ne_top {a : M} {s : UpperSet (ArchimedeanClass M)}
50+
(hs : s ≠ ⊤) : a ∈ ArchimedeanSubgroup.submodule K s ↔ ArchimedeanClass.mk a ∈ s :=
51+
mem_iff_of_ne_top hs
52+
53+
theorem ArchimedeanSubgroup.mem_submodule_Ioi_iff_of_ne_top {a : M} {A : ArchimedeanClass M}
54+
(hA : A ≠ ⊤) :
55+
a ∈ ArchimedeanSubgroup.submodule K (UpperSet.Ioi A) ↔ A < ArchimedeanClass.mk a :=
56+
mem_Ioi_iff_of_ne_top hA
57+
58+
@[simp]
59+
theorem ArchimedeanSubgroup.mem_submodule_Ici_iff_of_ne_top {a : M} {A : ArchimedeanClass M}
60+
: a ∈ ArchimedeanSubgroup.submodule K (UpperSet.Ici A) ↔ A ≤ ArchimedeanClass.mk a :=
61+
mem_Ici_iff
62+
63+
variable (M) in
64+
@[simp]
65+
theorem ArchimedeanSubgroup.submodule_eq_bot :
66+
ArchimedeanSubgroup.submodule K (M := M) ⊤ = ⊥ := by
67+
rw [Submodule.eq_bot_iff]
68+
change ∀ x ∈ ArchimedeanSubgroup ⊤, x = 0
69+
simp
70+
71+
variable (M) in
72+
@[simp]
73+
theorem ArchimedeanSubgroup.submodule_eq_bot_of_Ici_top :
74+
ArchimedeanSubgroup.submodule K (M := M) (UpperSet.Ici ⊤) = ⊥ := by
75+
rw [Submodule.eq_bot_iff]
76+
change ∀ x ∈ ArchimedeanSubgroup (UpperSet.Ici ⊤), x = 0
77+
simp
78+
79+
variable (M) in
80+
theorem ArchimedeanSubgroup.submodule_strictAntiOn :
81+
StrictAntiOn (ArchimedeanSubgroup.submodule (M := M) K) (Set.Iio ⊤) :=
82+
ArchimedeanSubgroup.strictAntiOn M
83+
84+
variable (M) in
85+
theorem ArchimedeanSubgroup.submodule_antitone :
86+
Antitone (ArchimedeanSubgroup.submodule (M := M) K) :=
87+
ArchimedeanSubgroup.antitone M
88+
89+
/-- a submodule `G` is called an Archimedean grade at `A : ArchimedeanClass M`
90+
iff $ Submodule[A, \top] = G \oplus Submodule(A, \top] $.
91+
92+
Such submodule is `Archimedean` itself (see `IsArchimedeanGrade.archimedean`),
93+
and a family of such submodules is linearly independent (see `IsArchimedeanGrade.iSupIndep`).
94+
-/
95+
def IsArchimedeanGrade (A : ArchimedeanClass M) (G : Submodule K M) :=
96+
Disjoint (ArchimedeanSubgroup.submodule K (UpperSet.Ioi A)) G ∧
97+
(ArchimedeanSubgroup.submodule K (UpperSet.Ioi A)) ⊔ G =
98+
(ArchimedeanSubgroup.submodule K (UpperSet.Ici A))
99+
100+
namespace IsArchimedeanGrade
101+
variable {A : ArchimedeanClass M} {G : Submodule K M}
102+
103+
theorem disjoint (hgrade : IsArchimedeanGrade K A G) :
104+
Disjoint (ArchimedeanSubgroup.submodule K (UpperSet.Ioi A)) G := hgrade.1
105+
106+
theorem sup_eq (hgrade : IsArchimedeanGrade K A G) :
107+
(ArchimedeanSubgroup.submodule K (UpperSet.Ioi A)) ⊔ G =
108+
(ArchimedeanSubgroup.submodule K (UpperSet.Ici A)) := hgrade.2
109+
110+
omit A in
111+
theorem eq_bot_of_top (hgrade : IsArchimedeanGrade K (⊤ : ArchimedeanClass M) G) : G = ⊥ := by
112+
obtain hsup := hgrade.sup_eq
113+
simpa using hsup
114+
115+
theorem nontrivial_of_ne_top (hgrade : IsArchimedeanGrade K A G) (h : A ≠ ⊤) :
116+
Nontrivial G := by
117+
obtain hcodisj := hgrade.sup_eq
118+
contrapose! hcodisj with htrivial
119+
have hbot : G = ⊥ := by simpa using Submodule.nontrivial_iff_ne_bot.not.mp htrivial
120+
have hA : UpperSet.Ioi A ∈ Set.Iio ⊤ := by
121+
suffices UpperSet.Ioi A < ⊤ by simpa using this
122+
refine Ne.lt_top (UpperSet.ext_iff.ne.mpr ?_)
123+
simpa using h
124+
rw [hbot, sup_bot_eq]
125+
rw [((ArchimedeanSubgroup.submodule_strictAntiOn M K).eq_iff_eq hA (by simp)).ne]
126+
rw [UpperSet.ext_iff.ne]
127+
by_contra!
128+
have h' : A ∈ Set.Ici A := Set.left_mem_Ici
129+
simp [show Set.Ici A = Set.Ioi A by exact this] at h'
130+
131+
theorem le_Ici (hgrade : IsArchimedeanGrade K A G) :
132+
G ≤ (ArchimedeanSubgroup.submodule K (UpperSet.Ici A)) := by
133+
simp [← hgrade.sup_eq]
134+
135+
theorem archimedeanClass_eq_of_mem (hgrade : IsArchimedeanGrade K A G) {a : M}
136+
(ha : a ∈ G) (h0 : a ≠ 0) : ArchimedeanClass.mk a = A := by
137+
apply le_antisymm
138+
· have hA : (UpperSet.Ioi A) ≠ ⊤ := by
139+
contrapose! h0
140+
have : A = ⊤ := IsMax.eq_top (Set.Ioi_eq_empty_iff.mp (UpperSet.ext_iff.mp h0))
141+
rw [this] at hgrade
142+
rw [hgrade.eq_bot_of_top] at ha
143+
exact (Submodule.mem_bot _).mp ha
144+
contrapose! h0 with hlt
145+
have ha' : a ∈ ArchimedeanSubgroup.submodule K (UpperSet.Ioi A) :=
146+
(ArchimedeanSubgroup.mem_iff_of_ne_top hA).mpr hlt
147+
exact (Submodule.disjoint_def.mp hgrade.disjoint) a ha' ha
148+
· apply (ArchimedeanSubgroup.mem_iff_of_ne_top (show (UpperSet.Ici A) ≠ ⊤ by simp)).mp
149+
exact Set.mem_of_subset_of_mem hgrade.le_Ici ha
150+
151+
theorem archimedean (hgrade : IsArchimedeanGrade K A G) : Archimedean G := by
152+
apply ArchimedeanClass.archimedean_of_mk_eq_mk
153+
intro a ha b hb
154+
suffices ArchimedeanClass.mk a.val = ArchimedeanClass.mk b.val by
155+
rw [ArchimedeanClass.mk_eq_mk] at this ⊢
156+
exact this
157+
rw [hgrade.archimedeanClass_eq_of_mem K a.prop (by simpa using ha)]
158+
rw [hgrade.archimedeanClass_eq_of_mem K b.prop (by simpa using hb)]
159+
160+
end IsArchimedeanGrade
161+
162+
theorem IsArchimedeanGrade.iSupIndep {F : ArchimedeanClass M → Submodule K M}
163+
(hgrade : ∀ A : ArchimedeanClass M, IsArchimedeanGrade K A (F A)) : iSupIndep F := by
164+
rw [iSupIndep_def]
165+
intro A
166+
rw [Submodule.disjoint_def']
167+
intro a ha b hb hab
168+
obtain ⟨f, hf⟩ := (Submodule.mem_iSup_iff_exists_dfinsupp' _ b).mp hb
169+
obtain hf' := congrArg ArchimedeanClass.mk hf
170+
contrapose! hf' with h0
171+
rw [← hab, DFinsupp.sum]
172+
by_cases hnonempty : f.support.Nonempty
173+
· have hmem (x : ArchimedeanClass M) : (f x).val ∈ F x :=
174+
Set.mem_of_mem_of_subset (f x).prop (by simp)
175+
have hmono : StrictMonoOn (fun i ↦ ArchimedeanClass.mk (f i).val) f.support := by
176+
intro x hx y hy hxy
177+
change ArchimedeanClass.mk (f x).val < ArchimedeanClass.mk (f y).val
178+
rw [(hgrade x).archimedeanClass_eq_of_mem K (hmem x) (by simpa using hx)]
179+
rw [(hgrade y).archimedeanClass_eq_of_mem K (hmem y) (by simpa using hy)]
180+
exact hxy
181+
rw [ArchimedeanClass.mk_sum hnonempty hmono]
182+
rw [(hgrade _).archimedeanClass_eq_of_mem K (hmem _)
183+
(by simpa using Finset.min'_mem f.support hnonempty)]
184+
by_contra!
185+
obtain h := this ▸ Finset.min'_mem f.support hnonempty
186+
contrapose! h
187+
rw [DFinsupp.notMem_support_iff, (hgrade _).archimedeanClass_eq_of_mem K ha h0]
188+
simpa using (f A).prop
189+
· rw [Finset.not_nonempty_iff_eq_empty.mp hnonempty]
190+
symm
191+
simpa using h0

0 commit comments

Comments
 (0)