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

• Relate this to Module.FinitePresentation
• Behaviour of presentations with respect to the extension of scalars and the restriction of scalars

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 : 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 : Module.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

• relations.Quotient = ((relations.G →₀ A) ⧸ Submodule.span A (Set.range relations.relation))

noncomputable instance Module.Relations.instAddCommGroupQuotient {A : Type u} [Ring A] (relations : Module.Relations A) : AddCommGroup relations.Quotient

Equations

• relations.instAddCommGroupQuotient = id inferInstance

noncomputable instance Module.Relations.instQuotient {A : Type u} [Ring A] (relations : Module.Relations A) : Module A relations.Quotient

Equations

• relations.instQuotient = id inferInstance

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

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

Equations

• relations.toQuotient = (Submodule.span A (Set.range relations.relation)).mkQ

theorem Module.Relations.Quotient.linearMap_ext {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {f : relations.Quotient →ₗ[A] M} {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'

theorem Module.Relations.surjective_toQuotient {A : Type u} [Ring A] (relations : Module.Relations A) : Function.Surjective ⇑relations.toQuotient

theorem Module.Relations.ker_toQuotient {A : Type u} [Ring A] (relations : Module.Relations A) : LinearMap.ker relations.toQuotient = Submodule.span A (Set.range relations.relation)

@[simp]

theorem Module.Relations.toQuotient_relation {A : Type u} [Ring A] (relations : Module.Relations A) (r : relations.R) : relations.toQuotient (relations.relation r) = 0

noncomputable def Module.Relations.map {A : Type u} [Ring A] (relations : Module.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

• relations.map = Finsupp.linearCombination A relations.relation

@[simp]

theorem Module.Relations.map_single {A : Type u} [Ring A] (relations : Module.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 : Module.Relations A) : LinearMap.range relations.map = Submodule.span A (Set.range relations.relation)

@[simp]

theorem Module.Relations.toQuotient_map {A : Type u} [Ring A] (relations : Module.Relations A) : relations.toQuotient ∘ₗ relations.map = 0

@[simp]

theorem Module.Relations.toQuotient_map_apply {A : Type u} [Ring A] (relations : Module.Relations A) (x : relations.R →₀ A) : relations.toQuotient (relations.map x) = 0

structure Module.Relations.Solution {A : Type u} [Ring A] (relations : Module.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.

• var : relations.G → M

  the image in M of each variable

• linearCombination_var_relation : ∀ (r : relations.R), (Finsupp.linearCombination A self.var) (relations.relation r) = 0

theorem Module.Relations.Solution.ext {A : Type u} : ∀ {inst : Ring A} {relations : Module.Relations A} {M : Type v} {inst_1 : AddCommGroup M} {inst_2 : Module A M} {x y : relations.Solution M}, x.var = y.var → x = y

theorem Module.Relations.Solution.linearCombination_var_relation {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (self : relations.Solution M) (r : relations.R) : (Finsupp.linearCombination A self.var) (relations.relation r) = 0

noncomputable def Module.Relations.Solution.π {A : Type u} [Ring A] {relations : Module.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

• solution.π = Finsupp.linearCombination A solution.var

@[simp]

theorem Module.Relations.Solution.π_single {A : Type u} [Ring A] {relations : Module.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 : Module.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 : Module.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 : Module.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 : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) : LinearMap.range solution.π = Submodule.span A (Set.range solution.var)

theorem Module.Relations.Solution.span_relation_le_ker_π {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) : Submodule.span A (Set.range relations.relation) ≤ LinearMap.ker solution.π

noncomputable def Module.Relations.Solution.fromQuotient {A : Type u} [Ring A] {relations : Module.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

• solution.fromQuotient = (Submodule.span A (Set.range relations.relation)).liftQ solution.π ⋯

@[simp]

theorem Module.Relations.Solution.fromQuotient_comp_toQuotient {A : Type u} [Ring A] {relations : Module.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 : Module.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 : Module.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 : Module.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 : Module.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 : Module.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 : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} {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 : Module.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 : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (π : (relations.G →₀ A) →ₗ[A] M) (hπ : ∀ (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

• Module.Relations.Solution.ofπ π hπ = { var := fun (g : relations.G) => π (Finsupp.single g 1), linearCombination_var_relation := ⋯ }

theorem Module.Relations.Solution.ofπ_var {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (π : (relations.G →₀ A) →ₗ[A] M) (hπ : ∀ (r : relations.R), π (relations.relation r) = 0) (g : relations.G) : (Module.Relations.Solution.ofπ π hπ).var g = π (Finsupp.single g 1)

@[simp]

theorem Module.Relations.Solution.ofπ_π {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (π : (relations.G →₀ A) →ₗ[A] M) (hπ : ∀ (r : relations.R), π (relations.relation r) = 0) : (Module.Relations.Solution.ofπ π hπ).π = π

noncomputable def Module.Relations.Solution.ofπ' {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (π : (relations.G →₀ A) →ₗ[A] M) (hπ : π ∘ₗ relations.map = 0) : relations.Solution M

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

Equations

• Module.Relations.Solution.ofπ' π hπ = Module.Relations.Solution.ofπ π ⋯

theorem Module.Relations.Solution.ofπ'_var {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (π : (relations.G →₀ A) →ₗ[A] M) (hπ : π ∘ₗ relations.map = 0) (g : relations.G) : (Module.Relations.Solution.ofπ' π hπ).var g = π (Finsupp.single g 1)

@[simp]

theorem Module.Relations.Solution.ofπ'_π {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (π : (relations.G →₀ A) →ₗ[A] M) (hπ : π ∘ₗ relations.map = 0) : (Module.Relations.Solution.ofπ' π hπ).π = π

theorem Module.Relations.Solution.injective_fromQuotient_iff_ker_π_eq_span {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) : Function.Injective ⇑solution.fromQuotient ↔ LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)

theorem Module.Relations.Solution.surjective_fromQuotient_iff_surjective_π {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) : Function.Surjective ⇑solution.fromQuotient ↔ Function.Surjective ⇑solution.π

theorem Module.Relations.Solution.surjective_π_iff_span_eq_top {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) : Function.Surjective ⇑solution.π ↔ Submodule.span A (Set.range solution.var) = ⊤

structure Module.Relations.Solution.IsPresentation {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) : Prop

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.

• bijective : Function.Bijective ⇑solution.fromQuotient

theorem Module.Relations.Solution.IsPresentation.bijective {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (self : solution.IsPresentation) : Function.Bijective ⇑solution.fromQuotient

noncomputable def Module.Relations.Solution.IsPresentation.linearEquiv {A : Type u} [Ring A] {relations : Module.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

• h.linearEquiv = LinearEquiv.ofBijective solution.fromQuotient ⋯

@[simp]

theorem Module.Relations.Solution.IsPresentation.linearEquiv_apply {A : Type u} [Ring A] {relations : Module.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 : Module.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 : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) : Function.Surjective ⇑solution.π

theorem Module.Relations.Solution.IsPresentation.ker_π {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) : LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)

theorem Module.Relations.Solution.IsPresentation.exact {A : Type u} [Ring A] {relations : Module.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 : Module.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) : M →ₗ[A] 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

• h.desc s = s.fromQuotient ∘ₗ ↑h.linearEquiv.symm

@[simp]

theorem Module.Relations.Solution.IsPresentation.desc_var {A : Type u} [Ring A] {relations : Module.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.postcomp_desc {A : Type u} [Ring A] {relations : Module.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 : Module.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} {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 : Module.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

• h.linearMapEquiv = { toFun := fun (f : M →ₗ[A] N) => solution.postcomp f, invFun := fun (s : relations.Solution N) => h.desc s, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Module.Relations.Solution.IsPresentation.linearMapEquiv_symm_apply {A : Type u} [Ring A] {relations : Module.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.linearMapEquiv.symm s = h.desc s

@[simp]

theorem Module.Relations.Solution.IsPresentation.linearMapEquiv_apply {A : Type u} [Ring A] {relations : Module.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 : Module.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) : M ≃ₗ[A] N

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

Equations

• h.uniq h' = LinearEquiv.ofLinear (h.desc solution') (h'.desc solution) ⋯ ⋯

@[simp]

theorem Module.Relations.Solution.IsPresentation.postcomp_uniq {A : Type u} [Ring A] {relations : Module.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 : Module.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 : Module.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 : Module.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 : Module.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 : Module.Relations A) : relations.Solution relations.Quotient

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

Equations

• Module.Relations.Solution.ofQuotient relations = Module.Relations.Solution.ofπ relations.toQuotient ⋯

@[simp]

theorem Module.Relations.Solution.ofQuotient_var {A : Type u} [Ring A] (relations : Module.Relations A) (g : relations.G) : (Module.Relations.Solution.ofQuotient relations).var g = relations.toQuotient (Finsupp.single g 1)

@[simp]

theorem Module.Relations.Solution.ofQuotient_π {A : Type u} [Ring A] (relations : Module.Relations A) : (Module.Relations.Solution.ofQuotient relations).π = (Submodule.span A (Set.range relations.relation)).mkQ

@[simp]

theorem Module.Relations.Solution.ofQuotient_fromQuotient {A : Type u} [Ring A] (relations : Module.Relations A) : (Module.Relations.Solution.ofQuotient relations).fromQuotient = LinearMap.id

theorem Module.Relations.Solution.ofQuotient_isPresentation {A : Type u} [Ring A] (relations : Module.Relations A) : (Module.Relations.Solution.ofQuotient relations).IsPresentation

structure Module.Relations.Solution.IsPresentationCore {A : Type u} [Ring A] {relations : Module.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.

• desc : {N : Type w'} → [inst : AddCommGroup N] → [inst_1 : Module A N] → relations.Solution N → M →ₗ[A] N

  any solution in a module N : Type w' is obtained in a unique way by postcomposing solution : relations.Solution M by a linear map M →ₗ[A] N.

• postcomp_desc : ∀ {N : Type w'} [inst : AddCommGroup N] [inst_1 : Module A N] (s : relations.Solution N), solution.postcomp (self.desc s) = s
• postcomp_injective : ∀ {N : Type w'} [inst : AddCommGroup N] [inst_1 : Module A N] {f f' : M →ₗ[A] N}, solution.postcomp f = solution.postcomp f' → f = f'

theorem Module.Relations.Solution.IsPresentationCore.postcomp_desc {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (self : solution.IsPresentationCore) {N : Type w'} [AddCommGroup N] [Module A N] (s : relations.Solution N) : solution.postcomp (self.desc s) = s

theorem Module.Relations.Solution.IsPresentationCore.postcomp_injective {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (self : solution.IsPresentationCore) {N : Type w'} [AddCommGroup N] [Module A N] {f : M →ₗ[A] N} {f' : M →ₗ[A] N} (h : solution.postcomp f = solution.postcomp f') : f = f'

@[simp]

theorem Module.Relations.Solution.IsPresentationCore.desc_var {A : Type u} [Ring A] {relations : Module.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 : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentationCore) : 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 : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] {solution : relations.Solution M} (h : solution.IsPresentationCore) : solution.IsPresentation

theorem Module.Relations.Solution.isPresentation_iff {A : Type u} [Ring A] {relations : Module.Relations A} {M : Type v} [AddCommGroup M] [Module A M] (solution : relations.Solution M) : solution.IsPresentation ↔ Submodule.span A (Set.range solution.var) = ⊤ ∧ LinearMap.ker solution.π = Submodule.span A (Set.range relations.relation)

theorem Module.Relations.Solution.isPresentation_mk {A : Type u} [Ring A] {relations : Module.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)) : solution.IsPresentation

structure Module.Presentation (A : Type u) [Ring A] (M : Type v) [AddCommGroup M] [Module A M] extends Module.Relations , Module.Relations.Solution , Module.Relations.Solution.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 : Module.Relations A} {solution : relations.Solution M} (h : solution.IsPresentation) : Module.Presentation A M

Constructor for Module.Presentation.

Equations

• Module.Presentation.ofIsPresentation h = { G := relations.G, R := relations.R, relation := relations.relation, toSolution := solution, toIsPresentation := h }

@[simp]

theorem Module.Presentation.ofIsPresentation_toRelations {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] {relations : Module.Relations A} {solution : relations.Solution M} (h : solution.IsPresentation) : (Module.Presentation.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 : Module.Relations A} {solution : relations.Solution M} (h : solution.IsPresentation) : (Module.Presentation.ofIsPresentation h).toSolution = solution

def Module.Presentation.ofLinearEquiv {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] (pres : Module.Presentation A M) {N : Type v'} [AddCommGroup N] [Module A N] (e : M ≃ₗ[A] N) : Module.Presentation 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

• pres.ofLinearEquiv e = Module.Presentation.ofIsPresentation ⋯

@[simp]

theorem Module.Presentation.ofLinearEquiv_toRelations {A : Type u} [Ring A] {M : Type v} [AddCommGroup M] [Module A M] (pres : Module.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 : Module.Presentation A M) {N : Type v'} [AddCommGroup N] [Module A N] (e : M ≃ₗ[A] N) : (pres.ofLinearEquiv e).toSolution = pres.postcomp ↑e