Zulip Chat Archive

Stream: new members

Topic: char_p for quotients by ideals


view this post on Zulip Kevin Buzzard (Jan 19 2021 at 14:44):

You were trying to prove alpha.beta.gamma was not zero in this ring, and now you're trying to prove that 1 is not zero. But this is easier -- you can write a ring homomorphism from the ring to Z/2Z and it sends 1 to 1.

view this post on Zulip Damiano Testa (Jan 19 2021 at 14:45):

In fact, the ideal is homogeneous, so you can simply quotient by all elements of positive degree to obtain a surjective map to the ground ring.

view this post on Zulip Kevin Buzzard (Jan 19 2021 at 14:46):

I guess it was already remarked earlier that things would be a lot easier if we had a theory of homogeneous ideals.

view this post on Zulip Eric Wieser (Jan 19 2021 at 14:48):

For the case of this thread, I only care aboutαβγ = 0 and zmod 2. I was hoping to come up with an example of how to actually apply the lemma I propose in #5809, hence my latest message - and in that case, it would be nice to know how to prove that statement for an arbitrary base ring.

view this post on Zulip Eric Wieser (Jan 19 2021 at 14:48):

Maybe I'll start a new thread for that

view this post on Zulip Kevin Buzzard (Jan 19 2021 at 14:49):

You're trying to prove that the map from KK to K[a,b,c]/(a2,b2,c2)K[a,b,c]/(a^2,b^2,c^2) is injective. I'm suggesting that you can do this by noting that there's one-sided inverse K[a,b,c]/(a2,b2,c2)KK[a,b,c]/(a^2,b^2,c^2)\to K sending a,b,ca,b,c to zero.

view this post on Zulip Eric Wieser (Jan 19 2021 at 14:52):

You're trying to prove ...

Assuming I haven't confused things by moving this thread, how do I convince lean that that's the same statement as my statement above?

view this post on Zulip Eric Wieser (Jan 19 2021 at 15:02):

I've updated the top post with a full #mwe, apologies for posting before I'd stated my problem clearly!

view this post on Zulip Adam Topaz (Jan 19 2021 at 15:58):

Does mathlib have the lemma saying that when AA is a ring of characteristic nn and ABA \to B is a morphism then the characteristic of BB divides nn?

view this post on Zulip Alex J. Best (Jan 19 2021 at 18:00):

Mathlib should have

lemma ring_hom.char_p_iff_char_p {K L : Type*} [division_ring K]
[nontrivial L] [semiring L] (f : K →+* L) (p : ) : char_p K p  char_p L p := ...

view this post on Zulip Alex J. Best (Jan 19 2021 at 18:00):

But currently docs#ring_hom.char_p_iff_char_p is not so general

view this post on Zulip Damiano Testa (Jan 19 2021 at 19:08):

It may not be difficult to show the following result:
If all the generators of an ideal evaluate to zero at the same point, then all the elements of the (submodule/ideal) span of them also evaluate to zero at that point.

This shows that your constant must be zero in the ground ring.

view this post on Zulip Damiano Testa (Jan 20 2021 at 08:12):

I have not found a lemma stating what is below (or something sufficiently close to it). Does it exist?

lemma submodule.mem_span_as_sum {R σ : Type*} [comm_semiring R] {f : R} {s : σ   R}
  (hf : f  submodule.span R (set.image s set.univ)) :
   F : σ →₀ R, f =  i in F.support, s i * F i :=

view this post on Zulip Kevin Buzzard (Jan 20 2021 at 08:22):

Are you sure you need it? Sometimes this is what "the proof in the books" says but you can get around it by just using an appropriate induction principle.

view this post on Zulip Kevin Buzzard (Jan 20 2021 at 08:23):

PS there is set.range

view this post on Zulip Damiano Testa (Jan 20 2021 at 08:30):

I am trying to prove that if all the polynomials in a set evaluate to zero at some point, then all the polynomials in the ideal generated by that set also evaluate to zero at that point. My strategy was by "the proof in the books"..

view this post on Zulip Kevin Buzzard (Jan 20 2021 at 10:49):

Why not just prove that the collection of polynomials vanishing at a point is an ideal, so if it contains the set then it contains the ideal generated by the set?

view this post on Zulip Damiano Testa (Jan 20 2021 at 11:59):

I like this suggestion! As always, I should stop thinking in terms of elements...


Last updated: May 10 2021 at 00:31 UTC