[Merged by Bors] - feat(Algebra/Order/{Monoid,GroupWithZero}/Lex): ordered inclusions and projections of prod of ordered groups

Mathlib.lean

@@ -826,6 +826,7 @@ import Mathlib.Algebra.Order.GroupWithZero.Action.Synonym
 import Mathlib.Algebra.Order.GroupWithZero.Bounds
 import Mathlib.Algebra.Order.GroupWithZero.Canonical
 import Mathlib.Algebra.Order.GroupWithZero.Finset
+import Mathlib.Algebra.Order.GroupWithZero.Lex
 import Mathlib.Algebra.Order.GroupWithZero.Submonoid
 import Mathlib.Algebra.Order.GroupWithZero.Synonym
 import Mathlib.Algebra.Order.GroupWithZero.Unbundled
@@ -859,6 +860,7 @@ import Mathlib.Algebra.Order.Monoid.Basic
 import Mathlib.Algebra.Order.Monoid.Canonical.Basic
 import Mathlib.Algebra.Order.Monoid.Canonical.Defs
 import Mathlib.Algebra.Order.Monoid.Defs
+import Mathlib.Algebra.Order.Monoid.Lex
 import Mathlib.Algebra.Order.Monoid.NatCast
 import Mathlib.Algebra.Order.Monoid.OrderDual
 import Mathlib.Algebra.Order.Monoid.Prod
@@ -4869,6 +4871,7 @@ import Mathlib.Order.Preorder.Chain
 import Mathlib.Order.Preorder.Finite
 import Mathlib.Order.PrimeIdeal
 import Mathlib.Order.PrimeSeparator
+import Mathlib.Order.Prod.Lex.Hom
 import Mathlib.Order.PropInstances
 import Mathlib.Order.Radical
 import Mathlib.Order.Rel.GaloisConnection

Mathlib/Algebra/Order/GroupWithZero/Lex.lean

@@ -0,0 +1,159 @@
+/-
+Copyright (c) 2025 Yakov Pechersky. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yakov Pechersky
+-/
+import Mathlib.Algebra.GroupWithZero.ProdHom
+import Mathlib.Algebra.Order.Hom.Monoid
+import Mathlib.Algebra.Order.Monoid.Lex
+import Mathlib.Data.Prod.Lex
+
+/-!
+# Order homomorphisms for products of linearly ordered groups with zero
+
+This file defines order homomorphisms for products of linearly ordered groups with zero,
+which is identified with the `WithZero` of the lexicographic product of the units of the groups.
+
+The product of linearly ordered groups with zero `WithZero (αˣ ×ₗ βˣ)` is a
+linearly ordered group with zero itself with natural inclusions but only one projection.
+One has to work with the lexicographic product of the units `αˣ ×ₗ βˣ` since otherwise,
+the plain product `αˣ × βˣ` would not be linearly ordered.
+
+## TODO
+
+Create the "LinOrdCommGrpWithZero" category.
+
+-/
+
+-- TODO: find a better place
+/-- `toLex` as a monoid isomorphism. -/
+def toLexMulEquiv (G H : Type*) [MulOneClass G] [MulOneClass H] : G × H ≃* G ×ₗ H where
+  toFun := toLex
+  invFun := ofLex
+  left_inv := ofLex_toLex
+  right_inv := toLex_ofLex
+  map_mul' := toLex_mul
+
+@[simp]
+lemma coe_toLexMulEquiv (G H : Type*) [MulOneClass G] [MulOneClass H] :
+    ⇑(toLexMulEquiv G H) = toLex :=
+  rfl
+
+@[simp]
+lemma coe_symm_toLexMulEquiv (G H : Type*) [MulOneClass G] [MulOneClass H] :
+    ⇑(toLexMulEquiv G H).symm = ofLex :=
+  rfl
+
+@[simp]
+lemma toEquiv_toLexMulEquiv (G H : Type*) [MulOneClass G] [MulOneClass H] :
+    ⇑(toLexMulEquiv G H : G × H ≃ G ×ₗ H) = toLex :=
+  rfl
+
+@[simp]
+lemma toEquiv_symm_toLexMulEquiv (G H : Type*) [MulOneClass G] [MulOneClass H] :
+    ⇑((toLexMulEquiv G H).symm : G ×ₗ H ≃ G × H) = ofLex :=
+  rfl
+
+namespace MonoidWithZeroHom
+
+variable {M₀ N₀ : Type*}
+
+lemma inl_mono [LinearOrderedCommGroupWithZero M₀] [GroupWithZero N₀] [Preorder N₀]
+    [DecidablePred fun x : M₀ ↦ x = 0] : Monotone (inl M₀ N₀) := by
+  refine (WithZero.map'_mono MonoidHom.inl_mono).comp ?_
+  intro x y
+  obtain rfl | ⟨x, rfl⟩ := GroupWithZero.eq_zero_or_unit x <;>
+  obtain rfl | ⟨y, rfl⟩ := GroupWithZero.eq_zero_or_unit y <;>
+  · simp [WithZero.zero_le, WithZero.withZeroUnitsEquiv]
+
+lemma inl_strictMono [LinearOrderedCommGroupWithZero M₀] [GroupWithZero N₀] [PartialOrder N₀]
+    [DecidablePred fun x : M₀ ↦ x = 0] : StrictMono (inl M₀ N₀) :=
+  inl_mono.strictMono_of_injective inl_injective
+
+lemma inr_mono [GroupWithZero M₀] [Preorder M₀] [LinearOrderedCommGroupWithZero N₀]
+    [DecidablePred fun x : N₀ ↦ x = 0] : Monotone (inr M₀ N₀) := by
+  refine (WithZero.map'_mono MonoidHom.inr_mono).comp ?_
+  intro x y
+  obtain rfl | ⟨x, rfl⟩ := GroupWithZero.eq_zero_or_unit x <;>
+  obtain rfl | ⟨y, rfl⟩ := GroupWithZero.eq_zero_or_unit y <;>
+  · simp [WithZero.zero_le, WithZero.withZeroUnitsEquiv]
+
+lemma inr_strictMono [GroupWithZero M₀] [PartialOrder M₀] [LinearOrderedCommGroupWithZero N₀]
+    [DecidablePred fun x : N₀ ↦ x = 0] : StrictMono (inr M₀ N₀) :=
+  inr_mono.strictMono_of_injective inr_injective
+
+lemma fst_mono [LinearOrderedCommGroupWithZero M₀] [GroupWithZero N₀] [Preorder N₀] :
+    Monotone (fst M₀ N₀) := by
+  refine WithZero.forall.mpr ?_
+  simp +contextual [WithZero.forall, Prod.le_def]
+
+
+lemma snd_mono [GroupWithZero M₀] [Preorder M₀] [LinearOrderedCommGroupWithZero N₀] :
+    Monotone (snd M₀ N₀) := by
+  refine WithZero.forall.mpr ?_
+  simp [WithZero.forall, Prod.le_def]
+
+end MonoidWithZeroHom
+
+namespace LinearOrderedCommGroupWithZero
+
+variable (α β : Type*) [LinearOrderedCommGroupWithZero α] [LinearOrderedCommGroupWithZero β]
+
+open MonoidWithZeroHom
+
+/-- Given linearly ordered groups with zero M, N, the natural inclusion ordered homomorphism from
+M to `WithZero (Mˣ ×ₗ Nˣ)`, which is the linearly ordered group with zero that can be identified
+as their product. -/
+@[simps!]
+nonrec def inl : α →*₀o WithZero (αˣ ×ₗ βˣ) where
+  __ := (WithZero.map' (toLexMulEquiv ..).toMonoidHom).comp (inl α β)
+  monotone' := by simpa using (WithZero.map'_mono (Prod.Lex.toLex_mono)).comp inl_mono
+
+/-- Given linearly ordered groups with zero M, N, the natural inclusion ordered homomorphism from
+N to `WithZero (Mˣ ×ₗ Nˣ)`, which is the linearly ordered group with zero that can be identified
+as their product. -/
+@[simps!]
+nonrec def inr : β →*₀o WithZero (αˣ ×ₗ βˣ) where
+  __ := (WithZero.map' (toLexMulEquiv ..).toMonoidHom).comp (inr α β)
+  monotone' := by simpa using (WithZero.map'_mono (Prod.Lex.toLex_mono)).comp inr_mono
+
+/-- Given linearly ordered groups with zero M, N, the natural projection ordered homomorphism from
+`WithZero (Mˣ ×ₗ Nˣ)` to M, which is the linearly ordered group with zero that can be identified
+as their product. -/
+@[simps!]
+nonrec def fst : WithZero (αˣ ×ₗ βˣ) →*₀o α where
+  __ := (fst α β).comp (WithZero.map' (toLexMulEquiv ..).symm.toMonoidHom)
+  monotone' := by
+    -- this can't rely on `Monotone.comp` since `ofLex` is not monotone
+    intro x y
+    cases x <;>
+    cases y
+    · simp
+    · simp
+    · simp [WithZero.zero_lt_coe]
+    · simpa using Prod.Lex.monotone_fst _ _
+
+@[simp]
+theorem fst_comp_inl : (fst _ _).comp (inl α β) = .id α := by
+  ext x
+  obtain rfl | ⟨_, rfl⟩ := GroupWithZero.eq_zero_or_unit x <;>
+  simp
+
+variable {α β}
+
+lemma inl_eq_coe_inlₗ {m : α} (hm : m ≠ 0) :
+    inl α β m = OrderMonoidHom.inlₗ αˣ βˣ (Units.mk0 _ hm) := by
+  lift m to αˣ using isUnit_iff_ne_zero.mpr hm
+  simp
+
+lemma inr_eq_coe_inrₗ {n : β} (hn : n ≠ 0) :
+    inr α β n = OrderMonoidHom.inrₗ αˣ βˣ (Units.mk0 _ hn) := by
+  lift n to βˣ using isUnit_iff_ne_zero.mpr hn
+  simp
+
+theorem inl_mul_inr_eq_coe_toLex {m : α} {n : β} (hm : m ≠ 0) (hn : n ≠ 0) :
+    inl α β m * inr α β n = toLex (Units.mk0 _ hm, Units.mk0 _ hn) := by
+  rw [inl_eq_coe_inlₗ hm, inr_eq_coe_inrₗ hn,
+      ← WithZero.coe_mul, OrderMonoidHom.inlₗ_mul_inrₗ_eq_toLex]
+
+end LinearOrderedCommGroupWithZero

Mathlib/Algebra/Order/Hom/Monoid.lean

@@ -926,15 +926,31 @@ end Mul
 section LinearOrderedCommMonoidWithZero
 
 variable {hα : Preorder α} {hα' : MulZeroOneClass α} {hβ : Preorder β} {hβ' : MulZeroOneClass β}
+  {hγ : Preorder γ} {hγ' : MulZeroOneClass γ}
 
 @[simp]
 theorem toMonoidWithZeroHom_eq_coe (f : α →*₀o β) : f.toMonoidWithZeroHom = f := by
   rfl
 
+@[simp]
+theorem toMonoidWithZeroHom_mk (f : α →*₀ β) (hf : Monotone f) :
+    ((OrderMonoidWithZeroHom.mk f hf) : α →*₀ β) = f := by
+  rfl
+
+@[simp]
+lemma toMonoidWithZeroHom_coe (f : β →*₀o γ) (g : α →*₀o β) :
+    (f.comp g : α →*₀ γ) = (f : β →*₀ γ).comp g :=
+  rfl
+
 @[simp]
 theorem toOrderMonoidHom_eq_coe (f : α →*₀o β) : f.toOrderMonoidHom = f :=
   rfl
 
+@[simp]
+lemma toOrderMonoidHom_comp (f : β →*₀o γ) (g : α →*₀o β) :
+    (f.comp g : α →*o γ) = (f : β →*o γ).comp g :=
+  rfl
+
 end LinearOrderedCommMonoidWithZero
 
 end OrderMonoidWithZeroHom

Mathlib/Algebra/Order/Monoid/Lex.lean

@@ -0,0 +1,154 @@
+/-
+Copyright (c) 2025 Yakov Pechersky. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yakov Pechersky
+-/
+import Mathlib.Algebra.Group.Prod
+import Mathlib.Algebra.Order.Hom.Monoid
+import Mathlib.Data.Prod.Lex
+import Mathlib.Order.Prod.Lex.Hom
+
+/-!
+# Order homomorphisms for products of ordered monoids
+
+This file defines order homomorphisms for products of ordered monoids, for both the plain product
+and the lexicographic product.
+
+The product of ordered monoids `α × β` is an ordered monoid itself with both natural inclusions
+and projections, making it the coproduct as well.
+
+## TODO
+
+Create the "OrdCommMon" category.
+
+-/
+
+namespace MonoidHom
+
+variable {α β : Type*} [Monoid α] [Preorder α] [Monoid β] [Preorder β]
+
+@[to_additive]
+lemma inl_mono : Monotone (MonoidHom.inl α β) :=
+  fun _ _ ↦ by simp
+
+@[to_additive]
+lemma inl_strictMono : StrictMono (MonoidHom.inl α β) :=
+  fun _ _ ↦ by simp
+
+@[to_additive]
+lemma inr_mono : Monotone (MonoidHom.inr α β) :=
+  fun _ _ ↦ by simp
+
+@[to_additive]
+lemma inr_strictMono : StrictMono (MonoidHom.inr α β) :=
+  fun _ _ ↦ by simp
+
+@[to_additive]
+lemma fst_mono : Monotone (MonoidHom.fst α β) :=
+  fun _ _ ↦ by simp +contextual [Prod.le_def]
+
+@[to_additive]
+lemma snd_mono : Monotone (MonoidHom.snd α β) :=
+  fun _ _ ↦ by simp +contextual [Prod.le_def]
+
+end MonoidHom
+
+namespace OrderMonoidHom
+
+variable (α β : Type*) [Monoid α] [PartialOrder α] [Monoid β] [Preorder β]
+
+/-- Given ordered monoids M, N, the natural inclusion ordered homomorphism from M to M × N. -/
+@[to_additive (attr := simps!) "Given ordered additive monoids M, N, the natural inclusion ordered
+homomorphism from M to M × N."]
+def inl : α →*o α × β where
+  __ := MonoidHom.inl _ _
+  monotone' := MonoidHom.inl_mono
+
+/-- Given ordered monoids M, N, the natural inclusion ordered homomorphism from N to M × N. -/
+@[to_additive (attr := simps!) "Given ordered additive monoids M, N, the natural inclusion ordered
+homomorphism from N to M × N."]
+def inr : β →*o α × β where
+  __ := MonoidHom.inr _ _
+  monotone' := MonoidHom.inr_mono
+
+/-- Given ordered monoids M, N, the natural projection ordered homomorphism from M × N to M. -/
+@[to_additive (attr := simps!) "Given ordered additive monoids M, N, the natural projection ordered
+homomorphism from M × N to M."]
+def fst : α × β →*o α where
+  __ := MonoidHom.fst _ _
+  monotone' := MonoidHom.fst_mono
+
+/-- Given ordered monoids M, N, the natural projection ordered homomorphism from M × N to N. -/
+@[to_additive (attr := simps!) "Given ordered additive monoids M, N, the natural projection ordered
+homomorphism from M × N to N."]
+def snd : α × β →*o β where
+  __ := MonoidHom.snd _ _
+  monotone' := MonoidHom.snd_mono
+
+/-- Given ordered monoids M, N, the natural inclusion ordered homomorphism from M to the
+lexicographic M ×ₗ N. -/
+@[to_additive (attr := simps!) "Given ordered additive monoids M, N, the natural inclusion ordered
+homomorphism from M to the lexicographic M ×ₗ N."]
+def inlₗ : α →*o α ×ₗ β where
+  __ := (Prod.Lex.toLexOrderHom).comp (inl α β)
+  map_one' := rfl
+  map_mul' := by simp [← toLex_mul]
+
+/-- Given ordered monoids M, N, the natural inclusion ordered homomorphism from N to the
+lexicographic M ×ₗ N. -/
+@[to_additive (attr := simps!) "Given ordered additive monoids M, N, the natural inclusion ordered
+homomorphism from N to the lexicographic M ×ₗ N."]
+def inrₗ : β →*o (α ×ₗ β) where
+  __ := Prod.Lex.toLexOrderHom.comp (inr α β)
+  map_one' := rfl
+  map_mul' := by simp [← toLex_mul]
+
+/-- Given ordered monoids M, N, the natural projection ordered homomorphism from the
+lexicographic M ×ₗ N to M. -/
+@[to_additive (attr := simps!) "Given ordered additive monoids M, N, the natural projection ordered
+homomorphism from the lexicographic M ×ₗ N to M."]
+def fstₗ : (α ×ₗ β) →*o α where
+  toFun p := (ofLex p).fst
+  map_one' := rfl
+  map_mul' := by simp
+  monotone' := Prod.Lex.monotone_fst_ofLex
+
+@[to_additive (attr := simp)]
+theorem fst_comp_inl : (fst α β).comp (inl α β) = .id α :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem fstₗ_comp_inlₗ : (fstₗ α β).comp (inlₗ α β) = .id α :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem snd_comp_inl : (snd α β).comp (inl α β) = 1 :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem fst_comp_inr : (fst α β).comp (inr α β) = 1 :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem snd_comp_inr : (snd α β).comp (inr α β) = .id β :=
+  rfl
+
+@[to_additive]
+theorem inl_mul_inr_eq_mk (m : α) (n : β) : inl α β m * inr α β n = (m, n) := by
+  simp
+
+@[to_additive]
+theorem inlₗ_mul_inrₗ_eq_toLex (m : α) (n : β) : inlₗ α β m * inrₗ α β n = toLex (m, n) := by
+  simp [← toLex_mul]
+
+variable {α β}
+
+@[to_additive]
+theorem commute_inl_inr (m : α) (n : β) : Commute (inl α β m) (inr α β n) :=
+  Commute.prod (.one_right m) (.one_left n)
+
+@[to_additive]
+theorem commute_inlₗ_inrₗ (m : α) (n : β) : Commute (inlₗ α β m) (inrₗ α β n) :=
+  Commute.prod (.one_right m) (.one_left n)
+
+end OrderMonoidHom

Mathlib/Order/Prod/Lex/Hom.lean

@@ -0,0 +1,18 @@
+/-
+Copyright (c) 2025 Yakov Pechersky. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yakov Pechersky
+-/
+import Mathlib.Data.Prod.Lex
+import Mathlib.Order.Hom.Basic
+
+/-!
+# Order homomorphism for `Prod.Lex`
+-/
+
+/-- `toLex` as an `OrderHom`. -/
+@[simps]
+def Prod.Lex.toLexOrderHom {α β : Type*} [PartialOrder α] [Preorder β] :
+    α × β →o α ×ₗ β where
+  toFun := toLex
+  monotone' := Prod.Lex.toLex_mono