English
If f: A →ₗ[R] B is linear and multiplicative (f(a1 a2) = f(a1) f(a2)), and x ∈ adjoin_R s, then f(x) ∈ adjoin_R (f''(s ∪ {1})).
Русский
Если f: A →ₗ[R] B линейный и умножительный (f(a1 a2) = f(a1) f(a2)) и x ∈ adjoin_R s, то f(x) ∈ adjoin_R (f''(s ∪ {1})).
LaTeX
$$$\\forall s,\\forall x\\in\\operatorname{adjoin}_R s,\\forall f:\\ A \\to_{}^{}_R B,\\ (\\forall a_1,a_2, f(a_1 a_2)=f(a_1)f(a_2)) \\Rightarrow f(x) \\in \\operatorname{adjoin}_R(f''(s\\cup\\{1\\}))$$$
Lean4
theorem mem_adjoin_of_map_mul {s} {x : A} {f : A →ₗ[R] B} (hf : ∀ a₁ a₂, f (a₁ * a₂) = f a₁ * f a₂)
(h : x ∈ adjoin R s) : f x ∈ adjoin R (f '' (s ∪ { 1 })) := by
induction h using adjoin_induction with
| mem a ha => exact subset_adjoin ⟨a, ⟨Set.subset_union_left ha, rfl⟩⟩
| algebraMap
r =>
have : f 1 ∈ adjoin R (f '' (s ∪ { 1 })) := subset_adjoin ⟨1, ⟨Set.subset_union_right <| Set.mem_singleton 1, rfl⟩⟩
convert Subalgebra.smul_mem (adjoin R (f '' (s ∪ { 1 }))) this r
rw [algebraMap_eq_smul_one]
exact f.map_smul _ _
| add y z _ _ hy hz => simpa [hy, hz] using Subalgebra.add_mem _ hy hz
| mul y z _ _ hy hz => simpa [hf, hy, hz] using Subalgebra.mul_mem _ hy hz
