English
Let Q be a representative factor of the minimal polynomial of x modulo I. The image under the equivalence normalizes to the span of I.map( algebraMap R S ) together with Q.aeval x. This expresses a span-theoretic correspondence between reductions and generators.
Русский
Пусть Q — представителя множителя минимального полинома x по модулю I. Образ через эквивалентность нормализуется на порождающее подпространство векторного пространства, порождаемое I.map(algebraMap R S) вместе с Q.aeval x.
LaTeX
$$((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm ⟨Q, hQ⟩).val = span (I.map (algebraMap R S) ∪ {Q.aeval x})$$
Lean4
/-- Let `Q` be a lift of factor of the minimal polynomial of `x`, a generator of `S` over `R`, taken
`mod I`. Then (the reduction of) `Q` corresponds via
`normalizedFactorsMapEquivNormalizedFactorsMinPolyMk` to
`span (I.map (algebraMap R S) ∪ {Q.aeval x})`. -/
theorem normalizedFactorsMapEquivNormalizedFactorsMinPolyMk_symm_apply_eq_span (hI : I.IsMaximal) {Q : R[X]}
(hQ : Q.map (Ideal.Quotient.mk I) ∈ normalizedFactors ((minpoly R x).map (Ideal.Quotient.mk I))) (hI' : I ≠ ⊥)
(hx : (conductor R x).comap (algebraMap R S) ⊔ I = ⊤) (hx' : IsIntegral R x) :
((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm ⟨_, hQ⟩).val =
span (I.map (algebraMap R S) ∪ {Q.aeval x}) :=
by
dsimp [normalizedFactorsMapEquivNormalizedFactorsMinPolyMk, normalizedFactorsEquivSpanNormalizedFactors]
rw [normalizedFactorsEquivOfQuotEquiv_symm]
dsimp [normalizedFactorsEquivOfQuotEquiv, idealFactorsEquivOfQuotEquiv, OrderIso.ofHomInv]
simp only [map_span, image_singleton, coe_coe, quotMapEquivQuotQuotMap_symm_apply hx hx' Q]
refine
le_antisymm (fun a ha ↦ ?_)
(span_le.mpr <| union_subset_iff.mpr <| ⟨le_comap_of_map_le (by simp), by simp [mem_span_singleton]⟩)
rw [mem_comap, Ideal.mem_span_singleton] at ha
obtain ⟨a', ha'⟩ := ha
obtain ⟨b, hb⟩ := Ideal.Quotient.mk_surjective a'
rw [← hb, ← map_mul, Quotient.mk_eq_mk_iff_sub_mem] at ha'
rw [union_comm, span_union, span_eq, mem_span_singleton_sup]
exact ⟨b, a - Q.aeval x * b, ha', by ring⟩
