English
Direct sums of module relations define a combined presentation whose generators are indexed by pairs (i, generators of i) and relations index accordingly.
Русский
Прямой сумма модульных отношений задаёт объединённую презентацию, где генераторы индексируются парами (i, генераторы i-го).
LaTeX
$$$directSum : Relations\\, A \\toRelations A$ with $G := \\Sigma i, (relations i).G$, $R := \\Sigma i, (relations i).R$ and a relation mapping sending $(i,r)$ to the respective relation in i.$$
Lean4
/-- 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. -/
@[simps G R relation]
noncomputable def directSum : Relations A where
G := Σ i, (relations i).G
R := Σ i, (relations i).R
relation := fun ⟨i, r⟩ ↦
Finsupp.embDomain (Function.Embedding.sigmaMk (β := fun i ↦ (relations i).G) i) ((relations i).relation r)
