adjoin_map — Mathlib

English

Let S ⊆ E and f: E →ₐ[F] E' be an F-algebra homomorphism. Then the image of the adjoin of S under f equals the adjoin of the image of S: map f (adjoin F S) = adjoin F (f'' S).

Русский

Пусть S ⊆ E и f: E →ₐ[F] E' — гомоморфизм алгебр над F. Тогда образ адъюнта S равен адъюнту образа S: map f (adjoin F S) = adjoin F (f '' S).

LaTeX

$$$(\\\\operatorname{adjoin}_F S).\\\\map f = \\\\operatorname{adjoin}_F (f '' S).$$$

Lean4

theorem adjoin_map {E' : Type*} [Field E'] [Algebra F E'] (f : E →ₐ[F] E') : (adjoin F S).map f = adjoin F (f '' S) :=
  le_antisymm (map_le_iff_le_comap.mpr <| adjoin_le_iff.mpr fun x hx ↦ subset_adjoin _ _ ⟨x, hx, rfl⟩)
    (adjoin_le_iff.mpr <| Set.monotone_image <| subset_adjoin _ _)

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