English
If one has a presentation of T over S and a presentation of S over R, one obtains a presentation of T over R by taking the disjoint sum of generators and appropriately combining relations.
Русский
Имея презентацию T над S и презентацию S над R, получаем презентацию T над R, используя сумму индексов генераторов и составление отношений.
LaTeX
$$$\\mathrm{comp}:\\; \\mathrm{Presentation}\\; R\\; T\\; (ι'\\oplus ι)\\; (σ'\\oplus σ) = (Q \\circ P)$$$
Lean4
/-- Given presentations of `T` over `S` and of `S` over `R`,
we may construct a presentation of `T` over `R`. -/
@[simps -isSimp relation]
noncomputable def comp : Presentation R T (ι' ⊕ ι) (σ' ⊕ σ)
where
toGenerators := Q.toGenerators.comp P.toGenerators
relation := Sum.elim (Q.comp_relation_aux P) (fun rp ↦ MvPolynomial.rename Sum.inr <| P.relation rp)
span_range_relation_eq_ker := Q.span_range_relation_eq_ker_comp P
