Skip to content

Commit 1f40b9f

Browse files
pecherskypechersky
committed
feat(Algebra/Order/{Monoid,GroupWithZero}/Lex): ordered inclusions and projections of prod of ordered groups (#22420)
1 parent 1a83ec9 commit 1f40b9f

File tree

5 files changed

+350
-0
lines changed

5 files changed

+350
-0
lines changed

‎Mathlib.lean

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -828,6 +828,7 @@ import Mathlib.Algebra.Order.GroupWithZero.Action.Synonym
828828
import Mathlib.Algebra.Order.GroupWithZero.Bounds
829829
import Mathlib.Algebra.Order.GroupWithZero.Canonical
830830
import Mathlib.Algebra.Order.GroupWithZero.Finset
831+
import Mathlib.Algebra.Order.GroupWithZero.Lex
831832
import Mathlib.Algebra.Order.GroupWithZero.Submonoid
832833
import Mathlib.Algebra.Order.GroupWithZero.Synonym
833834
import Mathlib.Algebra.Order.GroupWithZero.Unbundled
@@ -861,6 +862,7 @@ import Mathlib.Algebra.Order.Monoid.Basic
861862
import Mathlib.Algebra.Order.Monoid.Canonical.Basic
862863
import Mathlib.Algebra.Order.Monoid.Canonical.Defs
863864
import Mathlib.Algebra.Order.Monoid.Defs
865+
import Mathlib.Algebra.Order.Monoid.Lex
864866
import Mathlib.Algebra.Order.Monoid.NatCast
865867
import Mathlib.Algebra.Order.Monoid.OrderDual
866868
import Mathlib.Algebra.Order.Monoid.Prod
@@ -4887,6 +4889,7 @@ import Mathlib.Order.Preorder.Chain
48874889
import Mathlib.Order.Preorder.Finite
48884890
import Mathlib.Order.PrimeIdeal
48894891
import Mathlib.Order.PrimeSeparator
4892+
import Mathlib.Order.Prod.Lex.Hom
48904893
import Mathlib.Order.PropInstances
48914894
import Mathlib.Order.Radical
48924895
import Mathlib.Order.Rel.GaloisConnection

‎Mathlib/Algebra/Order/GroupWithZero/Lex.lean

Lines changed: 159 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,159 @@
1+
/-
2+
Copyright (c) 2025 Yakov Pechersky. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Yakov Pechersky
5+
-/
6+
import Mathlib.Algebra.GroupWithZero.ProdHom
7+
import Mathlib.Algebra.Order.Hom.Monoid
8+
import Mathlib.Algebra.Order.Monoid.Lex
9+
import Mathlib.Data.Prod.Lex
10+
11+
/-!
12+
# Order homomorphisms for products of linearly ordered groups with zero
13+
14+
This file defines order homomorphisms for products of linearly ordered groups with zero,
15+
which is identified with the `WithZero` of the lexicographic product of the units of the groups.
16+
17+
The product of linearly ordered groups with zero `WithZero (αˣ ×ₗ βˣ)` is a
18+
linearly ordered group with zero itself with natural inclusions but only one projection.
19+
One has to work with the lexicographic product of the units `αˣ ×ₗ βˣ` since otherwise,
20+
the plain product `αˣ × βˣ` would not be linearly ordered.
21+
22+
## TODO
23+
24+
Create the "LinOrdCommGrpWithZero" category.
25+
26+
-/
27+
28+
-- TODO: find a better place
29+
/-- `toLex` as a monoid isomorphism. -/
30+
def toLexMulEquiv (G H : Type*) [MulOneClass G] [MulOneClass H] : G × H ≃* G ×ₗ H where
31+
toFun := toLex
32+
invFun := ofLex
33+
left_inv := ofLex_toLex
34+
right_inv := toLex_ofLex
35+
map_mul' := toLex_mul
36+
37+
@[simp]
38+
lemma coe_toLexMulEquiv (G H : Type*) [MulOneClass G] [MulOneClass H] :
39+
⇑(toLexMulEquiv G H) = toLex :=
40+
rfl
41+
42+
@[simp]
43+
lemma coe_symm_toLexMulEquiv (G H : Type*) [MulOneClass G] [MulOneClass H] :
44+
⇑(toLexMulEquiv G H).symm = ofLex :=
45+
rfl
46+
47+
@[simp]
48+
lemma toEquiv_toLexMulEquiv (G H : Type*) [MulOneClass G] [MulOneClass H] :
49+
⇑(toLexMulEquiv G H : G × H ≃ G ×ₗ H) = toLex :=
50+
rfl
51+
52+
@[simp]
53+
lemma toEquiv_symm_toLexMulEquiv (G H : Type*) [MulOneClass G] [MulOneClass H] :
54+
⇑((toLexMulEquiv G H).symm : G ×ₗ H ≃ G × H) = ofLex :=
55+
rfl
56+
57+
namespace MonoidWithZeroHom
58+
59+
variable {M₀ N₀ : Type*}
60+
61+
lemma inl_mono [LinearOrderedCommGroupWithZero M₀] [GroupWithZero N₀] [Preorder N₀]
62+
[DecidablePred fun x : M₀ ↦ x = 0] : Monotone (inl M₀ N₀) := by
63+
refine (WithZero.map'_mono MonoidHom.inl_mono).comp ?_
64+
intro x y
65+
obtain rfl | ⟨x, rfl⟩ := GroupWithZero.eq_zero_or_unit x <;>
66+
obtain rfl | ⟨y, rfl⟩ := GroupWithZero.eq_zero_or_unit y <;>
67+
· simp [WithZero.zero_le, WithZero.withZeroUnitsEquiv]
68+
69+
lemma inl_strictMono [LinearOrderedCommGroupWithZero M₀] [GroupWithZero N₀] [PartialOrder N₀]
70+
[DecidablePred fun x : M₀ ↦ x = 0] : StrictMono (inl M₀ N₀) :=
71+
inl_mono.strictMono_of_injective inl_injective
72+
73+
lemma inr_mono [GroupWithZero M₀] [Preorder M₀] [LinearOrderedCommGroupWithZero N₀]
74+
[DecidablePred fun x : N₀ ↦ x = 0] : Monotone (inr M₀ N₀) := by
75+
refine (WithZero.map'_mono MonoidHom.inr_mono).comp ?_
76+
intro x y
77+
obtain rfl | ⟨x, rfl⟩ := GroupWithZero.eq_zero_or_unit x <;>
78+
obtain rfl | ⟨y, rfl⟩ := GroupWithZero.eq_zero_or_unit y <;>
79+
· simp [WithZero.zero_le, WithZero.withZeroUnitsEquiv]
80+
81+
lemma inr_strictMono [GroupWithZero M₀] [PartialOrder M₀] [LinearOrderedCommGroupWithZero N₀]
82+
[DecidablePred fun x : N₀ ↦ x = 0] : StrictMono (inr M₀ N₀) :=
83+
inr_mono.strictMono_of_injective inr_injective
84+
85+
lemma fst_mono [LinearOrderedCommGroupWithZero M₀] [GroupWithZero N₀] [Preorder N₀] :
86+
Monotone (fst M₀ N₀) := by
87+
refine WithZero.forall.mpr ?_
88+
simp +contextual [WithZero.forall, Prod.le_def]
89+
90+
91+
lemma snd_mono [GroupWithZero M₀] [Preorder M₀] [LinearOrderedCommGroupWithZero N₀] :
92+
Monotone (snd M₀ N₀) := by
93+
refine WithZero.forall.mpr ?_
94+
simp [WithZero.forall, Prod.le_def]
95+
96+
end MonoidWithZeroHom
97+
98+
namespace LinearOrderedCommGroupWithZero
99+
100+
variable (α β : Type*) [LinearOrderedCommGroupWithZero α] [LinearOrderedCommGroupWithZero β]
101+
102+
open MonoidWithZeroHom
103+
104+
/-- Given linearly ordered groups with zero M, N, the natural inclusion ordered homomorphism from
105+
M to `WithZero (Mˣ ×ₗ Nˣ)`, which is the linearly ordered group with zero that can be identified
106+
as their product. -/
107+
@[simps!]
108+
nonrec def inl : α →*₀o WithZero (αˣ ×ₗ βˣ) where
109+
__ := (WithZero.map' (toLexMulEquiv ..).toMonoidHom).comp (inl α β)
110+
monotone' := by simpa using (WithZero.map'_mono (Prod.Lex.toLex_mono)).comp inl_mono
111+
112+
/-- Given linearly ordered groups with zero M, N, the natural inclusion ordered homomorphism from
113+
N to `WithZero (Mˣ ×ₗ Nˣ)`, which is the linearly ordered group with zero that can be identified
114+
as their product. -/
115+
@[simps!]
116+
nonrec def inr : β →*₀o WithZero (αˣ ×ₗ βˣ) where
117+
__ := (WithZero.map' (toLexMulEquiv ..).toMonoidHom).comp (inr α β)
118+
monotone' := by simpa using (WithZero.map'_mono (Prod.Lex.toLex_mono)).comp inr_mono
119+
120+
/-- Given linearly ordered groups with zero M, N, the natural projection ordered homomorphism from
121+
`WithZero (Mˣ ×ₗ Nˣ)` to M, which is the linearly ordered group with zero that can be identified
122+
as their product. -/
123+
@[simps!]
124+
nonrec def fst : WithZero (αˣ ×ₗ βˣ) →*₀o α where
125+
__ := (fst α β).comp (WithZero.map' (toLexMulEquiv ..).symm.toMonoidHom)
126+
monotone' := by
127+
-- this can't rely on `Monotone.comp` since `ofLex` is not monotone
128+
intro x y
129+
cases x <;>
130+
cases y
131+
· simp
132+
· simp
133+
· simp [WithZero.zero_lt_coe]
134+
· simpa using Prod.Lex.monotone_fst _ _
135+
136+
@[simp]
137+
theorem fst_comp_inl : (fst _ _).comp (inl α β) = .id α := by
138+
ext x
139+
obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit x <;>
140+
simp
141+
142+
variable {α β}
143+
144+
lemma inl_eq_coe_inlₗ {m : α} (hm : m ≠ 0) :
145+
inl α β m = OrderMonoidHom.inlₗ αˣ βˣ (Units.mk0 _ hm) := by
146+
lift m to αˣ using isUnit_iff_ne_zero.mpr hm
147+
simp
148+
149+
lemma inr_eq_coe_inrₗ {n : β} (hn : n ≠ 0) :
150+
inr α β n = OrderMonoidHom.inrₗ αˣ βˣ (Units.mk0 _ hn) := by
151+
lift n to βˣ using isUnit_iff_ne_zero.mpr hn
152+
simp
153+
154+
theorem inl_mul_inr_eq_coe_toLex {m : α} {n : β} (hm : m ≠ 0) (hn : n ≠ 0) :
155+
inl α β m * inr α β n = toLex (Units.mk0 _ hm, Units.mk0 _ hn) := by
156+
rw [inl_eq_coe_inlₗ hm, inr_eq_coe_inrₗ hn,
157+
← WithZero.coe_mul, OrderMonoidHom.inlₗ_mul_inrₗ_eq_toLex]
158+
159+
end LinearOrderedCommGroupWithZero

‎Mathlib/Algebra/Order/Hom/Monoid.lean

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -926,15 +926,31 @@ end Mul
926926
section LinearOrderedCommMonoidWithZero
927927

928928
variable {hα : Preorder α} {hα' : MulZeroOneClass α} {hβ : Preorder β} {hβ' : MulZeroOneClass β}
929+
{hγ : Preorder γ} {hγ' : MulZeroOneClass γ}
929930

930931
@[simp]
931932
theorem toMonoidWithZeroHom_eq_coe (f : α →*₀o β) : f.toMonoidWithZeroHom = f := by
932933
rfl
933934

935+
@[simp]
936+
theorem toMonoidWithZeroHom_mk (f : α →*₀ β) (hf : Monotone f) :
937+
((OrderMonoidWithZeroHom.mk f hf) : α →*₀ β) = f := by
938+
rfl
939+
940+
@[simp]
941+
lemma toMonoidWithZeroHom_coe (f : β →*₀o γ) (g : α →*₀o β) :
942+
(f.comp g : α →*₀ γ) = (f : β →*₀ γ).comp g :=
943+
rfl
944+
934945
@[simp]
935946
theorem toOrderMonoidHom_eq_coe (f : α →*₀o β) : f.toOrderMonoidHom = f :=
936947
rfl
937948

949+
@[simp]
950+
lemma toOrderMonoidHom_comp (f : β →*₀o γ) (g : α →*₀o β) :
951+
(f.comp g : α →*o γ) = (f : β →*o γ).comp g :=
952+
rfl
953+
938954
end LinearOrderedCommMonoidWithZero
939955

940956
end OrderMonoidWithZeroHom

‎Mathlib/Algebra/Order/Monoid/Lex.lean

Lines changed: 154 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,154 @@
1+
/-
2+
Copyright (c) 2025 Yakov Pechersky. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Yakov Pechersky
5+
-/
6+
import Mathlib.Algebra.Group.Prod
7+
import Mathlib.Algebra.Order.Hom.Monoid
8+
import Mathlib.Data.Prod.Lex
9+
import Mathlib.Order.Prod.Lex.Hom
10+
11+
/-!
12+
# Order homomorphisms for products of ordered monoids
13+
14+
This file defines order homomorphisms for products of ordered monoids, for both the plain product
15+
and the lexicographic product.
16+
17+
The product of ordered monoids `α × β` is an ordered monoid itself with both natural inclusions
18+
and projections, making it the coproduct as well.
19+
20+
## TODO
21+
22+
Create the "OrdCommMon" category.
23+
24+
-/
25+
26+
namespace MonoidHom
27+
28+
variable {α β : Type*} [Monoid α] [Preorder α] [Monoid β] [Preorder β]
29+
30+
@[to_additive]
31+
lemma inl_mono : Monotone (MonoidHom.inl α β) :=
32+
fun _ _ ↦ by simp
33+
34+
@[to_additive]
35+
lemma inl_strictMono : StrictMono (MonoidHom.inl α β) :=
36+
fun _ _ ↦ by simp
37+
38+
@[to_additive]
39+
lemma inr_mono : Monotone (MonoidHom.inr α β) :=
40+
fun _ _ ↦ by simp
41+
42+
@[to_additive]
43+
lemma inr_strictMono : StrictMono (MonoidHom.inr α β) :=
44+
fun _ _ ↦ by simp
45+
46+
@[to_additive]
47+
lemma fst_mono : Monotone (MonoidHom.fst α β) :=
48+
fun _ _ ↦ by simp +contextual [Prod.le_def]
49+
50+
@[to_additive]
51+
lemma snd_mono : Monotone (MonoidHom.snd α β) :=
52+
fun _ _ ↦ by simp +contextual [Prod.le_def]
53+
54+
end MonoidHom
55+
56+
namespace OrderMonoidHom
57+
58+
variable (α β : Type*) [Monoid α] [PartialOrder α] [Monoid β] [Preorder β]
59+
60+
/-- Given ordered monoids M, N, the natural inclusion ordered homomorphism from M to M × N. -/
61+
@[to_additive (attr := simps!) "Given ordered additive monoids M, N, the natural inclusion ordered
62+
homomorphism from M to M × N."]
63+
def inl : α →*o α × β where
64+
__ := MonoidHom.inl _ _
65+
monotone' := MonoidHom.inl_mono
66+
67+
/-- Given ordered monoids M, N, the natural inclusion ordered homomorphism from N to M × N. -/
68+
@[to_additive (attr := simps!) "Given ordered additive monoids M, N, the natural inclusion ordered
69+
homomorphism from N to M × N."]
70+
def inr : β →*o α × β where
71+
__ := MonoidHom.inr _ _
72+
monotone' := MonoidHom.inr_mono
73+
74+
/-- Given ordered monoids M, N, the natural projection ordered homomorphism from M × N to M. -/
75+
@[to_additive (attr := simps!) "Given ordered additive monoids M, N, the natural projection ordered
76+
homomorphism from M × N to M."]
77+
def fst : α × β →*o α where
78+
__ := MonoidHom.fst _ _
79+
monotone' := MonoidHom.fst_mono
80+
81+
/-- Given ordered monoids M, N, the natural projection ordered homomorphism from M × N to N. -/
82+
@[to_additive (attr := simps!) "Given ordered additive monoids M, N, the natural projection ordered
83+
homomorphism from M × N to N."]
84+
def snd : α × β →*o β where
85+
__ := MonoidHom.snd _ _
86+
monotone' := MonoidHom.snd_mono
87+
88+
/-- Given ordered monoids M, N, the natural inclusion ordered homomorphism from M to the
89+
lexicographic M ×ₗ N. -/
90+
@[to_additive (attr := simps!) "Given ordered additive monoids M, N, the natural inclusion ordered
91+
homomorphism from M to the lexicographic M ×ₗ N."]
92+
def inlₗ : α →*o α ×ₗ β where
93+
__ := (Prod.Lex.toLexOrderHom).comp (inl α β)
94+
map_one' := rfl
95+
map_mul' := by simp [← toLex_mul]
96+
97+
/-- Given ordered monoids M, N, the natural inclusion ordered homomorphism from N to the
98+
lexicographic M ×ₗ N. -/
99+
@[to_additive (attr := simps!) "Given ordered additive monoids M, N, the natural inclusion ordered
100+
homomorphism from N to the lexicographic M ×ₗ N."]
101+
def inrₗ : β →*o (α ×ₗ β) where
102+
__ := Prod.Lex.toLexOrderHom.comp (inr α β)
103+
map_one' := rfl
104+
map_mul' := by simp [← toLex_mul]
105+
106+
/-- Given ordered monoids M, N, the natural projection ordered homomorphism from the
107+
lexicographic M ×ₗ N to M. -/
108+
@[to_additive (attr := simps!) "Given ordered additive monoids M, N, the natural projection ordered
109+
homomorphism from the lexicographic M ×ₗ N to M."]
110+
def fstₗ : (α ×ₗ β) →*o α where
111+
toFun p := (ofLex p).fst
112+
map_one' := rfl
113+
map_mul' := by simp
114+
monotone' := Prod.Lex.monotone_fst_ofLex
115+
116+
@[to_additive (attr := simp)]
117+
theorem fst_comp_inl : (fst α β).comp (inl α β) = .id α :=
118+
rfl
119+
120+
@[to_additive (attr := simp)]
121+
theorem fstₗ_comp_inlₗ : (fstₗ α β).comp (inlₗ α β) = .id α :=
122+
rfl
123+
124+
@[to_additive (attr := simp)]
125+
theorem snd_comp_inl : (snd α β).comp (inl α β) = 1 :=
126+
rfl
127+
128+
@[to_additive (attr := simp)]
129+
theorem fst_comp_inr : (fst α β).comp (inr α β) = 1 :=
130+
rfl
131+
132+
@[to_additive (attr := simp)]
133+
theorem snd_comp_inr : (snd α β).comp (inr α β) = .id β :=
134+
rfl
135+
136+
@[to_additive]
137+
theorem inl_mul_inr_eq_mk (m : α) (n : β) : inl α β m * inr α β n = (m, n) := by
138+
simp
139+
140+
@[to_additive]
141+
theorem inlₗ_mul_inrₗ_eq_toLex (m : α) (n : β) : inlₗ α β m * inrₗ α β n = toLex (m, n) := by
142+
simp [← toLex_mul]
143+
144+
variable {α β}
145+
146+
@[to_additive]
147+
theorem commute_inl_inr (m : α) (n : β) : Commute (inl α β m) (inr α β n) :=
148+
Commute.prod (.one_right m) (.one_left n)
149+
150+
@[to_additive]
151+
theorem commute_inlₗ_inrₗ (m : α) (n : β) : Commute (inlₗ α β m) (inrₗ α β n) :=
152+
Commute.prod (.one_right m) (.one_left n)
153+
154+
end OrderMonoidHom

‎Mathlib/Order/Prod/Lex/Hom.lean

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
/-
2+
Copyright (c) 2025 Yakov Pechersky. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Yakov Pechersky
5+
-/
6+
import Mathlib.Data.Prod.Lex
7+
import Mathlib.Order.Hom.Basic
8+
9+
/-!
10+
# Order homomorphism for `Prod.Lex`
11+
-/
12+
13+
/-- `toLex` as an `OrderHom`. -/
14+
@[simps]
15+
def Prod.Lex.toLexOrderHom {α β : Type*} [PartialOrder α] [Preorder β] :
16+
α × β →o α ×ₗ β where
17+
toFun := toLex
18+
monotone' := Prod.Lex.toLex_mono

0 commit comments

Comments
 (0)