English
Let Q be a family of generators S → T indexed by ι′ and let P be a family of generators R → S indexed by ι. Then there exists a canonical family of generators R → T indexed by ι′ ⊕ ι obtained by combining Q and P; the evaluation maps are defined by val = Sum.elim Q.val (S ↪→ T ∘ P.val), and the structure maps σ′ and aevalValσ′ are given by the stated formulae, making this a valid generator family over R → T.
Русский
Пусть Q — семейство генераторов S → T индексированное по ι′, а P — семейство генераторов R → S индексированное по ι. Тогда существует каноническое семейство генераторов R → T индексированное по ι′ ⊕ ι, получаемое из объединения Q и P; отображение val дано через Sum.elim, а соответствующие σ′ и aevalValσ′ задаются указанными формулами, образуя корректное семейство генераторов над R → T.
LaTeX
$$$\\exists G : \\text{Generators } R\\,T\\, (\\iota' \\oplus \\iota)\\text{ such that } G.{val} = \\mathrm{Sum.elim}(Q.{val}, (\\mathrm{algebraMap}\\, S \\to T) \\circ P.{val}), \\\\ G.{σ'}(x) = (Q.{σ}\\,x).sum \\big(\\lambda n\\, r \\;\\mapsto\\; \\mathrm{rename}\\, \\mathrm{Sum.inr}\\,(P.{σ} r) \\cdot \\mathrm{monomial}\\,(n.mapDomain(\\mathrm Sum.inl))\, 1\\big), \\\\ G.aeval\\_val\\_σ'(s) = \\text{(specified in Lean)}$$$
Lean4
/-- Given two families of generators `S[X] → T` and `R[Y] → S`,
we may construct the family of generators `R[X, Y] → T`. -/
@[simps val, simps -isSimp σ]
noncomputable def comp (Q : Generators S T ι') (P : Generators R S ι) : Generators R T (ι' ⊕ ι)
where
val := Sum.elim Q.val (algebraMap S T ∘ P.val)
σ' x := (Q.σ x).sum (fun n r ↦ rename Sum.inr (P.σ r) * monomial (n.mapDomain Sum.inl) 1)
aeval_val_σ'
s :=
by
have (x : P.Ring) : aeval (algebraMap S T ∘ P.val) x = algebraMap S T (aeval P.val x) := by
rw [map_aeval, aeval_def, coe_eval₂Hom, ← IsScalarTower.algebraMap_eq, Function.comp_def]
conv_rhs => rw [← Q.aeval_val_σ s, ← (Q.σ s).sum_single]
simp only [map_finsuppSum, map_mul, aeval_rename, Sum.elim_comp_inr, this, aeval_val_σ, aeval_monomial, map_one,
Finsupp.prod_mapDomain_index_inj Sum.inl_injective, Sum.elim_inl, one_mul, single_eq_monomial]
