feat(algebra/order/hom/ring): There's at most one hom between linear ordered fields (#13601)

There is at most one ring homomorphism from a linear ordered field to an archimedean linear ordered field. Also generalize `map_rat_cast` to take in `ring_hom_class`.

Co-authored-by: Alex J. Best <alex.j.best@gmail.com>

Author: YaelDillies

src/algebra/order/hom/ring.lean

@@ -3,6 +3,7 @@ Copyright (c) 2022 Alex J. Best, Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alex J. Best, Yaël Dillies
 -/
+import algebra.order.archimedean
 import algebra.order.hom.monoid
 import algebra.order.ring
 import algebra.ring.equiv
@@ -277,6 +278,10 @@ ext e.left_inv
 @[simp] lemma symm_trans_self (e : α ≃+*o β) : e.symm.trans e = order_ring_iso.refl β :=
 ext e.right_inv
 
+lemma symm_bijective : bijective (order_ring_iso.symm : (α ≃+*o β) → β ≃+*o α) :=
+⟨λ f g h, f.symm_symm.symm.trans $ (congr_arg order_ring_iso.symm h).trans g.symm_symm,
+  λ f, ⟨f.symm, f.symm_symm⟩⟩
+
 end has_le
 
 section non_assoc_semiring
@@ -294,5 +299,54 @@ def to_order_ring_hom (f : α ≃+*o β) : α →+*o β :=
 @[simp]
 lemma coe_to_order_ring_hom_refl : (order_ring_iso.refl α : α →+*o α) = order_ring_hom.id α := rfl
 
+lemma to_order_ring_hom_injective : injective (to_order_ring_hom : (α ≃+*o β) → α →+*o β) :=
+λ f g h, fun_like.coe_injective $ by convert fun_like.ext'_iff.1 h
+
 end non_assoc_semiring
 end order_ring_iso
+
+/-!
+### Uniqueness
+
+There is at most one ordered ring homomorphism from a linear ordered field to an archimedean linear
+ordered field. Reciprocally, such an ordered ring homomorphism exists when the codomain is further
+conditionally complete.
+-/
+
+/-- There is at most one ordered ring homomorphism from a linear ordered field to an archimedean
+linear ordered field. -/
+-- TODO[gh-6025]: make this an instance once safe to do so
+lemma order_ring_hom.subsingleton [linear_ordered_field α] [linear_ordered_field β]
+  [archimedean β] :
+  subsingleton (α →+*o β) :=
+⟨λ f g, begin
+  ext x,
+  by_contra' h,
+  wlog h : f x < g x using [f g, g f],
+  { exact ne.lt_or_lt h },
+  obtain ⟨q, hf, hg⟩ := exists_rat_btwn h,
+  rw ←map_rat_cast f at hf,
+  rw ←map_rat_cast g at hg,
+  exact (lt_asymm ((order_hom_class.mono g).reflect_lt hg) $
+    (order_hom_class.mono f).reflect_lt hf).elim,
+end⟩
+
+local attribute [instance] order_ring_hom.subsingleton
+
+/-- There is at most one ordered ring isomorphism between a linear ordered field and an archimedean
+linear ordered field. -/
+-- TODO[gh-6025]: make this an instance once safe to do so
+lemma order_ring_iso.subsingleton_right [linear_ordered_field α] [linear_ordered_field β]
+  [archimedean β] :
+  subsingleton (α ≃+*o β) :=
+order_ring_iso.to_order_ring_hom_injective.subsingleton
+
+local attribute [instance] order_ring_iso.subsingleton_right
+
+/-- There is at most one ordered ring isomorphism between an archimedean linear ordered field and a
+linear ordered field. -/
+-- TODO[gh-6025]: make this an instance once safe to do so
+lemma order_ring_iso.subsingleton_left [linear_ordered_field α] [archimedean α]
+  [linear_ordered_field β] :
+  subsingleton (α ≃+*o β) :=
+order_ring_iso.symm_bijective.injective.subsingleton

src/algebra/star/basic.lean

@@ -264,7 +264,7 @@ def star_ring_equiv [non_unital_semiring R] [star_ring R] : R ≃+* Rᵐᵒᵖ :
 
 @[simp, norm_cast] lemma star_rat_cast [division_ring R] [char_zero R] [star_ring R] (r : ℚ) :
   star (r : R) = r :=
-(congr_arg unop ((star_ring_equiv : R ≃+* Rᵐᵒᵖ).to_ring_hom.map_rat_cast r)).trans (unop_rat_cast _)
+(congr_arg unop $ map_rat_cast (star_ring_equiv : R ≃+* Rᵐᵒᵖ) r).trans (unop_rat_cast _)
 
 /-- `star` as a ring automorphism, for commutative `R`. -/
 @[simps apply]

src/data/complex/basic.lean

@@ -400,8 +400,7 @@ by rw [← of_real_int_cast, of_real_re]
 @[simp, norm_cast] lemma int_cast_im (n : ℤ) : (n : ℂ).im = 0 :=
 by rw [← of_real_int_cast, of_real_im]
 
-@[simp, norm_cast] theorem of_real_rat_cast (n : ℚ) : ((n : ℝ) : ℂ) = n :=
-of_real.map_rat_cast n
+@[simp, norm_cast] theorem of_real_rat_cast (n : ℚ) : ((n : ℝ) : ℂ) = n := map_rat_cast of_real n
 
 @[simp, norm_cast] lemma rat_cast_re (q : ℚ) : (q : ℂ).re = q :=
 by rw [← of_real_rat_cast, of_real_re]

src/data/complex/is_R_or_C.lean

@@ -442,7 +442,7 @@ by rw [← of_real_int_cast, of_real_im]
 
 @[simp, is_R_or_C_simps, norm_cast, priority 900] theorem of_real_rat_cast (n : ℚ) :
   ((n : ℝ) : K) = n :=
-(@is_R_or_C.of_real_hom K _).map_rat_cast n
+map_rat_cast (@is_R_or_C.of_real_hom K _) n
 
 @[simp, is_R_or_C_simps, norm_cast] lemma rat_cast_re (q : ℚ) : re (q : K) = q :=
 by rw [← of_real_rat_cast, of_real_re]

src/data/rat/cast.lean

@@ -24,8 +24,9 @@ casting lemmas showing the well-behavedness of this injection.
 rat, rationals, field, ℚ, numerator, denominator, num, denom, cast, coercion, casting
 -/
 
+variables {F α β : Type*}
+
 namespace rat
-variable {α : Type*}
 open_locale rat
 
 section with_div_ring
@@ -271,10 +272,9 @@ calc f r = f (r.1 / r.2) : by rw [← int.cast_coe_nat, ← mk_eq_div, num_denom
 
 -- This seems to be true for a `[char_p k]` too because `k'` must have the same characteristic
 -- but the proof would be much longer
-lemma ring_hom.map_rat_cast {k k'} [division_ring k] [char_zero k] [division_ring k']
-  (f : k →+* k') (r : ℚ) :
-  f r = r :=
-(f.comp (cast_hom k)).eq_rat_cast r
+@[simp] lemma map_rat_cast [division_ring α] [division_ring β] [char_zero α] [ring_hom_class F α β]
+  (f : F) (q : ℚ) : f q = q :=
+((f : α →+* β).comp $ cast_hom α).eq_rat_cast q
 
 lemma ring_hom.ext_rat {R : Type*} [semiring R] (f g : ℚ →+* R) : f = g :=
 begin
@@ -325,7 +325,7 @@ end monoid_with_zero_hom
 
 namespace mul_opposite
 
-variables {α : Type*} [division_ring α]
+variables [division_ring α]
 
 @[simp, norm_cast] lemma op_rat_cast (r : ℚ) : op (r : α) = (↑r : αᵐᵒᵖ) :=
 by rw [cast_def, div_eq_mul_inv, op_mul, op_inv, op_nat_cast, op_int_cast,

src/ring_theory/algebraic.lean

@@ -101,7 +101,7 @@ by { rw ←ring_hom.map_int_cast (algebra_map R A), exact is_algebraic_algebra_m
 
 lemma is_algebraic_rat (R : Type u) {A : Type v} [division_ring A] [field R] [char_zero R]
   [algebra R A] (n : ℚ) : is_algebraic R (n : A) :=
-by { rw ←ring_hom.map_rat_cast (algebra_map R A), exact is_algebraic_algebra_map n }
+by { rw ←map_rat_cast (algebra_map R A), exact is_algebraic_algebra_map n }
 
 lemma is_algebraic_algebra_map_of_is_algebraic {a : S} :
   is_algebraic R a → is_algebraic R (algebra_map S A a) :=