comap_top — Mathlib

English

For a nonunital algebra hom f: A →ₙₐ[R] B, the range of f equals ⊤ if and only if f is surjective.

Русский

Для неединичного гомоморфизма f: A →ₙₐ[R] B образ f равен ⊤ тогда и только тогда, когда f сюръективен.

LaTeX

$$$\operatorname{range}(f) = \top \;\iff \; \text{Surjective}(f)$$$

Lean4

@[simp]
theorem comap_top [IsScalarTower R B B] [SMulCommClass R B B] (f : A →ₙₐ[R] B) :
    (⊤ : NonUnitalSubalgebra R B).comap f = ⊤ :=
  eq_top_iff.2 fun _ => mem_top

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