comap — Mathlib

English

I.comap f is the preimage of I under f.

Русский

I.comap f есть предобраз I по отношению к f.

LaTeX

$$$I^{\\\\mathrm{comap} f} = f^{-1}(I)$$$

Lean4

/-- `I.comap f` is the preimage of `I` under `f`. -/
def comap [RingHomClass F R S] (I : Ideal S) : Ideal R
    where
  carrier := f ⁻¹' I
  add_mem' {x y} hx
    hy := by
    simp only [Set.mem_preimage, SetLike.mem_coe, map_add f] at hx hy ⊢
    exact add_mem hx hy
  zero_mem' := by simp only [Set.mem_preimage, map_zero, SetLike.mem_coe, Submodule.zero_mem]
  smul_mem' c x
    hx := by
    simp only [smul_eq_mul, Set.mem_preimage, map_mul, SetLike.mem_coe] at *
    exact mul_mem_left I _ hx

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