ideal generator element of ideal

Stream: Is there code for X?

[Michael Stoll]

library_search fails on the following.

import tactic
import ring_theory.ideal.basic

namespace test

variables {R : Type*} [comm_ring R]

lemma ideal.mem_of_mem_generators (s : set R) (a : R) (ha : a ∈ s) : a ∈ ideal.span s :=
begin
  library_search,
end

(and library_search! times out, as does suggest).
This looks like an obvious API lemma that should be in mathlib somewhere...

[Yaël Dillies]

docs#ideal.subset_span

[Johan Commelin]

But why does library_search not find it?

[Yaël Dillies]

I assume it's because it does not unfold ⊆ (whose meaning currently depends on the type it is applied to).

[Michael Stoll]

Yaël Dillies said:

docs#ideal.subset_span

Thanks!
I'm wondering why this lemma has only implicit arguments; I seemingly cannot use it without @.

[Johan Commelin]

ideal.subset_span ha should work

[Adam Topaz]

Or apply ideal.subset_span

[Johan Commelin]

If you have h : s ⊆ t and hx : x ∈ s then h hx : x ∈ t.

[Michael Stoll]

I still find it hard to know when something that does not look like it is really secretly an implication (or similar, e.g., is_coprime).

[Johan Commelin]

True. It is arguably hacky design. You need to know the underlying definition.

[Johan Commelin]

But it also leads to highly-compressable code

[Adam Topaz]

If you think of it in the usual mathy way of saying "now apply the fact that the set s is a subset of the ideal generated by s", it feels very natural to say apply ideal.subset_span which will reduce your goal to ha (as Johan was saying above).

[Adam Topaz]

The usual mathlib style is to golf things to make them completely unreadable, but IMO there is some value in leaving some steps in the proof that mimic what one might write down on paperr.

[Adam Topaz]

(Well, for trivial things like this, you can make the proof as incomprehensible as you want)

[Michael Stoll]

My goal right now is to find a simpler proof of the second lemma below.

lemma ideal.mem_of_linear_comb_of_two (I : ideal R) (a b x y : R) (ha : a ∈ I) (hb : b ∈ I) :
  x*a + y*b ∈ I :=
ideal.add_mem I (ideal.mul_mem_left I x ha) (ideal.mul_mem_left I y hb)

lemma ideal.top_of_coprime (a b : R) (hcop : is_coprime a b) : ideal.span ({a, b} : set R) = ⊤ :=
begin
  set I := ideal.span ({a, b} : set R), -- simplify notation
  rcases hcop with ⟨u, v, rel⟩,
  have h : (1 : R) ∈ I :=
  by { rw ← rel,
       exact ideal.mem_of_linear_comb_of_two I a b u v
               (ideal.subset_span (by simp : a ∈ {a, b}))
               (ideal.subset_span (by simp : b ∈ {a, b})), },
  exact (ideal.eq_top_iff_one I).mpr h,
end

Or is this good enough?

[Adam Topaz]

How is is_coprime defined?

[Adam Topaz]

docs#is_coprime

[Michael Stoll]

Exactly.

[Adam Topaz]

I'm not sure if the first lemma is really needed.

[Michael Stoll]

One could insert its proof, but that would probably make the second proof longer.

[Michael Stoll]

But I'll try anyway.

[Adam Topaz]

Here is the proof I came up with

lemma ideal.top_of_coprime (a b : R) (hcop : is_coprime a b) : ideal.span ({a, b} : set R) = ⊤ :=
begin
  rw ideal.eq_top_iff_one,
  obtain ⟨u,v,h⟩ := hcop, rw ← h,
  apply ideal.add_mem _ _ _,
  all_goals { apply ideal.mul_mem_left _ _ _, apply ideal.subset_span, simp }
end

[Michael Stoll]

OK; re-ordering some of the steps makes it a little bit shorter -- thanks!

[Michael Stoll]

Perhaps this is more useful:

lemma ideal.top_of_coprime' (I : ideal R) (a b : R) (ha : a ∈ I) (hb : b ∈ I) (hcop : is_coprime a b) :
  I = ⊤ :=
begin
  rw ideal.eq_top_iff_one,
  obtain ⟨ u, v, h ⟩ := hcop, rw ← h,
  apply ideal.add_mem _ _ _,
  all_goals { apply ideal.mul_mem_left _ _ _, assumption },
end

[Eric Rodriguez]

There may be a linear_comp lemma as well, those are nice

[Michael Stoll]

docs#ideal.mem_span_pair could probably be used to simplify this...

[Michael Stoll]

lemma ideal.top_of_coprime (a b : R) (hcop : is_coprime a b) : ideal.span ({a, b} : set R) = ⊤ :=
begin
  rw ideal.eq_top_iff_one,
  obtain ⟨ u, v, h ⟩ := hcop, rw ← h,
  rw ideal.mem_span_pair,
  use [u, v],
end