char_p for quotients by ideals

Stream: new members

[Kevin Buzzard]

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]

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]

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

[Eric Wieser]

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]

Maybe I'll start a new thread for that

[Kevin Buzzard]

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]

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]

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

[Adam Topaz]

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]

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]

But currently docs#ring_hom.char_p_iff_char_p is not so general

[Damiano Testa]

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]

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]

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]

PS there is set.range

[Damiano Testa]

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]

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]

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

[Eric Wieser]

Alex J. Best said:

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

We have this, but proving nontrivial (K_over R) which that lemma needs is just as hard as the original problem

[Alex J. Best]

We didnt have it on January 19th though :smile:

[Eric Wieser]

The full mwe again, this time using the lemma you suggest

import field_theory.mv_polynomial

open mv_polynomial

@[derive [comm_ring, semiring], reducible]
def K_over (R : Type*) [comm_ring R] :=
(ideal.span {x : mv_polynomial (fin 3) R | ∃ (i : fin 3), x = X i * X i}).quotient

instance {R : Type*} [comm_ring R] [nontrivial R] : nontrivial (K_over R) :=
sorry

instance K_over_char_p {R : Type*} {p : ℕ} [field R] [char_p R p] : char_p (K_over R) p :=
begin
  let f : R →+* K_over R :=  (ideal.quotient.mk _).comp _,
  exact (f.char_p_iff_char_p p).mp (by apply_instance),
  convert mv_polynomial.C using 1,  -- very slow without `convert`
end

[Alex J. Best]

Here's a proof of the original help, idk if you already have one?

lemma help (n : ℕ) (hn : ↑n ∈ ideal.span {x : mv_polynomial (fin 3) R | ∃ (i : fin 3), x = X i * X i}) :
  (n : mv_polynomial (fin 3) R) = 0 :=
begin
  have : ∀ x ∈ ideal.span {x : mv_polynomial (fin 3) R | ∃ (i : fin 3), x = X i * X i}, eval 0 x = 0,
  { intros x hx,
    apply submodule.span_induction hx,
    { rintro x ⟨H_w, rfl⟩,
      simp, },
    { simp, },
    { intros x y hx hy, simp [hx, hy], },
    { intros a x hx, simp [hx], }, },
  specialize this _ hn,
  simp at this,
  obtain ⟨p, hp⟩ := char_p.exists R,
  haveI := hp,
  rw char_p.cast_eq_zero_iff _ p,
  rwa char_p.cast_eq_zero_iff _ p at this,
  apply_instance,
  apply_instance,
end

[Alex J. Best]

We hopefully have a lemma saying the quotient by an ideal is nontrivial if the ideal is not top, and this (overkill for that purpose) proof shows the ideal is not top whenever R is non-trivial.

[Eric Wieser]

Yes, that's docs#ideal.quotient.nontrivial

[Alex J. Best]

Ok but your original proof works with the right imports char_p.quotient, so are you just looking for the cleanest way of doing this?

[Eric Wieser]

Well I never managed to reach a proof at all, so your comment above is excellent

[Eric Wieser]

But now I'm after the cleanest way of doing this

[Alex J. Best]

Yeah I guess I also don't see a way of showing 1 is not in the ideal that is easier than showing the only constant in the ideal is 0.

[Alex J. Best]

Like maybe if it was on paper I'd say that the ideal only contains even total degree monomials, so it can't contain everything, but formalizing that definitely seems longer, it would be a slightly more general argument though I guess

[Eric Wieser]

Slightly adjusted proof:

lemma C_mem_iff_zero (r : R)
  (hr : C r ∈ ideal.span {x : mv_polynomial (fin 3) R | ∃ (i : fin 3), x = X i * X i}) :
  (C r : mv_polynomial (fin 3) R) = 0 :=
begin
  rw [←C.map_zero, C_inj, ←constant_coeff_C (r : R)],
  have := ideal.apply_coe_mem_map (constant_coeff : mv_polynomial (fin 3) R →+* R) _ ⟨_, hr⟩,
  rw [ideal.map_span, subtype.coe_mk] at this,
  clear hr,
  revert this,
  generalize : constant_coeff (C r : mv_polynomial (fin 3) R) = x,
  intro hx,
  apply submodule.span_induction hx,
  { rintro x ⟨H_w, ⟨i, rfl⟩, rfl⟩,
    simp, },
  { simp, },
  { intros x y hx hy, simp [hx, hy], },
  { intros a x hx, simp [hx], },
end

lemma nat_cast_mem_iff_zero (n : ℕ)
  (hn : ↑n ∈ ideal.span {x : mv_polynomial (fin 3) R | ∃ (i : fin 3), x = X i * X i}) :
  (n : mv_polynomial (fin 3) R) = 0 :=
begin
  revert hn,
  rw [←C.map_nat_cast],
  exact C_mem_iff_zero _,
end