Represent a ideal generated by an integer

Stream: Is there code for X?

[Ben]

I think I get how to form an generated ideal (mathlib calls them span). I can't seem to lift them to sets in the way I have previously done for general ideals. Any ideas where I am going wrong:

example (I : @ideal.span int _ {2}) : 2 * (I: set int) = @ideal.span int _ {4}  := begin
  sorry
end

[Eric Wieser]

Your statement doesn't make sense; it says "let I be a member of ideal.span ({2} : set int)" (i.e. an integer), then it tries to turn it into a set of integers

[Eric Wieser]

I assume you meant

import ring_theory.ideal.operations

example : 2 * ideal.span ({2} : set int) = ideal.span {4} :=
begin
  rw [two_mul, ideal.add_eq_sup, sup_idem],
  sorry -- looks false to me!
end

[Kevin Buzzard]

Probably ideal.span {2} * ideal.span {2} = ideal.span {4} is true. It wouldn't surprise me if 2 * I is being interpreted as I + I which is of course I again.

[Eric Wieser]

Here's how to enable the instance you need so that you can write something similar to what you wanted:

import ring_theory.ideal.operations
import algebra.module.submodule.pointwise

open_locale pointwise

example : (2 : ℤ) • ideal.span ({2} : set int) = ideal.span {4} :=
begin
  change submodule.map _ _ = _,
  erw submodule.map_span,  -- this line and the one above combined are a missing lemma
  rw set.image_singleton,
  refl,
end

[Eric Wieser]

I made #17814 with some of the missing lemmas

[Ben]

Ah I see because ideal R is a type, ideal is type constructor. Whereas ideal.span generates a specific ideal (not a general one).

[Ben]

The full statement I am trying to prove here is:

example (I := ideal.span ({2}: set int)) (J := ideal.span ({4}: set int)): (I: set int) * J ≠ I ∩ J := sorry

[Eric Wieser]

That's false, because I := I_val does not mean what you think it means

[Eric Wieser]

It means "if the user doesn't specify the ideal I, use I_val", not "I is always equal to I_val"

[Eric Wieser]

You probably meant (I) (hI : I = ideal.span ({2}: set int))

[Ben]

Ah I didn't realise it could specified by a caller/user.
I did try:

def I := ideal.span ({2}: set int)
def J := ideal.span ({4}: set int)
example : (I: set int) * J ≠ I ∩ J := sorry

But it doesn't like (I: set int) :shrug:

[Eric Wieser]

What does the error message say?

[Ben]

invalid type ascription, term has type ideal R but is expected to have type set ℤ. Ah wait was because I already had a variable (I: ideal R) in scope... Lean doesn't seem to mind things with the same name in the scope

[Ben]

Coming back to this, I managed to prove my final statement. However wanted to tidy some stuff up and getting a (deterministic) timeout here. What am I doing wrong?

def I := ideal.span ({2}: set int)
def J := ideal.span ({4}: set int)
example : I * J = ideal.span ({8}: set int) := begin
  rw [I, J],
  exact @ideal.prod_span_singleton int int.comm_semiring int ({2, 4}: finset int) id,
end

[Kevin Buzzard]

Can you post a #mwe ?

[Kevin Buzzard]

One thing you're doing wrong is using @. The whole point of implicit arguments is that lean is supposed to handle them itself, for normal usage you're not expected to need @.

[Junyan Xu]

I think the LHS of @ideal.prod_span_singleton ... reduces to something like 1 * span {2} * span {4}, so it's not defeq to I * J.

[Junyan Xu]

You want docs#ideal.span_singleton_mul_span_singleton

[Junyan Xu]

BTW, no need to rw [I, J].

[Ben]

Junyan Xu said:

You want docs#ideal.span_singleton_mul_span_singleton

Ah this is the one I was looking for, don't know how I missed it :laughing:

[Ben]

Is there a ideal.mul_coe? looking for something that equates pointwise set multiplication being the same as multiplication of ideals

[Michael Stoll]

Pointwise set multiplication of ideals is not in general the same as multiplication of ideals (it is, of course, when the ideals are principal). The product I * J is the ideal generated by the pointwise product (the latter need not be an ideal).

[Ben]

Ah yes, is there a proof of that for principal ideals? I am unfortunately in set land as ideals don't have intersection or equality

[Patrick Massot]

What do you mean by "ideals don't have intersection or equality"??

[Ben]

Okay just realised equality works. But the following fails in Lean with failed to synthesize type class instance for has_inter (ideal R):

example {R: Type} [ring R] (I J: ideal R) : (I ∩ J) = (J ∩ I) := sorry

[Sky Wilshaw]

I think you need ⊓ notation instead of ∩ notation. The ∩ symbol is pretty much just used for sets in mathlib, while ⊓ is used in other (semi)lattices.

[Sky Wilshaw]

Then your example is proved by docs#inf_comm.

[Ben]

Ah yes just found that symbol while looking at the set.has_inter!

[Ben]

Huh theinf refers to infimum, only seen that use to refer to the greatest lower bound of a set, how does that relate to here

[Eric Wieser]

docs#has_inf should explain that

[Eric Wieser]

... but it does not. It stands for infimum

[Sky Wilshaw]

It's the infimum in a lattice. Set intersection is an example of an infimum. The infima of two elements of a linear order is also an example of the infimum, i.e. the usual inf operator.

[Sky Wilshaw]

If you want the greatest lower bound of a set of things in a linear order, for example, consider docs#complete_linear_order.Inf.

[Sky Wilshaw]

For more information, look at docs#lattice and docs#complete_lattice.

[Kevin Buzzard]

If I and J are ideals then I ⊓ J, the largest ideal which is contained in $I$ and $J$, is what a mathematician would call $I\cap J$ and I ⊔ J, the smallest ideal containing $I$ and $J$, is what a mathematician would call $I+J$.