mathlib

mathlib copied to clipboard

Proves that there are no nontrivial ring homomorphism from ℝ to ℝ.

This is motivated by a remark of K. Buzzard (see https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Continuous.20complex.20ring.20hom/near/293264751).

It looks like it should be a direct consequence of the results of algebra/order/complete.field but I was not able to see how to do it more directly.

---

This PR really makes me wonder if the rest of the file can be simplified a bit! But that's a question for another PR I guess

Is this generalization useful? Are there archimedean linearly-ordered fields that are not isomorphic to the reals?

instance real.ring_hom_subsingleton {R : Type*} [linear_ordered_field R] [archimedean R] :
  subsingleton (ℝ →+* R) :=
⟨λ f g, begin
  have fmon := real.ring_hom_monotone f,
  have gmon := real.ring_hom_monotone g,
  haveI : subsingleton (ℝ →+*o R) := order_ring_hom.subsingleton,
  exact congr_arg order_ring_hom.to_ring_hom (subsingleton.elim ⟨f, fmon⟩ ⟨g, gmon⟩),
end⟩

/-- There are no nontrivial ring homorphism `ℝ → ℝ`. -/
instance real.ring_hom_unique {R : Type*} [linear_ordered_field R] : unique (ℝ →+* ℝ) :=
unique_of_subsingleton default

Yes, the rationals are a Archimedean field that is linearly ordered but is not the reals

So that would give a way to prove that there's at most one ring hom from ℝ to ℚ. But I would rather just have a proof that no such ring hom exists.

Perhaps I should have asked whether there are any archimedean linearly-ordered fields that strictly embed the reals?

After a quick search online, it would appear that the answer is no

Here is a new version with a lemma:

variables {R S : Type*} [linear_ordered_field R] [linear_ordered_field S]
lemma ring_hom_monotone (hR : ∀ r : R, 0 ≤ r → ∃ s : R, s^2 = r) (f : R →+* S) : monotone f

and then we deduce the proof that unique (ℝ →+* ℝ)

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests