Presentation of a direct sum

If M : ι → Type _ is a family of A-modules, then the data of a presentation of each M i, we obtain a presentation of the module ⨁ i, M i. In particular, from a presentation of an A-module M, we get a presentation of ι →₀ M.

noncomputable def Module.Relations.directSum {A : Type u} [Ring A] {ι : Type w} (relations : ι → Relations A) : Relations A

The direct sum operations on Relations A. Given a family relations : ι → Relations A, the type of generators and relations in directSum relations are the corresponding Sigma types.

@[simp]

theorem Module.Relations.directSum_relation {A : Type u} [Ring A] {ι : Type w} (relations : ι → Relations A) (x✝ : (i : ι) × (relations i).R) : (directSum relations).relation x✝ = match x✝ with | ⟨i, r⟩ => Finsupp.embDomain (Function.Embedding.sigmaMk i) ((relations i).relation r)

@[simp]

theorem Module.Relations.directSum_G {A : Type u} [Ring A] {ι : Type w} (relations : ι → Relations A) : (directSum relations).G = ((i : ι) × (relations i).G)

@[simp]

theorem Module.Relations.directSum_R {A : Type u} [Ring A] {ι : Type w} (relations : ι → Relations A) : (directSum relations).R = ((i : ι) × (relations i).R)

noncomputable def Module.Relations.Solution.directSumEquiv {A : Type u} [Ring A] {ι : Type w} {relations : ι → Relations A} {N : Type v} [AddCommGroup N] [Module A N] : (Relations.directSum relations).Solution N ≃ ((i : ι) → (relations i).Solution N)

Given an A-module N and a family relations : ι → Relations A, the data of a solution of Relations.directSum relations in N is equivalent to the data of a family of solutions of relations i in N for all i.

@[simp]

theorem Module.Relations.Solution.directSumEquiv_apply_var {A : Type u} [Ring A] {ι : Type w} {relations : ι → Relations A} {N : Type v} [AddCommGroup N] [Module A N] (s : (Relations.directSum relations).Solution N) (i : ι) (g : (relations i).G) : (directSumEquiv s i).var g = s.var ⟨i, g⟩

@[simp]

theorem Module.Relations.Solution.directSumEquiv_symm_apply_var {A : Type u} [Ring A] {ι : Type w} {relations : ι → Relations A} {N : Type v} [AddCommGroup N] [Module A N] (t : (i : ι) → (relations i).Solution N) (x✝ : (Relations.directSum relations).G) : (directSumEquiv.symm t).var x✝ = match x✝ with | ⟨i, g⟩ => (t i).var g

noncomputable def Module.Relations.Solution.directSum {A : Type u} [Ring A] {ι : Type w} [DecidableEq ι] {relations : ι → Relations A} {M : ι → Type v} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module A (M i)] (solution : (i : ι) → (relations i).Solution (M i)) : (Relations.directSum relations).Solution (DirectSum ι fun (i : ι) => M i)

Given solution : ∀ (i : ι), (relations i).Solution (M i), this is the canonical solution of Relations.directSum relations in ⨁ i, M i.

@[simp]

theorem Module.Relations.Solution.directSum_var {A : Type u} [Ring A] {ι : Type w} [DecidableEq ι] {relations : ι → Relations A} {M : ι → Type v} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module A (M i)] (solution : (i : ι) → (relations i).Solution (M i)) (i : ι) (g : (relations i).G) : (directSum solution).var ⟨i, g⟩ = (DirectSum.lof A ι M i) ((solution i).var g)

noncomputable def Module.Relations.Solution.IsPresentation.directSum.isRepresentationCore {A : Type u} [Ring A] {ι : Type w} [DecidableEq ι] {relations : ι → Relations A} {M : ι → Type v} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module A (M i)] {solution : (i : ι) → (relations i).Solution (M i)} (h : ∀ (i : ι), (solution i).IsPresentation) : (Solution.directSum solution).IsPresentationCore

The direct sum admits a presentation by generators and relations.

theorem Module.Relations.Solution.IsPresentation.directSum {A : Type u} [Ring A] {ι : Type w} [DecidableEq ι] {relations : ι → Relations A} {M : ι → Type v} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module A (M i)] {solution : (i : ι) → (relations i).Solution (M i)} (h : ∀ (i : ι), (solution i).IsPresentation) : (Solution.directSum solution).IsPresentation

noncomputable def Module.Presentation.directSum {A : Type u} [Ring A] {ι : Type w} [DecidableEq ι] {M : ι → Type v} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module A (M i)] (pres : (i : ι) → Presentation A (M i)) : Presentation A (DirectSum ι fun (i : ι) => M i)

The obvious presentation of the module ⨁ i, M i that is obtained from the data of presentations of the module M i for each i.

@[simp]

theorem Module.Presentation.directSum_R {A : Type u} [Ring A] {ι : Type w} [DecidableEq ι] {M : ι → Type v} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module A (M i)] (pres : (i : ι) → Presentation A (M i)) : (directSum pres).R = ((i : ι) × (pres i).R)

@[simp]

theorem Module.Presentation.directSum_relation {A : Type u} [Ring A] {ι : Type w} [DecidableEq ι] {M : ι → Type v} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module A (M i)] (pres : (i : ι) → Presentation A (M i)) (x✝ : (i : ι) × ((fun (i : ι) => (pres i).toRelations) i).R) : (directSum pres).relation x✝ = Finsupp.embDomain (Function.Embedding.sigmaMk x✝.fst) ((pres x✝.fst).relation x✝.snd)

@[simp]

theorem Module.Presentation.directSum_G {A : Type u} [Ring A] {ι : Type w} [DecidableEq ι] {M : ι → Type v} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module A (M i)] (pres : (i : ι) → Presentation A (M i)) : (directSum pres).G = ((i : ι) × (pres i).G)

@[simp]

theorem Module.Presentation.directSum_var {A : Type u} [Ring A] {ι : Type w} [DecidableEq ι] {M : ι → Type v} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module A (M i)] (pres : (i : ι) → Presentation A (M i)) (i : ι) (g : (pres i).G) : (directSum pres).var ⟨i, g⟩ = (DirectSum.lof A ι M i) ((pres i).var g)

noncomputable def Module.Presentation.finsupp {A : Type u} [Ring A] {N : Type v} [AddCommGroup N] [Module A N] (pres : Presentation A N) (ι : Type w) [DecidableEq ι] [DecidableEq N] : Presentation A (ι →₀ N)

The obvious presentation of the module ι →₀ N that is deduced from a presentation of the module N.

@[simp]

theorem Module.Presentation.finsupp_relation {A : Type u} [Ring A] {N : Type v} [AddCommGroup N] [Module A N] (pres : Presentation A N) (ι : Type w) [DecidableEq ι] [DecidableEq N] (x✝ : (i : ι) × ((fun (i : ι) => ((fun (x : ι) => pres) i).toRelations) i).R) : (pres.finsupp ι).relation x✝ = Finsupp.embDomain (Function.Embedding.sigmaMk x✝.fst) (pres.relation x✝.snd)

@[simp]

theorem Module.Presentation.finsupp_R {A : Type u} [Ring A] {N : Type v} [AddCommGroup N] [Module A N] (pres : Presentation A N) (ι : Type w) [DecidableEq ι] [DecidableEq N] : (pres.finsupp ι).R = ((_ : ι) × pres.R)

@[simp]

theorem Module.Presentation.finsupp_G {A : Type u} [Ring A] {N : Type v} [AddCommGroup N] [Module A N] (pres : Presentation A N) (ι : Type w) [DecidableEq ι] [DecidableEq N] : (pres.finsupp ι).G = ((_ : ι) × pres.G)

@[simp]

theorem Module.Presentation.finsupp_var {A : Type u} [Ring A] {N : Type v} [AddCommGroup N] [Module A N] (pres : Presentation A N) (ι : Type w) [DecidableEq ι] [DecidableEq N] (i : ι) (g : pres.G) : (pres.finsupp ι).var ⟨i, g⟩ = Finsupp.single i (pres.var g)