comap_map_eq_self — Mathlib

English

If f^{-1}({0}) ⊆ S for a subalgebra S ⊆ A and f: A →ₐ[R] B, then (S.map f).comap f = S.

Русский

Если f^{-1}({0}) ⊆ S для подалгебры S ⊆ A и f: A →ₐ[R] B, то (S.map f).comap f = S.

LaTeX

$$$ (\operatorname{Subalgebra.map} f\ S)\operatorname{comap} f = S \quad\text{если } f^{-1}(\{0\}) \subseteq S. $$$

Lean4

theorem comap_map_eq_self {f : A →ₐ[R] B} {S : Subalgebra R A} (h : f ⁻¹' {0} ⊆ S) : (S.map f).comap f = S :=
  by
  convert comap_map_eq f S
  rwa [left_eq_sup, Algebra.adjoin_le_iff]

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