map_comap_of_equiv — Mathlib

English

If f is a ring equivalence, the map of I along f equals the comap of I along f.symm up to equivalence.

Русский

Если f — эквивалентное отображение, отображение идеала через f эквивалентно обратному образу через f.symm.

LaTeX

$$For a RingEquiv f, I.map f = I.comap f.symm.$$

Lean4

/-- If `f : R ≃+* S` is a ring isomorphism and `I : Ideal R`, then `map f I = comap f.symm I`. -/
theorem map_comap_of_equiv {I : Ideal R} (f : R ≃+* S) : I.map (f : R →+* S) = I.comap f.symm :=
  le_antisymm (Ideal.map_le_comap_of_inverse _ _ _ (Equiv.left_inv' _))
    (Ideal.comap_le_map_of_inverse _ _ _ (Equiv.right_inv' _))

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