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):

21/2=1/22=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: Dec 20 2023 at 11:08 UTC