map_comp — Mathlib

English

The map of a coeIdeal I by g equals the coeIdeal of the image, i.e., map g (I) = I in the fractional ideal sense when I is an ideal.

Русский

Образ по g дробного идеала, возникающего из идеала, равен коэ-идеалу образа: map g (I) = I.

LaTeX

$$map g (coeIdeal I) = coeIdeal (I)$$

Lean4

@[simp]
theorem map_comp (g' : P' →ₐ[R] P'') : I.map (g'.comp g) = (I.map g).map g' :=
  coeToSubmodule_injective (Submodule.map_comp g.toLinearMap g'.toLinearMap I)

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