English
Symmetric image under the inverse of quotMapOfEquivQuotMapCMapSpanMk composed with quotQuotMk yields the expected quotient map.
Русский
Образ под обратной картой quotMapOfEquivQuotMapCMapSpanMk, затем quotQuotMk, даёт ожидаемое отображение квоты.
LaTeX
$$$(quotMapOfEquivQuotMapCMapSpanMk I f).symm (Ideal.Quotient.mk (Ideal.map (span { f }) (I.map C)) p) = Ideal.Quotient.mk (I.map (of f)) p$$$
Lean4
/-- The natural isomorphism `R[α]/((I[x] ⊔ (f)) / (f)) ≅ (R[x]/I[x])/((f) ⊔ I[x] / I[x])`
for `α` a root of `f : R[X]` and `I : Ideal R` -/
def quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk :
AdjoinRoot f ⧸ (I.map (C : R →+* R[X])).map (Ideal.Quotient.mk (span ({ f } : Set R[X]))) ≃+*
(R[X] ⧸ I.map (C : R →+* R[X])) ⧸ (span ({ f } : Set R[X])).map (Ideal.Quotient.mk (I.map (C : R →+* R[X]))) :=
quotQuotEquivComm (Ideal.span ({ f } : Set R[X]))
(I.map (C : R →+* R[X]))
-- This lemma should have the simp tag but this causes a lint issue.
