# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: Ideals of an algebra are submodules

#### Kevin Buzzard (May 14 2020 at 11:16):

```
import ring_theory.noetherian -- or whatever
variables (R : Type) [comm_ring R]
example (S : Type) [comm_ring S] [algebra R S] (I : ideal S) : submodule R S :=
sorry
```

I've tried `library_search`

, `suggest`

and `hint`

. Is this function supposed to have a name or be in some system?

#### Kenny Lau (May 14 2020 at 13:01):

@Kevin Buzzard have you tried looking into the actual proof?

#### Kenny Lau (May 14 2020 at 13:04):

aha I did it explicitly:

https://github.com/leanprover-community/mathlib/blob/master/src/ring_theory/polynomial.lean#L138

```
/-- Transport an ideal of `R[X]` to an `R`-submodule of `R[X]`. -/
def of_polynomial (I : ideal (polynomial R)) : submodule R (polynomial R) :=
{ carrier := I.carrier,
zero := I.zero_mem,
add := λ _ _, I.add_mem,
smul := λ c x H, by rw [← C_mul']; exact submodule.smul_mem _ _ H }
```

#### Kevin Buzzard (May 14 2020 at 13:16):

```
import ring_theory.noetherian
import data.polynomial
import tactic
import ring_theory.algebra_operations
noncomputable theory
variables (R : Type) [comm_ring R] (hR : is_noetherian_ring R)
def ideal.to_submodule (S : Type) [comm_ring S] [algebra R S] (I : ideal S) :
submodule R S :=
{ carrier := I,
zero := I.zero_mem,
add := λ x y, I.add_mem,
smul := sorry}
```

I was surprised `smul`

was hard

#### Kevin Buzzard (May 14 2020 at 13:17):

I still can't do it and your proof doesn't cover this case

#### Reid Barton (May 14 2020 at 13:18):

I don't really know how the library is set up but isn't a sub-S-module also a sub-R-module?

#### Kevin Buzzard (May 14 2020 at 13:19):

Mathematically, sure.

#### Kevin Buzzard (May 14 2020 at 13:20):

but we're talking about submodules of `S`

, right? Is `submodule S S`

preferred to `ideal S`

?

#### Reid Barton (May 14 2020 at 13:21):

I'm just trying to remove irrelevant distractions like `ideal`

. But now I am not entirely sure it is irrelevant. How does one turn an S-module into an R-module?

#### Kevin Buzzard (May 14 2020 at 13:21):

there's a canonical map R -> S from `[algebra R S]`

#### Kevin Buzzard (May 14 2020 at 13:22):

and I want to pull back along that canonical map, and because that map is canonical, an S-module or S-submodule is an R-module or R-submodule canonically

#### Kevin Buzzard (May 14 2020 at 13:22):

My instinct is that automation should be making that map for me

#### Kevin Buzzard (May 14 2020 at 13:23):

because registering the instance `[algebra R S]`

means that now there is a canonical map which should be somehow inserted into a system?

#### Reid Barton (May 14 2020 at 13:23):

Is there not something like `comap`

for modules? Or am I just looking in the wrong place?

#### Johan Commelin (May 14 2020 at 14:31):

There's `map`

and `comap`

for submodules (and for ideals, which is slightly different). You need to feed it a ring hom.

#### Johan Commelin (May 14 2020 at 14:33):

But I don't think it has been hooked up to the `algebra`

API

Last updated: May 17 2021 at 15:13 UTC