map — Mathlib

English

Let S1 ≤ S2 be subalgebras of A, and f: A →ₐ[R] B an algebra homomorphism. Then map f S1 ≤ map f S2.

Русский

Пусть S1 ⊆ S2 — подалгебры A и дан гомоморфизм f: A →ₐ[R] B. Тогда образ отображения map f показывает, что map f S1 ⊆ map f S2.

LaTeX

$$$S_1 \le S_2 \;\Rightarrow\; \operatorname{map}(f,S_1) \le \operatorname{map}(f,S_2)$$$

Lean4

/-- Transport a subalgebra via an algebra homomorphism. -/
@[simps! coe toSubsemiring]
def map (f : A →ₐ[R] B) (S : Subalgebra R A) : Subalgebra R B :=
  { S.toSubsemiring.map (f : A →+* B) with
    algebraMap_mem' := fun r => f.commutes r ▸ Set.mem_image_of_mem _ (S.algebraMap_mem r) }

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