# Zulip Chat Archive

## Stream: maths

### Topic: unique ring hom from ℚ

#### Johan Commelin (May 14 2019 at 09:41):

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 (May 14 2019 at 09:42):

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 (May 14 2019 at 10:15):

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 (May 14 2019 at 10:16):

But Mario, the image of `1/n`

must be a multiplicative inverse of `n`

.

#### Mario Carneiro (May 14 2019 at 10:17):

that element must satisfy `n * a = 1`

but why is there a unique such element?

#### Mario Carneiro (May 14 2019 at 10:18):

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

#### Keeley Hoek (May 14 2019 at 10:19):

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

#### Mario Carneiro (May 14 2019 at 10:19):

I mean freely relative to that restriction of course

#### Keeley Hoek (May 14 2019 at 10:19):

I mean, there are even two ring homs `Q -> Q`

, the identity and the zero map.

#### Mario Carneiro (May 14 2019 at 10:19):

lol

#### Keeley Hoek (May 14 2019 at 10:19):

Wait are mathlib ring homs identity-preserving

#### Mario Carneiro (May 14 2019 at 10:20):

yes

#### Keeley Hoek (May 14 2019 at 10:20):

Ok then scratch that

#### Kevin Buzzard (May 14 2019 at 10:20):

Inverses are unique

#### Mario Carneiro (May 14 2019 at 10:20):

why?

#### Mario Carneiro (May 14 2019 at 10:20):

without cancellation

#### Kevin Buzzard (May 14 2019 at 10:21):

Are we talking about commutative rings?

#### Mario Carneiro (May 14 2019 at 10:21):

I guess so

#### Kevin Buzzard (May 14 2019 at 10:21):

Then inverses are unique

#### Mario Carneiro (May 14 2019 at 10:21):

why?

#### Kevin Buzzard (May 14 2019 at 10:21):

If `a*b=1`

and `a*c=1`

then `b*a*c=b=c`

#### Kevin Buzzard (May 14 2019 at 10:22):

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 (May 14 2019 at 10:22):

I see, so commutativity is essential here

#### Kevin Buzzard (May 14 2019 at 10:22):

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 (May 14 2019 at 10:23):

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

#### Kevin Buzzard (May 14 2019 at 10:23):

Man I am so bad at rings.

#### Kevin Buzzard (May 14 2019 at 10:23):

by which I mean noncommutative rings

#### Kevin Buzzard (May 14 2019 at 10:24):

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

#### Mario Carneiro (May 14 2019 at 10:24):

Is it true for the ring of half-integers?

#### Kevin Buzzard (May 14 2019 at 10:25):

It's bound to be true

#### Kevin Buzzard (May 14 2019 at 10:25):

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

#### Kevin Buzzard (May 14 2019 at 10:26):

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 (May 14 2019 at 10:26):

yes

#### Kevin Buzzard (May 14 2019 at 10:26):

And my money is on yes

#### Kevin Buzzard (May 14 2019 at 10:26):

2*1/2=1/2*2=1

#### Kevin Buzzard (May 14 2019 at 10:26):

meh

#### Kevin Buzzard (May 14 2019 at 10:27):

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

#### Kevin Buzzard (May 14 2019 at 10:27):

so I bet the same argument works

#### Kevin Buzzard (May 14 2019 at 10:27):

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 (May 14 2019 at 10:28):

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

#### Kevin Buzzard (May 14 2019 at 10:28):

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

#### Kevin Buzzard (May 14 2019 at 10:28):

(which implies 2 is going to 1+1)

#### Kevin Buzzard (May 14 2019 at 10:28):

(i.e. a unique place)

#### Kevin Buzzard (May 14 2019 at 10:29):

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 (May 14 2019 at 10:29):

yeah, that sounds right

#### Kevin Buzzard (May 14 2019 at 10:30):

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

#### Kevin Buzzard (May 14 2019 at 10:30):

so I think I was probably proving that.

#### Kevin Buzzard (May 14 2019 at 10:30):

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

#### Kevin Buzzard (May 14 2019 at 10:32):

OK see you in 2 weeks

#### Kevin Buzzard (May 14 2019 at 10:32):

when I've finished this marking

#### Kevin Buzzard (May 14 2019 at 10:32):

[yeah right]

#### Kevin Buzzard (May 14 2019 at 10:48):

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 (May 14 2019 at 10:48):

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

#### Kevin Buzzard (May 14 2019 at 10:49):

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

#### Johan Commelin (May 14 2019 at 10:49):

@Kevin Buzzard GO AWAY!!!

#### Kevin Buzzard (May 14 2019 at 10:59):

It's lunchtime now ;-)

#### Mario Carneiro (May 14 2019 at 11:07):

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 (May 14 2019 at 11:09):

@Mario Carneiro Merci beaucoup!

#### Mario Carneiro (May 14 2019 at 11:09):

de rien

#### Johan Commelin (May 14 2019 at 11:10):

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

#### Chris Hughes (May 14 2019 at 11:13):

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

#### Chris Hughes (May 14 2019 at 11:14):

Unless I'm being stupid.

#### Chris Hughes (May 14 2019 at 11:15):

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

#### Mario Carneiro (May 14 2019 at 11:16):

this is the important bit, I think; the fact that `f n`

is always in the center of the ring

#### Kevin Buzzard (May 14 2019 at 11:17):

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 (May 14 2019 at 11:19):

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 (May 14 2019 at 11:20):

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

#### Kevin Buzzard (May 14 2019 at 11:20):

and lunch is nearly over :-/

#### Kevin Buzzard (May 14 2019 at 11:20):

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

#### Kevin Buzzard (May 14 2019 at 11:22):

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

#### Mario Carneiro (May 14 2019 at 11:22):

Oops, I mean that `f n`

and `f m`

commute

#### Mario Carneiro (May 14 2019 at 11:23):

there's a theorem about that in `nat.cast`

#### Kevin Buzzard (May 14 2019 at 11:23):

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 (May 14 2019 at 11:24):

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

#### Jesse Michael Han (May 14 2019 at 13:43):

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

#### Kevin Buzzard (May 14 2019 at 14:50):

For commutative rings, sure.

#### Johan Commelin (May 15 2019 at 17:24):

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

Last updated: May 12 2021 at 07:17 UTC