ideal.span_image

Stream: Is there code for X?

[Eric Wieser]

Do we have this anywhere? We have docs#submodule.span_image, but I couldn't work out how to use it here:

lemma ideal.span_image {R A} [semiring R] [semiring A] (f : R →+* A)
  (s : set R) :
  ideal.span (f '' s) = (ideal.span s).map f :=
begin
  apply le_antisymm,
  { apply submodule.span_le.2 _,
    rw ideal.map,
    refine set.subset.trans _ submodule.subset_span,
    rintros x ⟨r, hr, rfl⟩,
    refine ⟨r,  ideal.subset_span hr, rfl⟩, },
  {apply ideal.map_le_of_le_comap _,
    apply submodule.span_le.2 _,
    rw ideal.comap,
    dsimp,
    rw ←set.image_subset_iff,
    apply ideal.subset_span, }
end

[Johan Commelin]

rg -A3 "lemma.*map_span"

[Johan Commelin]

Something exists. But I don't know which namespace

[Johan Commelin]

docs#map_span

[Johan Commelin]

Looks like docs#ideal.map_span is your friend

[Eric Wieser]

Annoying that the naming convention is the reverse of the submodule one

[Eric Wieser]

Thanks!

[Johan Commelin]

For submodule both seem to exist

[Eric Wieser]

src#submodule.map_span, src#submodule.span_image

[Eric Wieser]

Naturally both are proved from scratch...

[Johan Commelin]

I fear that a library_search-linter will be very expansive.

[Eric Wieser]

Dedup'd in #10219