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
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
Instances For
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))
Instances For
The canonical (surjective) linear map (relations.G →₀ A) →ₗ[A] relations.Quotient
.
Equations
- relations.toQuotient = (Submodule.span A (Set.range relations.relation)).mkQ
Instances For
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
Instances For
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
Instances For
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
Instances For
Given relations : Relations A
and solution : relations.Solution M
,
this is the canonical linear map from relations.R →₀ A
to the kernel
of solution.π : (relations.G →₀ A) →ₗ[A] M
.
Equations
- solution.mapToKer = LinearMap.codRestrict (LinearMap.ker solution.π) relations.map ⋯
Instances For
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.π ⋯
Instances For
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 := ⋯ }
Instances For
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 := ⋯ }
Instances For
Variant of ofπ
where the vanishing condition is expressed in terms
of a composition of linear maps.
Equations
Instances For
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
Instances For
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 ⋯
Instances For
The sequence (relations.R →₀ A) → (relations.G →₀ A) → M → 0
is exact.
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
Instances For
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
Instances For
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) ⋯ ⋯
Instances For
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 ⋯
Instances For
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 postcomposingsolution : relations.Solution M
by a linear mapM →ₗ[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
Instances For
The structure IsPresentationCore
can be shrunk to a lower universe.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given an A
-module M
, a term in this type is a presentation by M
by
generators and relations.
Instances For
Constructor for Module.Presentation
.
Equations
- Module.Presentation.ofIsPresentation h = { G := relations.G, R := relations.R, relation := relations.relation, toSolution := solution, toIsPresentation := h }