map_comap_map — Mathlib

English

Applying map to the comap of I and then map again yields the original mapped ideal: ((I.map f).comap f).map f = I.map f.

Русский

После применения map к прообразу I и снова map получается исходный образ: ((I.map f).comap f).map f = I.map f.

LaTeX

$$$((\\operatorname{map} f (\\operatorname{comap} f I))).map f = I.map f$$$

Lean4

@[simp]
theorem map_comap_map : ((I.map f).comap f).map f = I.map f :=
  (gc_map_comap f).l_u_l_eq_l I

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