English
Let A be a ring and M an A-module. There exists a presentation of M by generators [m] for every m in M, with relations [m1] + [m2] = [m1 + m2] and a · [m] = [a · m] for all m, m1, m2 in M and a in A. This presentation encodes the entire module structure tautologically via generators and the two basic linear relations.
Русский
Пусть A — кольцо, M — A-модуль. Существует презентация M порождателями [m] для каждого m ∈ M и отношениями [m1] + [m2] = [m1 + m2] и a · [m] = [a · m] для всех m, m1, m2 ∈ M и a ∈ A. Эта презентация тавтологически кодирует всю структуру модуля через порождающие и две базовые линейные отношения.
LaTeX
$$$$ M \\cong_A \\left(\\bigoplus_{m \\in M} A\\right) \\Big/ \\Big\\langle e_{m_1}+e_{m_2}-e_{m_1+m_2},\\; a\\,e_m-e_{a m} \\Big\\rangle \\,. $$$$
Lean4
/-- The tautological presentation of any `A`-module `M` by generators and relations.
There is a generator `[m]` for any element `m : M`, and there are two types of relations:
* `[m₁] + [m₂] - [m₁ + m₂] = 0`
* `a • [m] - [a • m] = 0`. -/
@[simps!]
noncomputable def tautological : Presentation A M :=
ofIsPresentation (tautologicalSolution_isPresentation A M)
