Lean4
theorem map_toComp_ker (Q : Generators S T ι') (P : Generators R S ι) :
P.ker.map (Q.toComp P).toAlgHom = RingHom.ker (Q.ofComp P).toAlgHom :=
by
letI : DecidableEq (ι' →₀ ℕ) := Classical.decEq _
apply le_antisymm
· rw [Ideal.map_le_iff_le_comap]
rintro x (hx : algebraMap P.Ring S x = 0)
have : (Q.ofComp P).toAlgHom.comp (Q.toComp P).toAlgHom = IsScalarTower.toAlgHom R _ _ := by ext1; simp
simp only [Ideal.mem_comap, RingHom.mem_ker, ← AlgHom.comp_apply, this, IsScalarTower.toAlgHom_apply]
rw [IsScalarTower.algebraMap_apply P.Ring S, hx, map_zero]
· rintro x (h₂ : (Q.ofComp P).toAlgHom x = 0)
let e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
suffices
∑ v ∈ (support x).map e, (monomial (e.symm v)) (coeff (e.symm v) x) ∈
Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
by
simpa only [AlgHom.toRingHom_eq_coe, Finset.sum_map, Equiv.coe_toEmbedding, EquivLike.coe_coe,
AddEquiv.symm_apply_apply, support_sum_monomial_coeff] using this
rw [← Finset.sum_fiberwise_of_maps_to (fun i ↦ Finset.mem_image_of_mem Prod.fst)]
refine sum_mem fun i hi ↦ ?_
convert_to
monomial (e.symm (i, 0)) 1 *
(Q.toComp P).toAlgHom.toRingHom
(∑ j ∈ (support x).map e.toEmbedding with j.1 = i, monomial j.2 (coeff (e.symm j) x)) ∈
_
· rw [map_sum, Finset.mul_sum]
refine Finset.sum_congr rfl fun j hj ↦ ?_
obtain rfl := (Finset.mem_filter.mp hj).2
obtain ⟨i, j⟩ := j
clear hj hi
have :
(Q.toComp P).toAlgHom (monomial j (coeff (e.symm (i, j)) x)) =
monomial (e.symm (0, j)) (coeff (e.symm (i, j)) x) :=
toComp_toAlgHom_monomial ..
simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, this]
rw [monomial_mul, ← map_add, Prod.mk_add_mk, add_zero, zero_add, one_mul]
· apply Ideal.mul_mem_left
refine Ideal.mem_map_of_mem _ ?_
simp only [ker_eq_ker_aeval_val, AddEquiv.toEquiv_eq_coe, RingHom.mem_ker, map_sum]
rw [← coeff_zero i, ← h₂]
clear h₂ hi
have (x : (Q.comp P).Ring) :
(Function.support fun a ↦ if a.1 = i then aeval P.val (monomial a.2 (coeff (e.symm a) x)) else 0) ⊆
((support x).map e).toSet :=
by
rw [← Set.compl_subset_compl]
intro j
obtain ⟨j, rfl⟩ := e.surjective j
simp_all
rw [Finset.sum_filter, ← finsum_eq_sum_of_support_subset _ (this x)]
induction x using MvPolynomial.induction_on' with
| monomial v a =>
rw [finsum_eq_sum_of_support_subset _ (this _), ← Finset.sum_filter]
obtain ⟨v, rfl⟩ := e.symm.surjective v
conv_rhs =>
simp only [e, Finsupp.sumFinsuppAddEquivProdFinsupp, Finsupp.sumFinsuppEquivProdFinsupp, AddEquiv.symm_mk,
AddEquiv.coe_mk, Equiv.coe_fn_symm_mk, ofComp_toAlgHom_monomial_sumElim]
classical
simp only [coeff_monomial, ← e.injective.eq_iff, map_zero, AddEquiv.apply_symm_apply, apply_ite]
rw [← apply_ite, Finset.sum_ite_eq]
simp only [Finset.mem_filter, Finset.mem_map_equiv, AddEquiv.coe_toEquiv_symm, mem_support_iff, coeff_monomial,
↓reduceIte, ne_eq, ite_and, ite_not]
split
· simp only [*, map_zero, ite_self]
· congr
| add p q hp hq =>
simp only [coeff_add, map_add, ite_add_zero]
rw [finsum_add_distrib, hp, hq]
· refine (((support p).map e).finite_toSet.subset ?_)
convert this p
· refine (((support q).map e).finite_toSet.subset ?_)
convert this q
