Documentation

Mathlib.Algebra.Module.Presentation.Tautological

The tautological presentation of a module #

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

source
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
source
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.

Equations
  • One or more equations did not get rendered due to their size.
source
@[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
source
@[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₂ => Finsupp.single m₁ 1 + Finsupp.single m₂ 1 - Finsupp.single (m₁ + m₂) 1 | tautological.R.smul a m => a • Finsupp.single m 1 - Finsupp.single (a • m) 1
source
@[simp]
theorem Module.Presentation.tautologicalRelations_G (A : Type u) [Ring A] (M : Type v) [AddCommGroup M] [Module A M] :
(tautologicalRelations A M).G = M
source
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.

Equations
  • One or more equations did not get rendered due to their size.
source
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.

Equations
source
@[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
source
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.

Equations
  • One or more equations did not get rendered due to their size.
source
theorem Module.Presentation.tautologicalSolution_isPresentation (A : Type u) [Ring A] (M : Type v) [AddCommGroup M] [Module A M] :
(tautologicalSolution A M).IsPresentation
source
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.
Equations
source
@[simp]
theorem Module.Presentation.tautological_G (A : Type u) [Ring A] (M : Type v) [AddCommGroup M] [Module A M] :
(tautological A M).G = M
source
@[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
source
@[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₂ => Finsupp.single m₁ 1 + Finsupp.single m₂ 1 - Finsupp.single (m₁ + m₂) 1 | tautological.R.smul a m => Finsupp.single m a - Finsupp.single (a • m) 1
source
@[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