English
Let φ: A → B be the A-algebra map. For every g in G, the contraction of the g‑rotated ideal g · P to A equals the contraction of P to A; i.e. φ^{-1}(g · P) = φ^{-1}(P) for all g ∈ G.
Русский
Пусть φ: A → B — A-алгебраическое отображение. Для каждого элемента g из G конрактия (сжатие) идеала g · P из B в A совпадает с конрактией P; то есть φ^{-1}(g · P) = φ^{-1}(P) для всех g ∈ G.
LaTeX
$$$ (\\operatorname{algebraMap}(A,B))^{-1}(g \\cdot P) = (\\operatorname{algebraMap}(A,B))^{-1}(P) \\quad \\forall g \\in G. $$$
Lean4
@[simp]
theorem under_smul : (g • P : Ideal B).under A = P.under A :=
by
ext a
rw [mem_comap, mem_comap, mem_pointwise_smul_iff_inv_smul_mem, smul_algebraMap]
