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 presention of ι →₀ M.

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

Equations

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

@[simp]

theorem Module.Relations.directSum_relation {A : Type u} [Ring A] {ι : Type w} (relations : ι → Module.Relations A) (x✝ : (i : ι) × (relations i).R) : (Module.Relations.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 : ι → Module.Relations A) : (Module.Relations.directSum relations).G = ((i : ι) × (relations i).G)

@[simp]

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

def Module.Relations.Solution.directSumEquiv {A : Type u} [Ring A] {ι : Type w} {relations : ι → Module.Relations A} {N : Type v} [AddCommGroup N] [Module A N] : (Module.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.

Equations

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

@[simp]

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

def Module.Relations.Solution.directSum {A : Type u} [Ring A] {ι : Type w} [DecidableEq ι] {relations : ι → Module.Relations A} {M : ι → Type v} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module A (M i)] (solution : (i : ι) → (relations i).Solution (M i)) : (Module.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.

Equations

• Module.Relations.Solution.directSum solution = Module.Relations.Solution.directSumEquiv.symm fun (i : ι) => (solution i).postcomp (DirectSum.lof A ι M i)

@[simp]

theorem Module.Relations.Solution.directSum_var {A : Type u} [Ring A] {ι : Type w} [DecidableEq ι] {relations : ι → Module.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) : (Module.Relations.Solution.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 : ι → Module.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) : (Module.Relations.Solution.directSum solution).IsPresentationCore

The direct sum admits a presentation by generators and relations.

Equations

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

theorem Module.Relations.Solution.IsPresentation.directSum {A : Type u} [Ring A] {ι : Type w} [DecidableEq ι] {relations : ι → Module.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) : (Module.Relations.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 : ι) → Module.Presentation A (M i)) : Module.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.

Equations

• Module.Presentation.directSum pres = Module.Presentation.ofIsPresentation ⋯

@[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 : ι) → Module.Presentation A (M i)) : (Module.Presentation.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 : ι) → Module.Presentation A (M i)) (r : (Module.Relations.directSum fun (i : ι) => (pres i).toRelations).R) : (Module.Presentation.directSum pres).relation r = match r with | ⟨i, r⟩ => Finsupp.embDomain (Function.Embedding.sigmaMk i) ((pres i).relation r)

@[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 : ι) → Module.Presentation A (M i)) : (Module.Presentation.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 : ι) → Module.Presentation A (M i)) (i : ι) (g : (pres i).G) : (Module.Presentation.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 : Module.Presentation A N) (ι : Type w) [DecidableEq ι] [DecidableEq N] : Module.Presentation A (ι →₀ N)

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

Equations

• pres.finsupp ι = (Module.Presentation.directSum fun (x : ι) => pres).ofLinearEquiv (finsuppLequivDFinsupp A).symm

@[simp]

theorem Module.Presentation.finsupp_relation {A : Type u} [Ring A] {N : Type v} [AddCommGroup N] [Module A N] (pres : Module.Presentation A N) (ι : Type w) [DecidableEq ι] [DecidableEq N] (r : (Module.Presentation.directSum fun (x : ι) => pres).R) : (pres.finsupp ι).relation r = match r with | ⟨i, r⟩ => Finsupp.embDomain (Function.Embedding.sigmaMk i) (pres.relation r)

@[simp]

theorem Module.Presentation.finsupp_R {A : Type u} [Ring A] {N : Type v} [AddCommGroup N] [Module A N] (pres : Module.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 : Module.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 : Module.Presentation A N) (ι : Type w) [DecidableEq ι] [DecidableEq N] (i : ι) (g : pres.G) : (pres.finsupp ι).var ⟨i, g⟩ = Finsupp.single i (pres.var g)