isAlgebraic_algHom_iff — Mathlib

English

If f: A →ₐ[R] B is injective, then for any a ∈ A, a is algebraic over R if and only if f(a) is algebraic over R.

Русский

Если f: A →ₐ[R] B инъективен, то для любого a ∈ A абелеалгебраично над R тогда и только тогда, когда f(a) алгебраично над R.

LaTeX

$$$\forall f: A \to_R B,\; \text{Injective}(f) \Rightarrow (\IsAlgebraic(R, a) \Leftrightarrow \IsAlgebraic(R, f(a))).$$$

Lean4

theorem isAlgebraic_algHom_iff (f : A →ₐ[R] B) (hf : Function.Injective f) {a : A} :
    IsAlgebraic R (f a) ↔ IsAlgebraic R a :=
  ⟨fun ⟨p, hp0, hp⟩ ↦ ⟨p, hp0, hf <| by rwa [map_zero, ← f.comp_apply, ← aeval_algHom]⟩, IsAlgebraic.algHom f⟩

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