isIntegral_algHom_iff — Mathlib

English

For an injective algebra homomorphism f: A → B, IsIntegral R (f x) iff IsIntegral R x for all x ∈ A.

Русский

Для инъективного алгебра-гомоморфизма f: A → B выполняется: IsIntegral R (f(x)) эквивалентно IsIntegral R (x) для всех x ∈ A.

LaTeX

$$$\\text{IsIntegral}_R(f(x)) \\iff \\text{IsIntegral}_R(x)$$$

Lean4

theorem isIntegral_algHom_iff (f : A →ₐ[R] B) (hf : Function.Injective f) {x : A} :
    IsIntegral R (f x) ↔ IsIntegral R x :=
  by
  refine ⟨fun ⟨p, hp, hx⟩ ↦ ⟨p, hp, ?_⟩, IsIntegral.map f⟩
  rwa [← f.comp_algebraMap, ← AlgHom.coe_toRingHom, ← hom_eval₂, AlgHom.coe_toRingHom, map_eq_zero_iff f hf] at hx

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