CODEWITHSUNDEEP
lean
Snow bunting
Snow bunting

Reputation: 1231

Lean: define product of R-ideal and R-module

I am trying to learn Lean and I am trying to figure out how one would create a new R-module I*M = {i*m | i in I, m in M} from an ideal I and an R-module M.

So my attempt was to define first a map ideal_mult that would create a new R-module and then figure out how to assign a nice notation for it.

import ring_theory.ideals
import algebra.module

universes u v
variables {R : Type u} {M : Type v}
variables [comm_ring R] [add_comm_group M] [module R M]
variables (I: ideal R)

def ideal_mult (I: ideal R) (M: Type v)
        [add_comm_group M] [module R M]: Type v
        :=
    sorry

#check ideal_mult I M

How could I define this, so that I could for example state a hypothesis like (h: I*M = M)?

Thank you for the help!

Upvotes: 2

Views: 174

Answers (1)

jmc
jmc

Reputation: 366

You should import ring_theory.ideal_operations. It has the definition that you want at https://github.com/leanprover-community/mathlib/blob/master/src/ring_theory/ideal_operations.lean#L556

You can then type I • ⊤ for the product (• = "\bullet", in VScode-lean, also ⊤ = "\top", which is the maximal submodule of M i.e., you can think of it as M itself). Your hypothesis would become I • ⊤ = ⊤.

Upvotes: 5

Related Questions