Zulip Chat Archive

Stream: maths

Topic: unique ring hom from ℚ


view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Keeley Hoek (May 14 2019 at 10:16):

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

view this post on Zulip Mario Carneiro (May 14 2019 at 10:17):

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

view this post on Zulip Mario Carneiro (May 14 2019 at 10:18):

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

view this post on Zulip Keeley Hoek (May 14 2019 at 10:19):

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

view this post on Zulip Mario Carneiro (May 14 2019 at 10:19):

I mean freely relative to that restriction of course

view this post on Zulip Keeley Hoek (May 14 2019 at 10:19):

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

view this post on Zulip Mario Carneiro (May 14 2019 at 10:19):

lol

view this post on Zulip Keeley Hoek (May 14 2019 at 10:19):

Wait are mathlib ring homs identity-preserving

view this post on Zulip Mario Carneiro (May 14 2019 at 10:20):

yes

view this post on Zulip Keeley Hoek (May 14 2019 at 10:20):

Ok then scratch that

view this post on Zulip Kevin Buzzard (May 14 2019 at 10:20):

Inverses are unique

view this post on Zulip Mario Carneiro (May 14 2019 at 10:20):

why?

view this post on Zulip Mario Carneiro (May 14 2019 at 10:20):

without cancellation

view this post on Zulip Kevin Buzzard (May 14 2019 at 10:21):

Are we talking about commutative rings?

view this post on Zulip Mario Carneiro (May 14 2019 at 10:21):

I guess so

view this post on Zulip Kevin Buzzard (May 14 2019 at 10:21):

Then inverses are unique

view this post on Zulip Mario Carneiro (May 14 2019 at 10:21):

why?

view this post on Zulip Kevin Buzzard (May 14 2019 at 10:21):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 14 2019 at 10:22):

I see, so commutativity is essential here

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 14 2019 at 10:23):

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

view this post on Zulip Kevin Buzzard (May 14 2019 at 10:23):

Man I am so bad at rings.

view this post on Zulip Kevin Buzzard (May 14 2019 at 10:23):

by which I mean noncommutative rings

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (May 14 2019 at 10:24):

Is it true for the ring of half-integers?

view this post on Zulip Kevin Buzzard (May 14 2019 at 10:25):

It's bound to be true

view this post on Zulip Kevin Buzzard (May 14 2019 at 10:25):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (May 14 2019 at 10:26):

yes

view this post on Zulip Kevin Buzzard (May 14 2019 at 10:26):

And my money is on yes

view this post on Zulip Kevin Buzzard (May 14 2019 at 10:26):

21/2=1/22=1

view this post on Zulip Kevin Buzzard (May 14 2019 at 10:26):

meh

view this post on Zulip Kevin Buzzard (May 14 2019 at 10:27):

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

view this post on Zulip Kevin Buzzard (May 14 2019 at 10:27):

so I bet the same argument works

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 14 2019 at 10:28):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 14 2019 at 10:28):

(which implies 2 is going to 1+1)

view this post on Zulip Kevin Buzzard (May 14 2019 at 10:28):

(i.e. a unique place)

view this post on Zulip 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"

view this post on Zulip Mario Carneiro (May 14 2019 at 10:29):

yeah, that sounds right

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 14 2019 at 10:30):

so I think I was probably proving that.

view this post on Zulip Kevin Buzzard (May 14 2019 at 10:30):

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

view this post on Zulip Kevin Buzzard (May 14 2019 at 10:32):

OK see you in 2 weeks

view this post on Zulip Kevin Buzzard (May 14 2019 at 10:32):

when I've finished this marking

view this post on Zulip Kevin Buzzard (May 14 2019 at 10:32):

[yeah right]

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 14 2019 at 10:48):

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

view this post on Zulip Kevin Buzzard (May 14 2019 at 10:49):

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

view this post on Zulip Johan Commelin (May 14 2019 at 10:49):

@Kevin Buzzard GO AWAY!!!

view this post on Zulip Kevin Buzzard (May 14 2019 at 10:59):

It's lunchtime now ;-)

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 14 2019 at 11:09):

@Mario Carneiro Merci beaucoup!

view this post on Zulip Mario Carneiro (May 14 2019 at 11:09):

de rien

view this post on Zulip Johan Commelin (May 14 2019 at 11:10):

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

view this post on Zulip Chris Hughes (May 14 2019 at 11:13):

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

view this post on Zulip Chris Hughes (May 14 2019 at 11:14):

Unless I'm being stupid.

view this post on Zulip Chris Hughes (May 14 2019 at 11:15):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 14 2019 at 11:20):

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

view this post on Zulip Kevin Buzzard (May 14 2019 at 11:20):

and lunch is nearly over :-/

view this post on Zulip Kevin Buzzard (May 14 2019 at 11:20):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (May 14 2019 at 11:22):

Oops, I mean that f n and f m commute

view this post on Zulip Mario Carneiro (May 14 2019 at 11:23):

there's a theorem about that in nat.cast

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 14 2019 at 11:24):

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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (May 14 2019 at 14:50):

For commutative rings, sure.

view this post on Zulip 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