## Stream: new members

### Topic: char_p for quotients by ideals

#### 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.

#### 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.

#### 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.

#### 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.

#### Eric Wieser (Jan 19 2021 at 14:48):

Maybe I'll start a new thread for that

#### Kevin Buzzard (Jan 19 2021 at 14:49):

You're trying to prove that the map from $K$ to $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]/(a^2,b^2,c^2)\to K$ sending $a,b,c$ to zero.

#### 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?

#### 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!

#### Adam Topaz (Jan 19 2021 at 15:58):

Does mathlib have the lemma saying that when $A$ is a ring of characteristic $n$ and $A \to B$ is a morphism then the characteristic of $B$ divides $n$?

#### 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 := ...


#### Alex J. Best (Jan 19 2021 at 18:00):

But currently docs#ring_hom.char_p_iff_char_p is not so general

#### 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.

#### 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 :=


#### 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.

#### Kevin Buzzard (Jan 20 2021 at 08:23):

PS there is set.range

#### 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"..

#### 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?

#### 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