Presentation of free modules

A module is free iff it admits a presentation with generators but no relation, see Module.free_iff_exists_presentation.

noncomputable def Module.Relations.solutionFinsupp {A : Type u} [Ring A] (relations : Module.Relations A) [IsEmpty relations.R] : relations.Solution (relations.G →₀ A)

If relations : Relations A involved no relation, then it has an obvious solution in the module relations.G →₀ A.

Equations

• relations.solutionFinsupp = { var := fun (g : relations.G) => Finsupp.single g 1, linearCombination_var_relation := ⋯ }

@[simp]

theorem Module.Relations.solutionFinsupp_var {A : Type u} [Ring A] (relations : Module.Relations A) [IsEmpty relations.R] (g : relations.G) : relations.solutionFinsupp.var g = Finsupp.single g 1

noncomputable def Module.Relations.solutionFinsupp.isPresentationCore {A : Type u} [Ring A] (relations : Module.Relations A) [IsEmpty relations.R] : relations.solutionFinsupp.IsPresentationCore

If relations : Relations A involves no relations ([IsEmpty relations.R]), then the free module relations.G →₀ A satisfies the universal property of the corresponding module defined by generators (and relations).

Equations

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

theorem Module.Relations.solutionFinsupp_isPresentation {A : Type u} [Ring A] (relations : Module.Relations A) [IsEmpty relations.R] : relations.solutionFinsupp.IsPresentation

theorem Module.Relations.Solution.IsPresentation.free {A : Type u} [Ring A] {relations : Module.Relations A} (M : Type v) [AddCommGroup M] [Module A M] [IsEmpty relations.R] {solution : relations.Solution M} (h : solution.IsPresentation) : Module.Free A M

noncomputable def Module.presentationFinsupp (A : Type u) [Ring A] (G : Type w₀) : Module.Presentation A (G →₀ A)

The presentation of the A-module G →₀ A with generators indexed by G, and no relation. (Note that there is an auxiliary universe parameter w₁ for the empty type R.)

Equations

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

@[simp]

theorem Module.presentationFinsupp_G (A : Type u) [Ring A] (G : Type w₀) : (Module.presentationFinsupp A G).G = G

@[simp]

theorem Module.presentationFinsupp_var (A : Type u) [Ring A] (G : Type w₀) (g : { G := G, R := PEmpty.{w₁ + 1}, relation := fun (r : PEmpty.{w₁ + 1}) => PEmpty.casesOn (fun (x : PEmpty.{w₁ + 1}) => G →₀ A) r }.G) : (Module.presentationFinsupp A G).var g = Finsupp.single g 1

@[simp]

theorem Module.presentationFinsupp_R (A : Type u) [Ring A] (G : Type w₀) : (Module.presentationFinsupp A G).R = PEmpty.{w₁ + 1}

theorem Module.free_iff_exists_presentation (A : Type u) [Ring A] (M : Type v) [AddCommGroup M] [Module A M] : Module.Free A M ↔ ∃ (p : Module.Presentation A M), IsEmpty p.R