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) : Module.Presentation.tautological.R A M
• smul {A : Type u} {M : Type v} (a : A) (m : M) : Module.Presentation.tautological.R A M

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[simp]

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

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] : (Module.Presentation.tautologicalRelations A M).Solution N ≃ (M →ₗ[A] N)

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

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• Module.Presentation.tautologicalSolution A M = Module.Presentation.tautologicalRelationsSolutionEquiv.symm LinearMap.id

@[simp]

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

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

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

Equations

• One or more equations did not get rendered due to their size.

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

noncomputable def Module.Presentation.tautological (A : Type u) [Ring A] (M : Type v) [AddCommGroup M] [Module A M] : Module.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.

Equations

• Module.Presentation.tautological A M = Module.Presentation.ofIsPresentation ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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