map — Mathlib

English

If b is integral over R, then its image under any compatible algebra homomorphism is integral over R.

Русский

Если b интегрален над R, то его образ под совместимым алгебра-гомоморфизмом также интегрален над R.

LaTeX

$$$\\text{IsIntegral}_R(b) \\Rightarrow \\text{IsIntegral}_R(f(b))$$$

Lean4

theorem map {B C F : Type*} [Ring B] [Ring C] [Algebra R B] [Algebra A B] [Algebra R C] [IsScalarTower R A B]
    [Algebra A C] [IsScalarTower R A C] {b : B} [FunLike F B C] [AlgHomClass F A B C] (f : F) (hb : IsIntegral R b) :
    IsIntegral R (f b) := by
  obtain ⟨P, hP⟩ := hb
  refine ⟨P, hP.1, ?_⟩
  rw [← aeval_def, ← aeval_map_algebraMap A, aeval_algHom_apply, aeval_map_algebraMap, aeval_def, hP.2, map_zero]

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