English
The quotientEquiv sends the coset of x modulo I to the coset of f(x) modulo J.
Русский
quotientEquiv отправляет косет x mod I в косет f(x) mod J.
LaTeX
$$$\text{quotientEquiv } I J f hIJ (\operatorname{Quotient.mk} I x) = \operatorname{Quotient.mk} J (f x)$$$
Lean4
/-- The ring equiv `R/I ≃+* S/J` induced by a ring equiv `f : R ≃+* S`, where `J = f(I)`. -/
@[simps]
def quotientEquiv : R ⧸ I ≃+* S ⧸ J
where
__ := quotientMap J f (hIJ ▸ le_comap_map)
invFun := quotientMap I f.symm (hIJ ▸ (map_comap_of_equiv f).le)
left_inv := by
rintro ⟨r⟩
simp only [Submodule.Quotient.quot_mk_eq_mk, Quotient.mk_eq_mk, RingHom.toFun_eq_coe, quotientMap_mk,
RingEquiv.coe_toRingHom, RingEquiv.symm_apply_apply]
right_inv := by
rintro ⟨s⟩
simp only [Submodule.Quotient.quot_mk_eq_mk, Quotient.mk_eq_mk, RingHom.toFun_eq_coe, quotientMap_mk,
RingEquiv.coe_toRingHom, RingEquiv.apply_symm_apply]
-- Not `@[simp]` since `simp` proves it.
