map_symm_map — Mathlib

English

For I ∈ FractionalIdeal S P', mapping by g.symm then by g yields I: (I.map g.symm).map g = I.

Русский

Для I ∈ FractionalIdeal S P', отображение через g.symm затем через g возвращает I: (I.map g.symm).map g = I.

LaTeX

$$$ (I.map (g.symm : P' \\rightarrowₐ[R] P)).map (g : P \\rightarrowₐ[R] P') = I $$$

Lean4

@[simp]
theorem map_symm_map (I : FractionalIdeal S P') (g : P ≃ₐ[R] P') :
    (I.map (g.symm : P' →ₐ[R] P)).map (g : P →ₐ[R] P') = I := by rw [← map_comp, g.comp_symm, map_id]

Похожие утверждения