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: Dec 20 2023 at 11:08 UTC