map_comap_eq — Mathlib

English

For any field homomorphism f, the image under map of the comap equals the intersection with the range of f.

Русский

При любом гомоморфизме полей f образ map(comap f S) равен S ⊓ fieldRange(f).

LaTeX

$$$(\operatorname{map} f (\operatorname{comap} f S)) = S \cap f.fieldRange$$$

Lean4

theorem map_comap_eq (f : L →ₐ[K] L') (S : IntermediateField K L') : (S.comap f).map f = S ⊓ f.fieldRange :=
  SetLike.coe_injective Set.image_preimage_eq_inter_range

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