ideal.nat_cast

Stream: Is there code for X?

[María Inés de Frutos Fernández]

Do we have the following lemma?

import ring_theory.ideal.operations

lemma ideal.nat_cast (R : Type*) [comm_ring R] (n : ℕ) :
  (n : ideal R) = ideal.span ({n} : set R) :=
sorry

[Yaël Dillies]

Is that true? If it were true, span {2} = 2 = 1 + 1 = span {1} + span {1} = univ + univ = univ

[Kevin Buzzard]

n : ideal R looks to me like an unfortunate consequence of the "if it has a + and a 0 and a 1, then it has an n for all n" rule (which is gone in Lean 4 if I understand correctly).

[Riccardo Brasca]

This indeed looks false. Addition on ideal R comes from docs#submodule.pointwise_add_comm_monoid, so it is the ideal generated by the two ideals, and 1 is the full ring. In particular 1+1+1+... = 1. The notation n : ideal R is mathematically irrelevant.

[María Inés de Frutos Fernández]

OK, I see. The (n : ideal R) appeared after applying simp to an hypothesis of the form n • I = 0, for I an ideal, but it seems that this is not the correct way to express this in Lean. Thanks!

[Riccardo Brasca]

Can you squeeze the simp and see which lemma is applied?

[María Inés de Frutos Fernández]

Yes, it applied nsmul_eq_mul.

[Riccardo Brasca]

n • I = I, right?

[Yaël Dillies]

docs#nsmul_eq_mul by any chance?

[Riccardo Brasca]

So I guess what is missing is a simp lemma saying ↑n * I = I

[Riccardo Brasca]

Wait

[Alex J. Best]

Kevin Buzzard said:

n : ideal R looks to me like an unfortunate consequence of the "if it has a + and a 0 and a 1, then it has an n for all n" rule (which is gone in Lean 4 if I understand correctly).

If we keep the semifield instance on fractional_ideal then I'd imagine we will always have a way of writing numerals and getting fractional ideals at least

[Alex J. Best]

Riccardo Brasca said:

Wait

unless n is 0?

[Riccardo Brasca]

Yes, that's annoying

[Riccardo Brasca]

@María Inés de Frutos Fernández it seems that cases n; simp is already able to do everything

[Riccardo Brasca]

It treats the cases as expected

[María Inés de Frutos Fernández]

Thanks!

[Kevin Buzzard]

Patrick gives this example (ideals) as the reason we need to have nonsense like semirings instead of just working with rings ;-) Great to see it working so well! ;-)

[Yaël Dillies]

I didn't know you hated nat so much, Kevin!

[Kevin Buzzard]

long live int!

[Kevin Buzzard]

We have a lot of lemmas proved for rings and then special cases nat.same_lemma and nnreal.same_lemma . If we dropped semirings we'd just have more of these.

[Riccardo Brasca]

It would be nice if simp could do the cases n part by itself, but this is maybe impossible.