English
There is a ring isomorphism between FractionalIdeal S P and FractionalIdeal S P' induced by the algebra equivalence g.
Русский
Существует кольцевой изоморфизм между FractionalIdeal S P и FractionalIdeal S P', индуцированный эквивалентностью g.
LaTeX
$$$ \\mathrm{mapEquiv}(g) : \\mathrm{FractionalIdeal}(S,P) \\cong^+_* \\mathrm{FractionalIdeal}(S,P') $$$
Lean4
/-- If `g` is an equivalence, `map g` is an isomorphism -/
def mapEquiv (g : P ≃ₐ[R] P') : FractionalIdeal S P ≃+* FractionalIdeal S P'
where
toFun := map g
invFun := map g.symm
map_add' I J := FractionalIdeal.map_add I J _
map_mul' I J := FractionalIdeal.map_mul I J _
left_inv I := by rw [← map_comp, AlgEquiv.symm_comp, map_id]
right_inv I := by rw [← map_comp, AlgEquiv.comp_symm, map_id]
