map_comap_eq — Mathlib

English

For a ring hom f : R →+* S and a subsemiring t of S, the induced equality map from t.comap f to t equals the intersection with the image range: map f (comap f t) = t ∩ range(f).

Русский

Для кольцевого гомоморфа f: R →+* S и подпол semiring t ⊆ S выполняется: map f (comap f t) = t ∩ range(f).

LaTeX

$$$\operatorname{map} f (\operatorname{comap} f t) = t \cap f.rangeS$$$

Lean4

theorem map_comap_eq (f : R →+* S) (t : Subsemiring S) : (t.comap f).map f = t ⊓ f.rangeS :=
  SetLike.coe_injective Set.image_preimage_eq_inter_range

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