comap_top — Mathlib

English

For any algebra homomorphism f: A →ₐ[R] B, the comorphism of the top subalgebra of B along f is still the top subalgebra of B.

Русский

Для любого алгебраического отображения f: A →ₐ[R] B обратная связь верхней подалгебры B по отношению к f остается верхней подалгеброй B.

LaTeX

$$$ (\\top : \\mathrm{Subalgebra} R B).comap f = \\top $$$

Lean4

@[simp]
theorem comap_top (f : A →ₐ[R] B) : (⊤ : Subalgebra R B).comap f = ⊤ :=
  eq_top_iff.2 fun _x => mem_top

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