map_sup — Mathlib

English

Let f be a nonunital star algebra homomorphism and S, T be nonunital star subalgebras of A. Then the image of the join equals the join of the images: (S ⊔ T).map f = S.map f ⊔ T.map f.

Русский

Пусть f — гомоморфизм неполноподобной звездной подалгебры. Тогда образ объединения равен объединению образов: (S ⊔ T).map f = S.map f ⊔ T.map f.

LaTeX

$$$(S \\sqcup T).map f = S.map f \\sqcup T.map f$$$

Lean4

theorem map_sup [IsScalarTower R B B] [SMulCommClass R B B] [StarModule R B] (f : F)
    (S T : NonUnitalStarSubalgebra R A) : ((S ⊔ T).map f : NonUnitalStarSubalgebra R B) = S.map f ⊔ T.map f :=
  (NonUnitalStarSubalgebra.gc_map_comap f).l_sup

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