English
This theorem asserts that applying the composed map to the kernel preimage recovers the original kernel element.
Русский
Это утверждение говорит, что применение составного отображения к элементу из диагонали предварительного образа ядра восстанавливает исходный элемент ядра.
LaTeX
$$$(Q.ofComp P).toAlgHom (Q.kerCompPreimage P x) = x$$$
Lean4
theorem ofComp_kerCompPreimage (Q : Generators S T ι') (P : Generators R S ι) (x : Q.ker) :
(Q.ofComp P).toAlgHom (kerCompPreimage Q P x) = x :=
by
conv_rhs => rw [← x.1.support_sum_monomial_coeff]
rw [kerCompPreimage, map_finsuppSum, Finsupp.sum]
refine Finset.sum_congr rfl fun j _ ↦ ?_
simp only [map_mul, Hom.toAlgHom_monomial]
rw [one_smul, Finsupp.prod_mapDomain_index_inj Sum.inl_injective]
rw [rename, ← AlgHom.comp_apply, comp_aeval]
simp only [ofComp_val, Sum.elim_inr, Function.comp_apply, Sum.elim_inl, monomial_eq, Hom.toAlgHom_X]
congr 1
rw [aeval_def, IsScalarTower.algebraMap_eq R S, ← MvPolynomial.algebraMap_eq, ← coe_eval₂Hom, ← map_aeval,
P.aeval_val_σ]
simp [coeff]
