comap_map_eq_self_of_injective — Mathlib

English

If f: A →ₐ[R] B is an injective algebra homomorphism, then for any Subalgebra S of A, comap f (map f S) = S.

Русский

Если f: A →ₐ[R] B является инъективным алгебра-гомоморфизмом, то для любого Subalgebra S ⊆ A имеет место comap f (map f S) = S.

LaTeX

$$$\operatorname{comap}_f(\operatorname{map}_f(S)) = S$ (при инъекции f)$$

Lean4

theorem comap_map_eq_self_of_injective {f : A →ₐ[R] B} (hf : Function.Injective f) (S : Subalgebra R A) :
    (S.map f).comap f = S :=
  SetLike.coe_injective (Set.preimage_image_eq _ hf)

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