comap_comap — Mathlib

English

For S a StarSubalgebra of C, and g: B →⋆ₐ[R] C and f: A →⋆ₐ[R] B, the two-step preimage equals the preimage under the composition: (S.comap g).comap f = S.comap (g.comp f).

Русский

Для S ⊆ C и гомоморфизмов g, f выполняется (S.comap g).comap f = S.comap (g.comp f).

LaTeX

$$$(S.comap\\ g).comap\\ f = S.comap (g.\\circ f)$$$

Lean4

theorem comap_comap (S : StarSubalgebra R C) (g : B →⋆ₐ[R] C) (f : A →⋆ₐ[R] B) :
    (S.comap g).comap f = S.comap (g.comp f) :=
  SetLike.coe_injective <| by exact Set.preimage_preimage

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