English
In the finitely-supported case, the prime-ness of constants is preserved under the C embedding.
Русский
При конечной размерности константы сохраняют простоту через отображение C.
LaTeX
$$Prime (C r) ⇔ Prime r$$
Lean4
theorem prime_rename_iff (s : Set σ) {p : MvPolynomial s R} :
Prime (rename ((↑) : s → σ) p) ↔ Prime (p : MvPolynomial s R) := by
classical
symm
let eqv := (sumAlgEquiv R (↥sᶜ) s).symm.trans (renameEquiv R <| (Equiv.sumComm (↥sᶜ) s).trans <| Equiv.Set.sumCompl s)
have : (rename (↑)).toRingHom = eqv.toAlgHom.toRingHom.comp C :=
by
apply ringHom_ext
· intro
simp only [eqv, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, rename_C, AlgEquiv.toAlgHom_eq_coe,
AlgEquiv.toAlgHom_toRingHom, RingHom.coe_comp, AlgEquiv.coe_trans, Function.comp_apply,
MvPolynomial.sumAlgEquiv_symm_apply, iterToSum_C_C, renameEquiv_apply, Equiv.coe_trans, Equiv.sumComm_apply]
· intro
simp only [eqv, AlgHom.toRingHom_eq_coe, RingHom.coe_coe, rename_X, AlgEquiv.toAlgHom_eq_coe,
AlgEquiv.toAlgHom_toRingHom, RingHom.coe_comp, AlgEquiv.coe_trans, Function.comp_apply,
MvPolynomial.sumAlgEquiv_symm_apply, iterToSum_C_X, renameEquiv_apply, Equiv.coe_trans, Equiv.sumComm_apply,
Sum.swap_inr, Equiv.Set.sumCompl_apply_inl]
apply_fun (· p) at this
simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, AlgEquiv.toAlgHom_eq_coe, AlgEquiv.toAlgHom_toRingHom,
RingHom.coe_comp, Function.comp_apply] at this
rw [this, MulEquiv.prime_iff, prime_C_iff]
