Documentation

Mathlib.Algebra.Module.Presentation.Basic

Presentations of modules #

Given a ring A, we introduce a structure Relations A which contains the data that is necessary to define a module by generators and relations. A term relations : Relations A involves two index types: a type G for the generators and a type R for the relations. The relation attached to r : R is an element G →₀ A which expresses the coefficients of the expected linear relation.

One may think of relations : Relations A as a particular shape for systems of linear equations in any A-module M. Each g : G can be thought of as a variable (in M) and each r : R specifies a linear relation that these variables should satisfy. This way, we get a type relations.Solution M. Then, if solution : relations.Solution M, we introduce the predicate solution.IsPresentation which asserts that solution is the universal solution to the given equations, i.e. solution gives a presentation of M by generators and relations.

Given an A-module M, we also introduce the type Presentation A M which contains all the data and properties involved in a presentation of M by generators and relations.

TODO #

structure Module.Relations (A : Type u) [Ring A] :
Type (max (max u (w₀ + 1)) (w₁ + 1))

Given a ring A, this structure involves a family of elements (indexed by a type R) in a free module G →₀ A. This allows to define an A-module by generators and relations, see Relations.Quotient.

  • G : Type w₀

    the index type for generators

  • R : Type w₁

    the index type for relations

  • relation (r : self.R) : self.G →₀ A

    the coefficients of the linear relations that are expected between the generators

def Module.Relations.Quotient {A : Type u} [Ring A] (relations : Relations A) :
Type (max u w₀)

The module that is presented by generators and relations given by relations : Relations A. This is the quotient of the free A-module on relations.G by the submodule generated by the given relations.

Equations
noncomputable instance Module.Relations.instAddCommGroupQuotient {A : Type u} [Ring A] (relations : Relations A) :
Equations
noncomputable instance Module.Relations.instQuotient {A : Type u} [Ring A] (relations : Relations A) :
Module A relations.Quotient
Equations
def Module.Relations.toQuotient {A : Type u} [Ring A] (relations : Relations A) :
(relations.G →₀ A) →ₗ[A] relations.Quotient

The canonical (surjective) linear map (relations.G →₀ A) →ₗ[A] relations.Quotient.

Equations
theorem Module.Relations.Quotient.linearMap_ext {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] {f f' : relations.Quotient →ₗ[A] M} (h : ∀ (g : relations.G), f (relations.toQuotient (Finsupp.single g 1)) = f' (relations.toQuotient (Finsupp.single g 1))) :
f = f'
@[simp]
theorem Module.Relations.toQuotient_relation {A : Type u} [Ring A] (relations : Relations A) (r : relations.R) :
relations.toQuotient (relations.relation r) = 0
noncomputable def Module.Relations.map {A : Type u} [Ring A] (relations : Relations A) :
(relations.R →₀ A) →ₗ[A] relations.G →₀ A

The linear map (relations.R →₀ A) →ₗ[A] (relations.G →₀ A) corresponding to the relations given by relations : Relations A.

Equations
@[simp]
theorem Module.Relations.map_single {A : Type u} [Ring A] (relations : Relations A) (r : relations.R) :
relations.map (Finsupp.single r 1) = relations.relation r
@[simp]
theorem Module.Relations.range_map {A : Type u} [Ring A] (relations : Relations A) :
@[simp]
theorem Module.Relations.toQuotient_map {A : Type u} [Ring A] (relations : Relations A) :
relations.toQuotient ∘ₗ relations.map = 0
@[simp]
theorem Module.Relations.toQuotient_map_apply {A : Type u} [Ring A] (relations : Relations A) (x : relations.R →₀ A) :
relations.toQuotient (relations.map x) = 0
structure Module.Relations.Solution {A : Type u} [Ring A] (relations : Relations A) (M : Type v) [AddCommGroup M] [Module A M] :
Type (max v w₀)

The type of solutions in a module M of the equations given by relations : Relations A.

theorem Module.Relations.Solution.ext {A : Type u} {inst✝ : Ring A} {relations : Relations A} {M : Type v} {inst✝¹ : AddCommGroup M} {inst✝² : Module A M} {x y : relations.Solution M} (var : x.var = y.var) :
x = y
noncomputable def Module.Relations.Solution.π {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) :
(relations.G →₀ A) →ₗ[A] M

Given relations : Relations A and a solution in relations.Solution M, this is the linear map (relations.G →₀ A) →ₗ[A] M canonically associated to the solution.

Equations
@[simp]
theorem Module.Relations.Solution.π_single {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) (g : relations.G) :
solution.π (Finsupp.single g 1) = solution.var g
@[simp]
theorem Module.Relations.Solution.π_relation {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) (r : relations.R) :
solution.π (relations.relation r) = 0
@[simp]
theorem Module.Relations.Solution.π_comp_map {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) :
solution.π ∘ₗ relations.map = 0
@[simp]
theorem Module.Relations.Solution.π_comp_map_apply {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) (x : relations.R →₀ A) :
solution.π (relations.map x) = 0
theorem Module.Relations.Solution.range_π {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) :
theorem Module.Relations.Solution.span_relation_le_ker_π {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) :
noncomputable def Module.Relations.Solution.fromQuotient {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) :
relations.Quotient →ₗ[A] M

Given relations : Relations A and solution : relations.Solution M, this is the canonical linear map relations.Quotient →ₗ[A] M from the module.

Equations
@[simp]
theorem Module.Relations.Solution.fromQuotient_comp_toQuotient {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) :
solution.fromQuotient ∘ₗ relations.toQuotient = solution.π
@[simp]
theorem Module.Relations.Solution.fromQuotient_toQuotient {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) (x : relations.G →₀ A) :
solution.fromQuotient (relations.toQuotient x) = solution.π x
def Module.Relations.Solution.postcomp {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) {N : Type v'} [AddCommGroup N] [Module A N] (f : M →ₗ[A] N) :
relations.Solution N

The image of a solution to relations : Relation A by a linear map M →ₗ[A] N.

Equations
  • solution.postcomp f = { var := fun (g : relations.G) => f (solution.var g), linearCombination_var_relation := }
@[simp]
theorem Module.Relations.Solution.postcomp_var {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) {N : Type v'} [AddCommGroup N] [Module A N] (f : M →ₗ[A] N) (g : relations.G) :
(solution.postcomp f).var g = f (solution.var g)
@[simp]
theorem Module.Relations.Solution.postcomp_comp {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) {N : Type v'} [AddCommGroup N] [Module A N] (f : M →ₗ[A] N) {N' : Type v''} [AddCommGroup N'] [Module A N'] (g : N →ₗ[A] N') :
solution.postcomp (g ∘ₗ f) = (solution.postcomp f).postcomp g
@[simp]
theorem Module.Relations.Solution.postcomp_id {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) :
solution.postcomp LinearMap.id = solution
theorem Module.Relations.Solution.congr_var {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution solution' : relations.Solution M} (h : solution = solution') (g : relations.G) :
solution.var g = solution'.var g
theorem Module.Relations.Solution.congr_postcomp {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} {N : Type v'} [AddCommGroup N] [Module A N] {solution' : relations.Solution M} (h : solution = solution') (f : M →ₗ[A] N) :
solution.postcomp f = solution'.postcomp f
noncomputable def Module.Relations.Solution.ofπ {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] (π : (relations.G →₀ A) →ₗ[A] M) ( : ∀ (r : relations.R), π (relations.relation r) = 0) :
relations.Solution M

Given relations : Relations A and an A-module M, this is a constructor for relations.Solution M for which the data is given as a linear map π : (relations.G →₀ A) →ₗ[A] M. (See also ofπ' for an alternate vanishing criterion.)

Equations
theorem Module.Relations.Solution.ofπ_var {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] (π : (relations.G →₀ A) →ₗ[A] M) ( : ∀ (r : relations.R), π (relations.relation r) = 0) (g : relations.G) :
(ofπ π ).var g = π (Finsupp.single g 1)
@[simp]
theorem Module.Relations.Solution.ofπ_π {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] (π : (relations.G →₀ A) →ₗ[A] M) ( : ∀ (r : relations.R), π (relations.relation r) = 0) :
(ofπ π ).π = π
noncomputable def Module.Relations.Solution.ofπ' {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] (π : (relations.G →₀ A) →ₗ[A] M) ( : π ∘ₗ relations.map = 0) :
relations.Solution M

Variant of ofπ where the vanishing condition is expressed in terms of a composition of linear maps.

Equations
theorem Module.Relations.Solution.ofπ'_var {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] (π : (relations.G →₀ A) →ₗ[A] M) ( : π ∘ₗ relations.map = 0) (g : relations.G) :
(ofπ' π ).var g = π (Finsupp.single g 1)
@[simp]
theorem Module.Relations.Solution.ofπ'_π {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] (π : (relations.G →₀ A) →ₗ[A] M) ( : π ∘ₗ relations.map = 0) :
(ofπ' π ).π = π
theorem Module.Relations.Solution.surjective_π_iff_span_eq_top {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) :
structure Module.Relations.Solution.IsPresentation {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) :

Given relations : Relations A, an A-module M and solution : relations.Solution M, this property asserts that solution gives a presentation of M by generators and relations.

noncomputable def Module.Relations.Solution.IsPresentation.linearEquiv {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) :
relations.Quotient ≃ₗ[A] M

When M admits a presentation by generators and relations given by solution : relations.Solutions M, this is the associated linear equivalence relations.Quotient ≃ₗ[A] M.

Equations
@[simp]
theorem Module.Relations.Solution.IsPresentation.linearEquiv_apply {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) (x : relations.Quotient) :
h.linearEquiv x = solution.fromQuotient x
@[simp]
theorem Module.Relations.Solution.IsPresentation.linearEquiv_symm_var {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) (g : relations.G) :
h.linearEquiv.symm (solution.var g) = relations.toQuotient (Finsupp.single g 1)
theorem Module.Relations.Solution.IsPresentation.surjective_π {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) :
theorem Module.Relations.Solution.IsPresentation.ker_π {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) :
theorem Module.Relations.Solution.IsPresentation.exact {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) :
Function.Exact relations.map solution.π

The sequence (relations.R →₀ A) → (relations.G →₀ A) → M → 0 is exact.

noncomputable def Module.Relations.Solution.IsPresentation.desc {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'} [AddCommGroup N] [Module A N] (s : relations.Solution N) :

If M admits a presentation by generators and relations, and we have a solution of the same equations in a module N, then this is the canonical induced linear map M →ₗ[A] N.

Equations
@[simp]
theorem Module.Relations.Solution.IsPresentation.desc_var {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'} [AddCommGroup N] [Module A N] (s : relations.Solution N) (g : relations.G) :
(h.desc s) (solution.var g) = s.var g
@[simp]
theorem Module.Relations.Solution.IsPresentation.desc_comp_π {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'} [AddCommGroup N] [Module A N] (s : relations.Solution N) :
h.desc s ∘ₗ solution.π = s.π
@[simp]
theorem Module.Relations.Solution.IsPresentation.π_desc_apply {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'} [AddCommGroup N] [Module A N] (s : relations.Solution N) (x : relations.G →₀ A) :
(h.desc s) (solution.π x) = s.π x
@[simp]
theorem Module.Relations.Solution.IsPresentation.postcomp_desc {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'} [AddCommGroup N] [Module A N] (s : relations.Solution N) :
solution.postcomp (h.desc s) = s
theorem Module.Relations.Solution.IsPresentation.postcomp_injective {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'} [AddCommGroup N] [Module A N] {f f' : M →ₗ[A] N} (h' : solution.postcomp f = solution.postcomp f') :
f = f'
noncomputable def Module.Relations.Solution.IsPresentation.linearMapEquiv {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'} [AddCommGroup N] [Module A N] :
(M →ₗ[A] N) relations.Solution N

If M admits a presentation by generators and relations, then linear maps from M can be (naturally) identified to the solutions of certain linear equations.

Equations
@[simp]
theorem Module.Relations.Solution.IsPresentation.linearMapEquiv_symm_apply {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'} [AddCommGroup N] [Module A N] (s : relations.Solution N) :
@[simp]
theorem Module.Relations.Solution.IsPresentation.linearMapEquiv_apply {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'} [AddCommGroup N] [Module A N] (f : M →ₗ[A] N) :
h.linearMapEquiv f = solution.postcomp f
noncomputable def Module.Relations.Solution.IsPresentation.uniq {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'} [AddCommGroup N] [Module A N] {solution' : relations.Solution N} (h' : solution'.IsPresentation) :

Uniqueness (up to a unique linear equivalence) of the module defined by generators and relations.

Equations
@[simp]
theorem Module.Relations.Solution.IsPresentation.postcomp_uniq {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'} [AddCommGroup N] [Module A N] {solution' : relations.Solution N} (h' : solution'.IsPresentation) :
solution.postcomp (h.uniq h') = solution'
@[simp]
theorem Module.Relations.Solution.IsPresentation.postcomp_uniq_symm {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'} [AddCommGroup N] [Module A N] {solution' : relations.Solution N} (h' : solution'.IsPresentation) :
solution'.postcomp (h.uniq h').symm = solution
@[simp]
theorem Module.Relations.Solution.IsPresentation.uniq_var {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'} [AddCommGroup N] [Module A N] {solution' : relations.Solution N} (h' : solution'.IsPresentation) (g : relations.G) :
(h.uniq h') (solution.var g) = solution'.var g
@[simp]
theorem Module.Relations.Solution.IsPresentation.uniq_symm_var {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'} [AddCommGroup N] [Module A N] {solution' : relations.Solution N} (h' : solution'.IsPresentation) (g : relations.G) :
(h.uniq h').symm (solution'.var g) = solution.var g
theorem Module.Relations.Solution.IsPresentation.of_linearEquiv {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) {N : Type v'} [AddCommGroup N] [Module A N] (e : M ≃ₗ[A] N) :
(solution.postcomp e).IsPresentation
noncomputable def Module.Relations.Solution.ofQuotient {A : Type u} [Ring A] (relations : Relations A) :
relations.Solution relations.Quotient

Given relations : Relations A, this is the obvious solution to relations in the quotient relations.Quotient.

Equations
@[simp]
theorem Module.Relations.Solution.ofQuotient_var {A : Type u} [Ring A] (relations : Relations A) (g : relations.G) :
(ofQuotient relations).var g = relations.toQuotient (Finsupp.single g 1)
@[simp]
theorem Module.Relations.Solution.ofQuotient_π {A : Type u} [Ring A] (relations : Relations A) :
(ofQuotient relations).π = (Submodule.span A (Set.range relations.relation)).mkQ
structure Module.Relations.Solution.IsPresentationCore {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) :
Type (max (max (max u v) (w' + 1)) w₀)

Helper structure in order to prove Module.Relations.Solutions.IsPresentation by showing the universal property of the module defined by generators and relations. The universal property is restricted to modules that are in Type w' for an auxiliary universe w'. See IsPresentationCore.isPresentation.

@[simp]
theorem Module.Relations.Solution.IsPresentationCore.desc_var {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentationCore) {N : Type w'} [AddCommGroup N] [Module A N] (s : relations.Solution N) (g : relations.G) :
(h.desc s) (solution.var g) = s.var g
def Module.Relations.Solution.IsPresentationCore.down {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentationCore) :

The structure IsPresentationCore can be shrunk to a lower universe.

Equations
  • One or more equations did not get rendered due to their size.
theorem Module.Relations.Solution.IsPresentationCore.isPresentation {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentationCore) :
theorem Module.Relations.Solution.isPresentation_iff {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) :
theorem Module.Relations.Solution.isPresentation_mk {A : Type u} [Ring A] {relations : Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) (h₁ : Submodule.span A (Set.range solution.var) = ) (h₂ : LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)) :
structure Module.Presentation (A : Type u) [Ring A] (M : Type v) [AddCommGroup M] [Module A M] extends Module.Relations A, self.Solution M, self.IsPresentation :
Type (max (max (max u v) (w₀ + 1)) (w₁ + 1))

Given an A-module M, a term in this type is a presentation by M by generators and relations.

def Module.Presentation.ofIsPresentation {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] {relations : Relations A} {solution : relations.Solution M} (h : solution.IsPresentation) :

Constructor for Module.Presentation.

Equations
@[simp]
theorem Module.Presentation.ofIsPresentation_toRelations {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] {relations : Relations A} {solution : relations.Solution M} (h : solution.IsPresentation) :
(ofIsPresentation h).toRelations = { G := relations.G, R := relations.R, relation := relations.relation }
@[simp]
theorem Module.Presentation.ofIsPresentation_toSolution {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] {relations : Relations A} {solution : relations.Solution M} (h : solution.IsPresentation) :
def Module.Presentation.ofLinearEquiv {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] (pres : Presentation A M) {N : Type v'} [AddCommGroup N] [Module A N] (e : M ≃ₗ[A] N) :

The presentation of an A-module N that is deduced from a presentation of a module M and a linear equivalence e : M ≃ₗ[A] N.

Equations
@[simp]
theorem Module.Presentation.ofLinearEquiv_toRelations {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] (pres : Presentation A M) {N : Type v'} [AddCommGroup N] [Module A N] (e : M ≃ₗ[A] N) :
(pres.ofLinearEquiv e).toRelations = { G := pres.G, R := pres.R, relation := pres.relation }
@[simp]
theorem Module.Presentation.ofLinearEquiv_toSolution {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] (pres : Presentation A M) {N : Type v'} [AddCommGroup N] [Module A N] (e : M ≃ₗ[A] N) :
(pres.ofLinearEquiv e).toSolution = pres.postcomp e