English
Under hx and h_alg, there is a canonical isomorphism from R<x> / I.map(algebraMap R R<x>) to S / I.map(algebraMap R S).
Русский
При условиях hx и h_alg существует каноническое изоморфизм от R<x> / I.map(algebraMap R R<x>) к S / I.map(algebraMap R S).
LaTeX
$$$R\\langle x\\rangle / I.map(\\mathrm{algebraMap} \\, R \\langle x\\rangle) \\cong_+^* S / I.map(\\mathrm{algebraMap} \\, R S)$$$
Lean4
/-- This technical lemma tell us that if `C` is the conductor of `R<x>` and `I` is an ideal of `R`
then `p * (I * S) ⊆ I * R<x>` for any `p` in `C ∩ R` -/
theorem prod_mem_ideal_map_of_mem_conductor {p : R} {z : S} (hp : p ∈ Ideal.comap (algebraMap R S) (conductor R x))
(hz' : z ∈ I.map (algebraMap R S)) : algebraMap R S p * z ∈ algebraMap R<x> S '' ↑(I.map (algebraMap R R<x>)) :=
by
rw [Ideal.map, Ideal.span, Finsupp.mem_span_image_iff_linearCombination] at hz'
obtain ⟨l, H, H'⟩ := hz'
rw [Finsupp.linearCombination_apply] at H'
rw [← H', mul_comm, Finsupp.sum_mul]
have lem :
∀ {a : R}, a ∈ I → l a • algebraMap R S a * algebraMap R S p ∈ algebraMap R<x> S '' I.map (algebraMap R R<x>) :=
by
intro a ha
rw [Algebra.id.smul_eq_mul, mul_assoc, mul_comm, mul_assoc, Set.mem_image]
refine Exists.intro (algebraMap R R<x> a * ⟨l a * algebraMap R S p, show l a * algebraMap R S p ∈ R<x> from ?h⟩) ?_
case h =>
rw [mul_comm]
exact mem_conductor_iff.mp (Ideal.mem_comap.mp hp) _
· refine ⟨?_, ?_⟩
· rw [mul_comm]
apply Ideal.mul_mem_left (I.map (algebraMap R R<x>)) _ (Ideal.mem_map_of_mem _ ha)
· simp only [RingHom.map_mul, mul_comm (algebraMap R S p) (l a)]
rfl
refine Finset.sum_induction _ (fun u => u ∈ algebraMap R<x> S '' I.map (algebraMap R R<x>)) (fun a b => ?_) ?_ ?_
· rintro ⟨z, hz, rfl⟩ ⟨y, hy, rfl⟩
rw [← RingHom.map_add]
exact ⟨z + y, Ideal.add_mem _ (SetLike.mem_coe.mp hz) hy, rfl⟩
· exact ⟨0, SetLike.mem_coe.mpr <| Ideal.zero_mem _, RingHom.map_zero _⟩
· intro y hy
exact lem ((Finsupp.mem_supported _ l).mp H hy)
