map_map_symm — Mathlib

English

If g is an algebra equivalence P ≃ₐ[R] P', then mapping I along g and then along g.symm returns I: (I.map g).map g.symm = I.

Русский

Если g — алгебраическое эквивалентство P ≃ₐ[R] P', то последовательный образ через g и затем через g.symm возвращает исходный идеал: (I.map g).map g.symm = I.

LaTeX

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

Lean4

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

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