English
For a polynomial Q over R, the symmetric quotient map sends Q to its evaluation at x under the isomorphism quotMapEquivQuotQuotMap.
Русский
Для многочлена Q над R симметричное отображение через quotient-map переводит Q в Q(a) через эквивалентность quotMapEquivQuotQuotMap.
LaTeX
$$$$ (quotMapEquivQuotQuotMap(hx,hx')).symm (Q.map (Ideal.Quotient.mk I)) = Q.aeval x. $$$$
Lean4
/-- The isomorphism of rings between `S / I` and `(R / I)[X] / minpoly x` when `I`
and `(conductor R x) ∩ R` are coprime.
-/
noncomputable def quotMapEquivQuotQuotMap (hx : (conductor R x).comap (algebraMap R S) ⊔ I = ⊤) (hx' : IsIntegral R x) :
S ⧸ I.map (algebraMap R S) ≃+* (R ⧸ I)[X] ⧸ span {(minpoly R x).map (Ideal.Quotient.mk I)} :=
(quotAdjoinEquivQuotMap hx (FaithfulSMul.algebraMap_injective (Algebra.adjoin R { x }) S)).symm.trans <|
((Algebra.adjoin.powerBasis' hx').quotientEquivQuotientMinpolyMap I).toRingEquiv.trans <|
quotEquivOfEq (by rw [Algebra.adjoin.powerBasis'_minpoly_gen hx'])
