Блог

Я пытаюсь изучить Lean и пытаюсь выяснить, как можно было бы создать новый R-модуль I*M = {i*m | i in I, m in M} из ideal I и R-модуля M.

Итак, моя попытка состояла в том, чтобы сначала определить map ideal_mult , который создал бы новый R-модуль, а затем выяснить, как назначить для него хорошую нотацию.

 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
  

Как я мог бы это определить, чтобы я мог, например, сформулировать гипотезу, подобную (h: I*M = M) ?

Спасибо за помощь!

Вы должны import ring_theory.ideal_operations . У него есть определение, которое вы хотите на https://github.com/leanprover-community/mathlib/blob/master/src/ring_theory/ideal_operations.lean#L556

Затем вы можете ввести I • ⊤ для продукта ( • = «bullet» в VSCode-lean, также ⊤ = «top», который является максимальным подмодулем M , т.е. вы можете думать о нем как о M нем самом). Ваша гипотеза стала бы I • ⊤ = ⊤ .