image of a add_submonoid by a ring_hom

Stream: new members

[Antoine Chambert-Loir]

Apparently, mathlib doesn't know about quotients of graded rings by homogeneous ideals, and @María Inés de Frutos Fernández and I need that…
I am struggling with add_monoid_class : I want to define the image of an add_submonoid by a ring_hom_map, but what works below is strange , because of the apply without which I couldn't make it work…

import ring_theory.graded_algebra.homogeneous_ideal
import ring_theory.ideal.quotient

variables {ι : Type*} [decidable_eq ι] [add_monoid ι]
variables {A : Type*} [comm_ring A]
variables {σ : Type*} [set_like σ A] [add_submonoid_class σ A]

variable (𝒜 : ι → σ)

def graded_quot (I : ideal A) [graded_ring 𝒜] (hI: ideal.is_homogeneous 𝒜 I) : ι → add_submonoid (A ⧸ I) :=
λ i,  add_submonoid.map (ideal.quotient.mk I),
⟨𝒜 i, begin apply add_mem , end, begin apply zero_mem, end,⟩,
end

[Adam Topaz]

It's just a syntax issue:

def graded_quot (I : ideal A) [graded_ring 𝒜] (hI: ideal.is_homogeneous 𝒜 I) : ι → add_submonoid (A ⧸ I) :=
λ i, add_submonoid.map (ideal.quotient.mk I) ⟨𝒜 i, begin apply add_mem , end, begin apply zero_mem, end⟩

[Adam Topaz]

or maybe I misunderstood the issue?

[Adam Topaz]

Oh I think I did misunderstand. Are you looking for some function that takes some term of a type with an add_submonoid_class instance, and returns an actuall add_submonoid? I couldn't find such a thing, but maybe I didn't look hard enough (it it should certainly exist)

[Adam Topaz]

Are we just missing a coercion here?

[Adam Topaz]

or maybe the add_submonoid.map should be generalized? I suppose @Anne Baanen might be a good person to ask?

[Eric Wieser]

I'll take a look at this tomorrow

[Anne Baanen]

Adam Topaz said:

or maybe the add_submonoid.map should be generalized? I suppose Anne Baanen might be a good person to ask?

My intuition says adding a coercion is useful in more cases than generalizing map, but there's no technical objection to doing either. We might have to be careful that coe_sort doesn't get overambitious, i.e. we don't want to end up following a coercion path along the lines of σ → add_submonoid_class →add_submonoid → set_like → Type instead of σ → set_like → Type.

[Eric Wieser]

I don't thing generalizing add_submonoid.map would be very useful

[Eric Wieser]

Because it still has to generate an add_submonoid

[Eric Wieser]

The add_submonoid_class -> add_submonoid coercion is probably ok, but it opens a simpNF can of worms

[Eric Wieser]

Because now we need lemmas translating between a_submodule.to_add_submonoid vs coe a_submodule, coe a_subalgebra.to_submodule vs coe a_subalgebra, etc

[Eric Wieser]

Regarding your original question, it works fine without apply:

def graded_quot (I : ideal A) [graded_ring 𝒜] (hI: ideal.is_homogeneous 𝒜 I) : ι → add_submonoid (A ⧸ I) :=
λ i, add_submonoid.map (ideal.quotient.mk I) ⟨𝒜 i, λ _ _, add_mem, zero_mem _⟩

[Eric Wieser]

You just needed to fix the type errors due to the wrong number of arguments to add_mem

[Antoine Chambert-Loir]

Thank you — and sorry.
What had confused me here, is that library_search suggested exact add_mem, which does not work. My impression was because of the “curly braced” implicit arguments which had to be given again. I see now how to do that. Thanks again.