feat: more API about order types

Mathlib.lean

@@ -5652,6 +5652,8 @@ public import Mathlib.Order.SymmDiff
 public import Mathlib.Order.Synonym
 public import Mathlib.Order.TeichmullerTukey
 public import Mathlib.Order.TransfiniteIteration
+public import Mathlib.Order.Types.Defs
+public import Mathlib.Order.Types.Basic
 public import Mathlib.Order.TypeTags
 public import Mathlib.Order.ULift
 public import Mathlib.Order.UpperLower.Basic

Mathlib/Data/Sum/Order.lean

@@ -717,6 +717,22 @@ theorem sumLexDualAntidistrib_symm_inr :
     (sumLexDualAntidistrib α β).symm (inr (toDual a)) = toDual (inl a) :=
   rfl
 
+/-- `Equiv.sumEmpty` as an `OrderIso` with the lexicographic sum. -/
+def sumLexEmpty [IsEmpty β] :
+    Lex (α ⊕ β) ≃o α := RelIso.sumLexEmpty ..
+
+/-- `Equiv.emptySum` as an `OrderIso` with the lexicographic sum. -/
+def emptySumLex [IsEmpty β] :
+    Lex (β ⊕ α) ≃o α := RelIso.emptySumLex ..
+
+@[simp]
+lemma sumLexEmpty_apply_inl [IsEmpty β] (x : α) :
+  sumLexEmpty (β := β) (toLex <| .inl x) = x := rfl
+
+@[simp]
+lemma emptySumLex_apply_inr [IsEmpty β] (x : α) :
+  emptySumLex (β := β) (toLex <| .inr x) = x := rfl
+
 end OrderIso
 
 variable [LE α]

Mathlib/Order/Category/LinOrd.lean

@@ -20,25 +20,8 @@ open CategoryTheory
 
 universe u
 
-/-- The category of linear orders. -/
-structure LinOrd where
-  /-- Construct a bundled `LinOrd` from the underlying type and typeclass. -/
-  of ::
-  /-- The underlying linearly ordered type. -/
-  (carrier : Type*)
-  [str : LinearOrder carrier]
-
-attribute [instance] LinOrd.str
-
-initialize_simps_projections LinOrd (carrier → coe, -str)
-
 namespace LinOrd
 
-instance : CoeSort LinOrd (Type _) :=
-  ⟨LinOrd.carrier⟩
-
-attribute [coe] LinOrd.carrier
-
 set_option backward.privateInPublic true in
 /-- The type of morphisms in `LinOrd R`. -/
 @[ext]

Mathlib/Order/Defs/LinearOrder.lean

@@ -236,4 +236,25 @@ instance : Std.LawfulBCmp (compare (α := α)) where
 
 end Ord
 
+/-- The category of linear orders. -/
+structure LinOrd where
+  /-- Construct a bundled `LinOrd` from the underlying type and typeclass. -/
+  of ::
+  /-- The underlying linearly ordered type. -/
+  (carrier : Type*)
+  [str : LinearOrder carrier]
+
+attribute [instance] LinOrd.str
+
+initialize_simps_projections LinOrd (carrier → coe, -str)
+
+namespace LinOrd
+
+instance : CoeSort LinOrd (Type _) :=
+  ⟨LinOrd.carrier⟩
+
+attribute [coe] LinOrd.carrier
+
+end LinOrd
+
 end LinearOrder

Mathlib/Order/Hom/Basic.lean

@@ -884,6 +884,13 @@ def prodComm : α × β ≃o β × α where
   toEquiv := Equiv.prodComm α β
   map_rel_iff' := Prod.swap_le_swap
 
+/-- `Equiv.prodAssoc` promoted to an order isomorphism. -/
+@[simps! (attr := grind =)]
+def prodAssoc (α β γ : Type*) [LE α] [LE β] [LE γ] :
+    (α × β) × γ ≃o α × (β × γ) where
+  toEquiv := .prodAssoc α β γ
+  map_rel_iff' := @fun ⟨⟨_, _⟩, _⟩ ⟨⟨_, _⟩, _⟩ ↦ by simp [Equiv.prodAssoc, and_assoc]
+
 @[simp]
 theorem coe_prodComm : ⇑(prodComm : α × β ≃o β × α) = Prod.swap :=
   rfl
@@ -1069,6 +1076,10 @@ noncomputable def ofUnique
   toEquiv := Equiv.ofUnique α β
   map_rel_iff' := by simp
 
+/-- `Equiv.equivOfIsEmpty` promoted to an `OrderIso`. -/
+def ofIsEmpty (α β : Type*) [Preorder α] [Preorder β] [IsEmpty α] [IsEmpty β] : α ≃o β :=
+  ⟨Equiv.equivOfIsEmpty α β, @isEmptyElim _ _ _⟩
+
 end OrderIso
 
 namespace Equiv

Mathlib/Order/Hom/Lex.lean

@@ -179,4 +179,33 @@ variable {α β} in
 theorem uniqueProd_apply [Preorder α] [Unique α] [LE β] (x : α ×ₗ β) :
     uniqueProd α β x = (ofLex x).2 := rfl
 
+/-- `Equiv.prodAssoc` promoted to an order isomorphism of lexicographic products. -/
+@[simps!]
+def prodLexAssoc (α β γ : Type*)
+    [Preorder α] [Preorder β] [Preorder γ] : (α ×ₗ β) ×ₗ γ ≃o α ×ₗ β ×ₗ γ where
+  toEquiv := .trans ofLex <| .trans (.prodCongr ofLex <| .refl _) <|
+      .trans (.prodAssoc α β γ) <| .trans (.prodCongr (.refl _) toLex) <| toLex
+  map_rel_iff' := by
+    simp only [Prod.Lex.le_iff, Prod.Lex.lt_iff, Equiv.trans_apply, Equiv.prodCongr_apply,
+      Equiv.prodAssoc_apply]
+    grind [EmbeddingLike.apply_eq_iff_eq, ofLex_toLex]
+
+/-- `Equiv.sumProdDistrib` promoted to an order isomorphism of lexicographic products.
+
+Right distributivity doesn't hold. A counterexample is `ℕ ×ₗ (Unit ⊕ₗ Unit) ≃o ℕ`
+which is not isomorphic to `ℕ ×ₗ Unit ⊕ₗ ℕ ×ₗ Unit ≃o ℕ ⊕ₗ ℕ`. -/
+@[simps!]
+def sumLexProdLexDistrib (α β γ : Type*)
+    [Preorder α] [Preorder β] [Preorder γ] : (α ⊕ₗ β) ×ₗ γ ≃o α ×ₗ γ ⊕ₗ β ×ₗ γ where
+  toEquiv := .trans ofLex <| .trans (.prodCongr ofLex <| .refl _) <|
+    .trans (.sumProdDistrib α β γ) <| .trans (.sumCongr toLex toLex) toLex
+  map_rel_iff' := by simp [Prod.Lex.le_iff]
+
+/-- `Equiv.prodCongr` promoted to an order isomorphism between lexicographic products. -/
+@[simps! apply]
+def prodLexCongr {α β γ δ : Type*} [Preorder α] [Preorder β]
+    [Preorder γ] [Preorder δ] (ea : α ≃o β) (eb : γ ≃o δ) : α ×ₗ γ ≃o β ×ₗ δ where
+  toEquiv := ofLex.trans ((Equiv.prodCongr ea eb).trans toLex)
+  map_rel_iff' := by simp [Prod.Lex.le_iff]
+
 end Prod.Lex

Mathlib/Order/Types/Basic.lean

@@ -0,0 +1,145 @@
+/-
+Copyright (c) 2025 Yan Yablonovskiy. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yan Yablonovskiy
+-/
+module
+
+public import Mathlib.Data.Real.Basic
+public import Mathlib.SetTheory.Cardinal.Order
+public import Mathlib.Algebra.Ring.Defs
+public import Mathlib.Order.Fin.Basic
+public import Mathlib.Order.Types.Defs
+public import Mathlib.Order.Interval.Set.Basic
+
+/-!
+
+## Main definitions
+
+* `OrderType.card o`: the cardinality of an OrderType `o`.
+* `o₁ + o₂`: the lexicographic sum of order types, which forms an `AddMonoid`.
+* `o₁ * o₂`: the lexicographic product of order types, which forms a `MonoidWithZero`.
+
+## Notation
+
+The following are notations in the `OrderType` namespace:
+
+* `η` is a notation for the order type of `ℚ` with its natural order.
+* `θ` is a notation for the order type of `ℝ` with its natural order.
+
+## References
+
+* <https://en.wikipedia.org/wiki/Order_type>
+* Dauben, J. W. Georg Cantor: His Mathematics and Philosophy of the Infinite. Princeton,
+  NJ: Princeton University Press, 1990.
+* Enderton, Herbert B. Elements of Set Theory. United Kingdom: Academic Press, 1977.
+
+## Tags
+
+order type, order isomorphism, linear order
+-/
+
+public noncomputable section
+
+namespace OrderType
+
+universe u v w w'
+
+variable {α : Type u} {β : Type v} {γ : Type w} {δ : Type w'}
+
+instance : ZeroLEOneClass OrderType :=
+  ⟨OrderType.zero_le _⟩
+
+instance : Add OrderType.{u} where
+  add := Quotient.map₂ (fun r s ↦ ⟨(r ⊕ₗ s)⟩)
+    fun _ _ ha _ _ hb ↦ ⟨OrderIso.sumLexCongr (Classical.choice ha) (Classical.choice hb)⟩
+
+instance : HAdd OrderType.{u} OrderType.{v} OrderType.{max u v} where
+  hAdd := Quotient.map₂ (fun r s ↦ ⟨(r ⊕ₗ s)⟩)
+   fun _ _ ha _ _ hb ↦ ⟨OrderIso.sumLexCongr (Classical.choice ha) (Classical.choice hb)⟩
+
+instance : AddMonoid OrderType where
+  add_assoc o₁ o₂ o₃ :=
+    inductionOn₃ o₁ o₂ o₃ fun α _ β _ γ _ ↦ (OrderIso.sumLexAssoc α β γ).orderType_eq
+  zero_add o :=
+    inductionOn o (fun α _ ↦ RelIso.orderType_eq OrderIso.emptySumLex)
+  add_zero o :=
+   inductionOn o (fun α _ ↦ RelIso.orderType_eq OrderIso.sumLexEmpty)
+  nsmul := nsmulRec
+
+instance (n : Nat) : OfNat OrderType n where
+ ofNat := Fin n |> type
+
+@[simp]
+lemma type_add (α : Type u) (β : Type v) [LinearOrder α] [LinearOrder β] :
+    type (α ⊕ₗ β) = type α + type β := rfl
+
+instance : Mul OrderType where
+  mul := Quotient.map₂ (fun r s ↦ ⟨(s ×ₗ r)⟩)
+   fun _ _ ha _ _ hb ↦ ⟨Prod.Lex.prodLexCongr  (Classical.choice hb) (Classical.choice ha)⟩
+
+instance : HMul OrderType.{u} OrderType.{v} OrderType.{max u v} where
+  hMul := Quotient.map₂ (fun r s ↦ ⟨(s ×ₗ r)⟩)
+   fun _ _ ha _ _ hb ↦ ⟨Prod.Lex.prodLexCongr  (Classical.choice hb) (Classical.choice ha)⟩
+
+@[simp]
+lemma type_mul (α : Type u) (β : Type v) [LinearOrder α] [LinearOrder β] :
+    type (α ×ₗ β) = type β * type α := rfl
+
+instance : Monoid OrderType where
+  mul_assoc o₁ o₂ o₃ :=
+    inductionOn₃ o₁ o₂ o₃ (fun α _ β _ γ _ ↦
+    RelIso.orderType_eq (Prod.Lex.prodLexAssoc γ β α).symm)
+  one_mul o := inductionOn o (fun α _ ↦ RelIso.orderType_eq (Prod.Lex.prodUnique α PUnit))
+  mul_one o := inductionOn o (fun α _ ↦ RelIso.orderType_eq (Prod.Lex.uniqueProd PUnit α)) --6
+
+instance : LeftDistribClass OrderType where
+  left_distrib a b c := by
+    refine inductionOn₃ a b c (fun _ _ _ _ _ _ ↦ ?_)
+    simp only [←type_mul,←type_add]
+    exact RelIso.orderType_eq (Prod.Lex.sumLexProdLexDistrib _ _ _)
+
+/-- The order type of the rational numbers. -/
+def eta : OrderType := type ℚ
+
+/-- The order type of the real numbers. -/
+def theta : OrderType := type ℝ
+
+@[inherit_doc]
+scoped notation "η" => OrderType.eta
+recommended_spelling "eta" for "η" in [eta, «termη»]
+
+@[inherit_doc]
+scoped notation "θ" => OrderType.theta
+recommended_spelling "theta" for "θ" in [theta, «termθ»]
+
+section Cardinal
+
+open Cardinal
+
+/-- The cardinal of an `OrderType` is the cardinality of any type on which a relation
+with that order type is defined. -/
+@[expose]
+def card : OrderType → Cardinal :=
+  Quotient.map _ fun _ _ ⟨e⟩ ↦ ⟨e.toEquiv⟩
+
+@[simp]
+theorem card_type [LinearOrder α] : card (type α) = #α :=
+  rfl
+
+@[gcongr]
+theorem card_le_card {o₁ o₂ : OrderType} : o₁ ≤ o₂ → card o₁ ≤ card o₂ :=
+  inductionOn o₁ fun _ ↦ inductionOn o₂ fun _ _ ⟨f⟩ ↦ ⟨f.toEmbedding⟩
+
+theorem card_mono : Monotone card := by
+ rw [Monotone]; exact @card_le_card
+
+@[simp]
+theorem card_zero : card 0 = 0 := mk_eq_zero _
+
+@[simp]
+theorem card_one : card 1 = 1 := mk_eq_one _
+
+end Cardinal
+
+end OrderType