unique ring hom from ℚ

Stream: maths

[Johan Commelin]

Lean is asking me to prove f r = g r where f and g are two ring homs, and r : ℚ. Is this statement in mathlib?

[Johan Commelin]

There is eq_cast, but this gives you a ton of goals instead of just is_ring_hom f. Also, the cast only works for division rings :scream: (which is of course necessary, but doesn't help me)

[Mario Carneiro]

It's not true for arbitrary ring homs, I think. You can freely define the "divide by p" operation in the ring unless you know the ring is a domain or is multiplicatively cancellative

[Keeley Hoek]

But Mario, the image of 1/n must be a multiplicative inverse of n.

[Mario Carneiro]

that element must satisfy n * a = 1 but why is there a unique such element?

[Mario Carneiro]

unless you know n * a = n * a' => a = a'

[Keeley Hoek]

Sure yeah, I just baulked at "freely" without thinking

[Mario Carneiro]

I mean freely relative to that restriction of course

[Keeley Hoek]

I mean, there are even two ring homs Q -> Q, the identity and the zero map.

[Mario Carneiro]

lol

[Keeley Hoek]

Wait are mathlib ring homs identity-preserving

[Mario Carneiro]

yes

[Keeley Hoek]

Ok then scratch that

[Kevin Buzzard]

Inverses are unique

[Mario Carneiro]

why?

[Mario Carneiro]

without cancellation

[Kevin Buzzard]

Are we talking about commutative rings?

[Mario Carneiro]

I guess so

[Kevin Buzzard]

Then inverses are unique

[Mario Carneiro]

why?

[Kevin Buzzard]

If a*b=1 and a*c=1 then b*a*c=b=c

[Kevin Buzzard]

Just like there's a unique map from Z to any ring, there's at most one map from Q to any comm ring

[Mario Carneiro]

I see, so commutativity is essential here

[Kevin Buzzard]

My gut feeling is that we don't need comm ring but I'm supposed to be marking 500 scripts not reading this

[Kevin Buzzard]

So let me humiliate myself by trying to figure this out in real time

[Kevin Buzzard]

Man I am so bad at rings.

[Kevin Buzzard]

by which I mean noncommutative rings

[Kevin Buzzard]

Obviously we need that a ring hom sends 1 to 1 (and I know people who don't even believe this)

[Mario Carneiro]

Is it true for the ring of half-integers?

[Kevin Buzzard]

It's bound to be true

[Kevin Buzzard]

I'd know a weird example if it weren't true

[Kevin Buzzard]

So the question currently is that if Z[1/2] -> R is a ring hom between rings with 1 (R not necc commutative) which sends 1 to 1 then is it the only one?

[Mario Carneiro]

yes

[Kevin Buzzard]

And my money is on yes

[Kevin Buzzard]

21/2=1/22=1

[Kevin Buzzard]

meh

[Kevin Buzzard]

2 x 1/2 and 1/2 x 2 are both 1 in Z[1/2]

[Kevin Buzzard]

so I bet the same argument works

[Kevin Buzzard]

If a and b are two candidates for the image of 1/2 then we can still run the same argument becuase we have associativity and one_mul and mul_one

[Kevin Buzzard]

a*(2*b)=(a*2)*b

[Kevin Buzzard]

and this works in general, so Johan doesn't even need commutative, as long as 1 is going to 1

[Kevin Buzzard]

(which implies 2 is going to 1+1)

[Kevin Buzzard]

(i.e. a unique place)

[Kevin Buzzard]

Students learn in maths departments that in lots of categories "surjective" is the same as "epimorphism" and "injective" is the same as "monomorphism"

[Mario Carneiro]

yeah, that sounds right

[Kevin Buzzard]

and then we pull out the example of the category of rings, where Z -> Q is both monic and epic

[Kevin Buzzard]

so I think I was probably proving that.

[Kevin Buzzard]

whilst worrying about whether we should have been pulling out the category of commutative rings instead.

[Kevin Buzzard]

OK see you in 2 weeks

[Kevin Buzzard]

when I've finished this marking

[Kevin Buzzard]

[yeah right]

[Kevin Buzzard]

I guess the correct statement is that in a general not-necc-commutative ring, two-sided inverses are unique. There are rings where a*b=1 but b*a isn't.

[Kevin Buzzard]

so it should be called coe_inj for units R -> R or something

[Kevin Buzzard]

crap I have over 500 scripts still to mark. I really must go away.

[Johan Commelin]

@Kevin Buzzard GO AWAY!!!

[Kevin Buzzard]

It's lunchtime now ;-)

[Mario Carneiro]

import data.rat algebra.char_zero

theorem nat.semiring_hom_eq_cast {α} [ring α]
  (f : ℕ → α) [is_semiring_hom f] (n : ℕ) : f n = n :=
nat.eq_cast' _ (is_semiring_hom.map_one _) (λ _ _, is_semiring_hom.map_add f) _

theorem int.ring_hom_eq_cast {α} [ring α]
  (f : ℤ → α) [is_ring_hom f] (n : ℤ) : f n = n :=
int.eq_cast _ (is_ring_hom.map_one _) (λ _ _, is_ring_hom.map_add f) _

theorem rat.ring_hom_unique {α} [ring α]
  (f g : ℚ → α) [is_ring_hom f] [is_ring_hom g] (r : ℚ) : f r = g r :=
rat.num_denom_cases_on' r $ λ a b b0, begin
  rw [rat.mk_eq_div, int.cast_coe_nat],
  have b0' : (b:ℚ) ≠ 0 := nat.cast_ne_zero.2 b0,
  have : ∀ n : ℤ, f n = g n := λ n,
    (int.ring_hom_eq_cast (f ∘ int.cast) n).trans
    (int.ring_hom_eq_cast (g ∘ int.cast) n).symm,
  calc f (a * b⁻¹)
      = f a * f b⁻¹ * (g (b:ℤ) * g b⁻¹) : by rw [
    int.cast_coe_nat, ← is_ring_hom.map_mul g,
    mul_inv_cancel b0', is_ring_hom.map_one g, mul_one,
    is_ring_hom.map_mul f]
  ... = g a * f b⁻¹ * (f (b:ℤ) * g b⁻¹) : by rw [this a, ← this b]
  ... = g (a * b⁻¹) : by rw [
    int.cast_coe_nat, mul_assoc, ← mul_assoc (f b⁻¹),
    ← is_ring_hom.map_mul f, inv_mul_cancel b0',
    is_ring_hom.map_one f, one_mul,
    is_ring_hom.map_mul g]
end

[Johan Commelin]

@Mario Carneiro Merci beaucoup!

[Mario Carneiro]

de rien

[Johan Commelin]

Now we know for sure that ring homs from ℚ are unique :sweat_smile:

[Chris Hughes]

If they're two sided inverses then you obviously don't need commutativity.

[Chris Hughes]

Unless I'm being stupid.

[Chris Hughes]

The image of a ring hom from a commutative ring is a commutative ring.

[Mario Carneiro]

this is the important bit, I think; the fact that f n is always in the center of the ring

[Kevin Buzzard]

The image of a ring hom from a commutative ring is a commutative ring.

Yes but the problem with this argument is that the two images might be different commutative subrings.

[Kevin Buzzard]

this is the important bit, I think; the fact that f n is always in the center of the ring

Is that obvious? I don't see how we have access to facts about stuff not in the image.

[Kevin Buzzard]

It might well be true but I don't see it immediately.

[Kevin Buzzard]

and lunch is nearly over :-/

[Kevin Buzzard]

I have no feeling for how bad noncommutative rings can be.

[Kevin Buzzard]

Is there some crazy non-commutative polynomial ring Q[z] where lambda z isn't z lambda for lambda in Q?

[Mario Carneiro]

Oops, I mean that f n and f m commute

[Mario Carneiro]

there's a theorem about that in nat.cast

[Kevin Buzzard]

For commutative rings I have a really powerful feeling about how to build them -- throwing in generators and relations -- but for non-commutative rings I don't know what one can get away with.

[Kevin Buzzard]

I think non-commutative rings are as broken as semigroups -- not enough axioms!

[Jesse Michael Han]

this follows from the universal property of the fraction field and the uniqueness of maps from Z, right?

[Kevin Buzzard]

For commutative rings, sure.

[Johan Commelin]

@Mario Carneiro Do you want to PR you lemma? Or shall I do it? What would be a good file to put it in?