English
The map invFun is a left inverse of the algebra isomorphism toFunAlgHom; for all x, invFun(toFunAlgHom x) = x.
Русский
Левый обратный элемент: invFun является левым обратным к toFunAlgHom; для всех x выполняется invFun(toFunAlgHom x) = x.
LaTeX
$$invFun_R A( (toFunAlgHom_R A) x ) = x$$
Lean4
theorem left_inv (x : A ⊗ R[X]) : invFun R A ((toFunAlgHom R A) x) = x :=
by
refine TensorProduct.induction_on x ?_ ?_ ?_
· simp [invFun]
· intro a p
dsimp only [invFun]
rw [toFunAlgHom_apply_tmul, eval₂_sum]
simp_rw [eval₂_monomial, AlgHom.coe_toRingHom, Algebra.TensorProduct.tmul_pow, one_pow,
Algebra.TensorProduct.includeLeft_apply, Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul, ←
Algebra.commutes, ← Algebra.smul_def, smul_tmul, sum_def, ← tmul_sum]
conv_rhs => rw [← sum_C_mul_X_pow_eq p]
simp only [Algebra.smul_def]
rfl
· intro p q hp hq
simp only [map_add, invFun_add, hp, hq]
