map_comap_eq — Mathlib

English

For a ring hom f and a subfield s of L, the map of the comap of s under f equals the infimum of s with the field-range of f.

Русский

Для кольцогомомора f и подполя s над L отображение образа обратного изображения равно пересечению s с диапазоном f.

LaTeX

$$$ (s.\\mathrm{comap}\ f).\\mathrm{map}\ f = s \\cap f\\mathrm{.fieldRange}$$$

Lean4

theorem map_comap_eq (f : K →+* L) (s : Subfield L) : (s.comap f).map f = s ⊓ f.fieldRange :=
  SetLike.coe_injective Set.image_preimage_eq_inter_range

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