The tautological presentation of a module

Given an A-module M, we provide its tautological presentation:

• there is a generator [m] for each m : M;
• the relations are [m₁] + [m₂] - [m₁ + m₂] = 0 and a • [m] - [a • m] = 0.

inductive Module.Presentation.tautological.R (A : Type u) (M : Type v) : Type (max u v)

The type which parametrizes the tautological relations in an A-module M.

• add {A : Type u} {M : Type v} (m₁ m₂ : M) : R A M
• smul {A : Type u} {M : Type v} (a : A) (m : M) : R A M

noncomputable def Module.Presentation.tautologicalRelations (A : Type u) [Ring A] (M : Type v) [AddCommGroup M] [Module A M] : Relations A

The system of equations corresponding to the tautological presentation of an A-module.

@[simp]

theorem Module.Presentation.tautologicalRelations_R (A : Type u) [Ring A] (M : Type v) [AddCommGroup M] [Module A M] : (tautologicalRelations A M).R = tautological.R A M

@[simp]

theorem Module.Presentation.tautologicalRelations_relation (A : Type u) [Ring A] (M : Type v) [AddCommGroup M] [Module A M] (x✝ : tautological.R A M) : (tautologicalRelations A M).relation x✝ = match x✝ with | tautological.R.add m₁ m₂ => ((fun₀ | m₁ => 1) + fun₀ | m₂ => 1) - fun₀ | m₁ + m₂ => 1 | tautological.R.smul a m => (a • fun₀ | m => 1) - fun₀ | a • m => 1

@[simp]

theorem Module.Presentation.tautologicalRelations_G (A : Type u) [Ring A] (M : Type v) [AddCommGroup M] [Module A M] : (tautologicalRelations A M).G = M

noncomputable def Module.Presentation.tautologicalRelationsSolutionEquiv {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] {N : Type w} [AddCommGroup N] [Module A N] : (tautologicalRelations A M).Solution N ≃ (M →ₗ[A] N)

Solutions of tautologicalRelations A M in an A-module N identify to M →ₗ[A] N.

noncomputable def Module.Presentation.tautologicalSolution (A : Type u) [Ring A] (M : Type v) [AddCommGroup M] [Module A M] : (tautologicalRelations A M).Solution M

The obvious solution of tautologicalRelations A M in the module M.

@[simp]

theorem Module.Presentation.tautologicalSolution_var (A : Type u) [Ring A] (M : Type v) [AddCommGroup M] [Module A M] (a : M) : (tautologicalSolution A M).var a = a

noncomputable def Module.Presentation.tautologicalSolutionIsPresentationCore (A : Type u) [Ring A] (M : Type v) [AddCommGroup M] [Module A M] : (tautologicalSolution A M).IsPresentationCore

Any A-module admits a tautological presentation by generators and relations.

theorem Module.Presentation.tautologicalSolution_isPresentation (A : Type u) [Ring A] (M : Type v) [AddCommGroup M] [Module A M] : (tautologicalSolution A M).IsPresentation

noncomputable def Module.Presentation.tautological (A : Type u) [Ring A] (M : Type v) [AddCommGroup M] [Module A M] : Presentation A M

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.

@[simp]

theorem Module.Presentation.tautological_var (A : Type u) [Ring A] (M : Type v) [AddCommGroup M] [Module A M] (a : M) : (tautological A M).var a = a

@[simp]

theorem Module.Presentation.tautological_R (A : Type u) [Ring A] (M : Type v) [AddCommGroup M] [Module A M] : (tautological A M).R = tautological.R A M

@[simp]

theorem Module.Presentation.tautological_relation (A : Type u) [Ring A] (M : Type v) [AddCommGroup M] [Module A M] (x✝ : tautological.R A M) : (tautological A M).relation x✝ = match x✝ with | tautological.R.add m₁ m₂ => ((fun₀ | m₁ => 1) + fun₀ | m₂ => 1) - fun₀ | m₁ + m₂ => 1 | tautological.R.smul a m => (fun₀ | m => a) - fun₀ | a • m => 1

@[simp]

theorem Module.Presentation.tautological_G (A : Type u) [Ring A] (M : Type v) [AddCommGroup M] [Module A M] : (tautological A M).G = M