comap_comap — Mathlib

English

For two ring homomorphisms f: R → S and g: S → T and an ideal I ⊆ T, the comap along the composition equals the composition of comaps: (I.comap g).comap f = I.comap (g ∘ f).

Русский

Пусть $f:R\\to S$, $g:S\\to T$ — кольцевые гомоморфизмы, и I — идеал T. Тогда $(I\\circ g)\\circ f = I\\circ (g\\circ f)$.

LaTeX

$$$ (I^{\\mathrm{comap}(g)})^{\\mathrm{comap}(f)} = I^{\\mathrm{comap}(g\\circ f)} $$$

Lean4

theorem comap_comap (I : TwoSidedIdeal T) (f : R →+* S) (g : S →+* T) : (I.comap g).comap f = I.comap (g.comp f) := by
  ext; simp [mem_comap]

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