English
A detailed constructive proof showing how to build the (Q.comp P).ker element from a Q.ker element, by decomposing into monomials and matching coefficients.
Русский
Детальное конструкторское доказательство того, как построить элемент \\((Q.comp P).ker\\) из элемента \\(Q.ker\\) путём разложения по мономамам и сопоставления коэффициентов.
LaTeX
$$$\\text{proof1}$$$
Lean4
/-- Given `R[X] → S` and `S[Y] → T`, this is the lift of an element in `ker(S[Y] → T)`
to `ker(R[X][Y] → S[Y] → T)` constructed from `P.σ`.
-/
noncomputable def kerCompPreimage (Q : Generators S T ι') (P : Generators R S ι) (x : Q.ker) : (Q.comp P).ker :=
by
refine ⟨x.1.sum fun n r ↦ ?_, ?_⟩
· -- The use of `refine` is intentional to control the elaboration order
-- so that the term has type `(Q.comp P).Ring` and not `MvPolynomial (Q.vars ⊕ P.vars) R`
refine rename ?_ (P.σ r) * monomial ?_ 1
exacts [Sum.inr, n.mapDomain Sum.inl]
· simp only [ker_eq_ker_aeval_val, RingHom.mem_ker]
conv_rhs => rw [← aeval_val_eq_zero x.2, ← x.1.support_sum_monomial_coeff]
simp only [Finsupp.sum, map_sum, map_mul, aeval_rename, Function.comp_def, comp_val, Sum.elim_inr, aeval_monomial,
map_one, Finsupp.prod_mapDomain_index_inj Sum.inl_injective, Sum.elim_inl, one_mul]
congr! with v i
simp_rw [← IsScalarTower.toAlgHom_apply R, ← comp_aeval, AlgHom.comp_apply, P.aeval_val_σ, coeff]
