Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic

RingHom.isIntegralElem_map theorem

{x : R} : f.IsIntegralElem (f x)

Full source

theorem RingHom.isIntegralElem_map {x : R} : f.IsIntegralElem (f x) :=
  ⟨X - C x, monic_X_sub_C _, by simp⟩

Images under ring homomorphisms are integral elements

Informal description

For any element $x$ in a ring $R$, the image $f(x)$ under a ring homomorphism $f: R \to A$ is integral over $R$ with respect to $f$.

isIntegral_algebraMap theorem

{x : R} : IsIntegral R (algebraMap R A x)

Full source

theorem isIntegral_algebraMap {x : R} : IsIntegral R (algebraMap R A x) :=
  (algebraMap R A).isIntegralElem_map

Canonical Algebra Map Preserves Integrality

Informal description

For any element $x$ in a commutative ring $R$, the image of $x$ under the canonical algebra map $\text{algebraMap} \colon R \to A$ is integral over $R$.

IsIntegral.map theorem

 {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)

Full source

theorem IsIntegral.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]

Integrality is preserved under algebra homomorphisms

Informal description

Let $R$, $A$, $B$, and $C$ be rings with $R$-algebra structures, and let $F$ be a type of algebra homomorphisms from $B$ to $C$ that are $A$-linear. Suppose $b \in B$ is integral over $R$. Then for any algebra homomorphism $f \colon B \to C$ in $F$, the image $f(b)$ is integral over $R$.

isIntegral_algHom_iff theorem

(f : A →ₐ[R] B) (hf : Function.Injective f) {x : A} : IsIntegral R (f x) ↔ IsIntegral R x

Full source

theorem isIntegral_algHom_iff (f : A →ₐ[R] B) (hf : Function.Injective f) {x : A} :
    IsIntegralIsIntegral 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

Integrality Criterion via Injective Algebra Homomorphism

Informal description

Let $R$ be a commutative ring, and let $A$ and $B$ be $R$-algebras. Given an injective $R$-algebra homomorphism $f \colon A \to B$ and an element $x \in A$, the element $x$ is integral over $R$ if and only if its image $f(x)$ is integral over $R$.

Submodule.span_range_natDegree_eq_adjoin theorem

 {R A} [CommRing R] [Semiring A] [Algebra R A] {x : A} {f : R[X]} (hf : f.Monic) (hfx : aeval x f = 0) :
  span R (Finset.image (x ^ ·) (Finset.range (natDegree f))) = Subalgebra.toSubmodule (Algebra.adjoin R { x })

Full source

theorem Submodule.span_range_natDegree_eq_adjoin {R A} [CommRing R] [Semiring A] [Algebra R A]
    {x : A} {f : R[X]} (hf : f.Monic) (hfx : aeval x f = 0) :
    span R (Finset.image (x ^ ·) (Finset.range (natDegree f))) =
      Subalgebra.toSubmodule (Algebra.adjoin R {x}) := by
  nontriviality A
  have hf1 : f ≠ 1 := by rintro rfl; simp [one_ne_zero' A] at hfx
  refine (span_le.mpr fun s hs ↦ ?_).antisymm fun r hr ↦ ?_
  · rcases Finset.mem_image.1 hs with ⟨k, -, rfl⟩
    exact (Algebra.adjoin R {x}).pow_mem (Algebra.subset_adjoin rfl) k
  rw [Subalgebra.mem_toSubmodule, Algebra.adjoin_singleton_eq_range_aeval] at hr
  rcases (aeval x).mem_range.mp hr with ⟨p, rfl⟩
  rw [← modByMonic_add_div p hf, map_add, map_mul, hfx,
      zero_mul, add_zero, ← sum_C_mul_X_pow_eq (p %ₘ f), aeval_def, eval₂_sum, sum_def]
  refine sum_mem fun k hkq ↦ ?_
  rw [C_mul_X_pow_eq_monomial, eval₂_monomial, ← Algebra.smul_def]
  exact smul_mem _ _ (subset_span <| Finset.mem_image_of_mem _ <| Finset.mem_range.mpr <|
    (le_natDegree_of_mem_supp _ hkq).trans_lt <| natDegree_modByMonic_lt p hf hf1)

Span of Powers Equals Adjoint Submodule for Integral Elements

Informal description

Let $R$ be a commutative ring and $A$ a semiring with an $R$-algebra structure. Given a monic polynomial $f \in R[X]$ and an element $x \in A$ such that the evaluation of $f$ at $x$ via the algebra map is zero (i.e., $f(x) = 0$), the $R$-submodule generated by the powers $\{x^n \mid n < \deg f\}$ is equal to the submodule corresponding to the $R$-algebra generated by $x$.

IsIntegral.fg_adjoin_singleton theorem

[Algebra R B] {x : B} (hx : IsIntegral R x) : (Algebra.adjoin R { x }).toSubmodule.FG

Full source

theorem IsIntegral.fg_adjoin_singleton [Algebra R B] {x : B} (hx : IsIntegral R x) :
    (Algebra.adjoin R {x}).toSubmodule.FG := by
  classical
  rcases hx with ⟨f, hfm, hfx⟩
  use (Finset.range <| f.natDegree).image (x ^ ·)
  exact span_range_natDegree_eq_adjoin hfm (by rwa [aeval_def])

Finitely Generated Adjoint Submodule for Integral Elements

Informal description

Let $R$ be a commutative ring and $B$ an $R$-algebra. For any element $x \in B$ that is integral over $R$, the submodule corresponding to the $R$-algebra generated by $\{x\}$ is finitely generated.

RingHom.isIntegralElem_zero theorem

: f.IsIntegralElem 0

Full source

theorem RingHom.isIntegralElem_zero : f.IsIntegralElem 0 :=
  f.map_zero ▸ f.isIntegralElem_map

Integrality of Zero under Ring Homomorphism

Informal description

For any ring homomorphism $f: R \to A$, the element $0 \in A$ is integral over $R$ with respect to $f$.

isIntegral_zero theorem

[Algebra R B] : IsIntegral R (0 : B)

Full source

theorem isIntegral_zero [Algebra R B] : IsIntegral R (0 : B) :=
  (algebraMap R B).isIntegralElem_zero

Integrality of Zero in an Algebra Extension

Informal description

Let $R$ be a commutative ring and $B$ an $R$-algebra. The zero element $0 \in B$ is integral over $R$, i.e., there exists a monic polynomial $p \in R[X]$ such that $p(0) = 0$ under the algebra map $R \to B$.

RingHom.isIntegralElem_one theorem

: f.IsIntegralElem 1

Full source

theorem RingHom.isIntegralElem_one : f.IsIntegralElem 1 :=
  f.map_one ▸ f.isIntegralElem_map

Integrality of One under Ring Homomorphism

Informal description

For any ring homomorphism $f: R \to A$, the element $1 \in A$ is integral over $R$ with respect to $f$.

isIntegral_one theorem

[Algebra R B] : IsIntegral R (1 : B)

Full source

theorem isIntegral_one [Algebra R B] : IsIntegral R (1 : B) :=
  (algebraMap R B).isIntegralElem_one

Integrality of One in an Algebra Extension

Informal description

Let $R$ be a commutative ring and $B$ an $R$-algebra. The multiplicative identity element $1 \in B$ is integral over $R$, i.e., there exists a monic polynomial $p \in R[X]$ such that $p(1) = 0$ under the algebra map $R \to B$.

IsIntegral.of_pow theorem

[Algebra R B] {x : B} {n : ℕ} (hn : 0 < n) (hx : IsIntegral R <| x ^ n) : IsIntegral R x

Full source

theorem IsIntegral.of_pow [Algebra R B] {x : B} {n : ℕ} (hn : 0 < n) (hx : IsIntegral R <| x ^ n) :
    IsIntegral R x :=
  have ⟨p, hmonic, heval⟩ := hx
  ⟨expand R n p, hmonic.expand hn, by rwa [← aeval_def, expand_aeval]⟩

Integrality of Root Implies Integrality of Element

Informal description

Let $R$ be a commutative ring and $B$ an $R$-algebra. For any element $x \in B$ and positive integer $n$, if $x^n$ is integral over $R$, then $x$ is integral over $R$.

IsIntegral.of_aeval_monic theorem

{x : A} {p : R[X]} (monic : p.Monic) (deg : p.natDegree ≠ 0) (hx : IsIntegral R (aeval x p)) : IsIntegral R x

Full source

theorem IsIntegral.of_aeval_monic {x : A} {p : R[X]} (monic : p.Monic)
    (deg : p.natDegree ≠ 0) (hx : IsIntegral R (aeval x p)) : IsIntegral R x :=
  have ⟨p, hmonic, heval⟩ := hx
  ⟨_, hmonic.comp monic deg, by rwa [eval₂_comp, ← aeval_def x]⟩

Integrality of Evaluation Implies Integrality of Element for Monic Polynomials

Informal description

Let $R$ be a commutative ring and $A$ an $R$-algebra. For any element $x \in A$ and monic polynomial $p \in R[X]$ with nonzero degree, if the evaluation of $p$ at $x$ (via the algebra map) is integral over $R$, then $x$ itself is integral over $R$.

IsIntegral.map_of_comp_eq theorem

 {R S T U : Type*} [CommRing R] [Ring S] [CommRing T] [Ring U] [Algebra R S] [Algebra T U] (φ : R →+* T) (ψ : S →+* U)
  (h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)) {a : S} (ha : IsIntegral R a) : IsIntegral T (ψ a)

Full source

theorem IsIntegral.map_of_comp_eq {R S T U : Type*} [CommRing R] [Ring S]
    [CommRing T] [Ring U] [Algebra R S] [Algebra T U] (φ : R →+* T) (ψ : S →+* U)
    (h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)) {a : S} (ha : IsIntegral R a) :
    IsIntegral T (ψ a) :=
  let ⟨p, hp⟩ := ha
  ⟨p.map φ, hp.1.map _, by
    rw [← eval_map, map_map, h, ← map_map, eval_map, eval₂_at_apply, eval_map, hp.2, ψ.map_zero]⟩

Integrality Preservation Under Ring Homomorphisms with Commuting Diagram

Informal description

Let $R$, $S$, $T$, and $U$ be commutative rings with $S$ and $U$ being $R$-algebra and $T$-algebra respectively. Given ring homomorphisms $\varphi: R \to T$ and $\psi: S \to U$ such that the diagram \[ \begin{tikzcd} R \arrow[r, "\varphi"] \arrow[d, "\text{algebraMap}"] & T \arrow[d, "\text{algebraMap}"] \\ S \arrow[r, "\psi"] & U \end{tikzcd} \] commutes, then for any element $a \in S$ that is integral over $R$, its image $\psi(a) \in U$ is integral over $T$.

isIntegral_algEquiv theorem

 {A B : Type*} [Ring A] [Ring B] [Algebra R A] [Algebra R B] (f : A ≃ₐ[R] B) {x : A} :
  IsIntegral R (f x) ↔ IsIntegral R x

Full source

@[simp]
theorem isIntegral_algEquiv {A B : Type*} [Ring A] [Ring B] [Algebra R A] [Algebra R B]
    (f : A ≃ₐ[R] B) {x : A} : IsIntegralIsIntegral R (f x) ↔ IsIntegral R x :=
  ⟨fun h ↦ by simpa using h.map f.symm, IsIntegral.map f⟩

Integrality is preserved under $R$-algebra isomorphisms

Informal description

Let $R$ be a commutative ring, and let $A$ and $B$ be $R$-algebras. Given an $R$-algebra isomorphism $f \colon A \to B$ and an element $x \in A$, the element $f(x) \in B$ is integral over $R$ if and only if $x$ is integral over $R$.

IsIntegral.tower_top theorem

[Algebra A B] [IsScalarTower R A B] {x : B} (hx : IsIntegral R x) : IsIntegral A x

Full source

/-- If `R → A → B` is an algebra tower,
then if the entire tower is an integral extension so is `A → B`. -/
theorem IsIntegral.tower_top [Algebra A B] [IsScalarTower R A B] {x : B}
    (hx : IsIntegral R x) : IsIntegral A x :=
  let ⟨p, hp, hpx⟩ := hx
  ⟨p.map <| algebraMap R A, hp.map _, by rw [← aeval_def, aeval_map_algebraMap, aeval_def, hpx]⟩

Integrality in Tower: $R \to A \to B$ Implies Integrality over Intermediate Ring

Informal description

Let $R \to A \to B$ be an algebra tower (i.e., $B$ is an $A$-algebra and $A$ is an $R$-algebra, with compatible scalar multiplication). If an element $x \in B$ is integral over $R$, then it is also integral over $A$.

RingEquiv.isIntegral_iff theorem

 {R S T : Type*} [CommRing R] [Ring S] [CommRing T] [Algebra R S] [Algebra T S] (φ : R ≃+* T)
  (h : (algebraMap T S).comp φ.toRingHom = algebraMap R S) (a : S) : IsIntegral R a ↔ IsIntegral T a

Full source

theorem RingEquiv.isIntegral_iff {R S T : Type*} [CommRing R] [Ring S] [CommRing T]
    [Algebra R S] [Algebra T S] (φ : R ≃+* T)
    (h : (algebraMap T S).comp φ.toRingHom = algebraMap R S) (a : S) :
    IsIntegralIsIntegral R a ↔ IsIntegral T a := by
  constructor <;> intro ha
  · letI : Algebra R T := φ.toRingHom.toAlgebra
    letI : IsScalarTower R T S :=
      ⟨fun r t s ↦ by simp only [Algebra.smul_def, map_mul, ← h, mul_assoc]; rfl⟩
    exact IsIntegral.tower_top ha
  · have h' : (algebraMap T S) = (algebraMap R S).comp φ.symm.toRingHom := by
      simp only [← h, RingHom.comp_assoc, RingEquiv.toRingHom_eq_coe, RingEquiv.comp_symm,
        RingHomCompTriple.comp_eq]
    letI : Algebra T R := φ.symm.toRingHom.toAlgebra
    letI : IsScalarTower T R S :=
      ⟨fun r t s ↦ by simp only [Algebra.smul_def, map_mul, h', mul_assoc]; rfl⟩
    exact IsIntegral.tower_top ha

Integrality Equivalence under Ring Isomorphism

Informal description

Let $R$, $S$, and $T$ be commutative rings with $S$ being an $R$-algebra and a $T$-algebra. Given a ring isomorphism $\varphi \colon R \to T$ such that the algebra maps satisfy $(\text{algebraMap}\, T\, S) \circ \varphi = \text{algebraMap}\, R\, S$, then for any element $a \in S$, $a$ is integral over $R$ if and only if $a$ is integral over $T$.

map_isIntegral_int theorem

 {B C F : Type*} [Ring B] [Ring C] {b : B} [FunLike F B C] [RingHomClass F B C] (f : F) (hb : IsIntegral ℤ b) :
  IsIntegral ℤ (f b)

Full source

theorem map_isIntegral_int {B C F : Type*} [Ring B] [Ring C] {b : B}
    [FunLike F B C] [RingHomClass F B C] (f : F)
    (hb : IsIntegral ℤ b) : IsIntegral ℤ (f b) :=
  hb.map (f : B →+* C).toIntAlgHom

Integrality over $\mathbb{Z}$ is preserved under ring homomorphisms

Informal description

Let $B$ and $C$ be rings, and let $F$ be a type of ring homomorphisms from $B$ to $C$. For any element $b \in B$ that is integral over $\mathbb{Z}$ and any ring homomorphism $f \colon B \to C$ in $F$, the image $f(b)$ is integral over $\mathbb{Z}$.

IsIntegral.of_subring theorem

{x : B} (T : Subring R) (hx : IsIntegral T x) : IsIntegral R x

Full source

theorem IsIntegral.of_subring {x : B} (T : Subring R) (hx : IsIntegral T x) : IsIntegral R x :=
  hx.tower_top

Integrality over subring implies integrality over base ring

Informal description

Let $R$ be a commutative ring and $B$ an $R$-algebra. For any subring $T$ of $R$ and any element $x \in B$, if $x$ is integral over $T$, then $x$ is integral over $R$.

IsIntegral.algebraMap theorem

[Algebra A B] [IsScalarTower R A B] {x : A} (h : IsIntegral R x) : IsIntegral R (algebraMap A B x)

Full source

protected theorem IsIntegral.algebraMap [Algebra A B] [IsScalarTower R A B] {x : A}
    (h : IsIntegral R x) : IsIntegral R (algebraMap A B x) := by
  rcases h with ⟨f, hf, hx⟩
  use f, hf
  rw [IsScalarTower.algebraMap_eq R A B, ← hom_eval₂, hx, RingHom.map_zero]

Integrality is preserved under algebra maps in a tower

Informal description

Let $R$, $A$, and $B$ be commutative rings with $R \to A \to B$ forming a tower of algebra maps. If an element $x \in A$ is integral over $R$, then its image under the algebra map $A \to B$ is also integral over $R$.

isIntegral_algebraMap_iff theorem

 [Algebra A B] [IsScalarTower R A B] {x : A} (hAB : Function.Injective (algebraMap A B)) :
  IsIntegral R (algebraMap A B x) ↔ IsIntegral R x

Full source

theorem isIntegral_algebraMap_iff [Algebra A B] [IsScalarTower R A B] {x : A}
    (hAB : Function.Injective (algebraMap A B)) :
    IsIntegralIsIntegral R (algebraMap A B x) ↔ IsIntegral R x :=
  isIntegral_algHom_iff (IsScalarTower.toAlgHom R A B) hAB

Integrality Criterion via Injective Algebra Map in Tower

Informal description

Let $R$, $A$, and $B$ be commutative rings with algebra maps forming a tower $R \to A \to B$. Suppose the algebra map $\text{algebraMap} \colon A \to B$ is injective. Then for any element $x \in A$, the image $\text{algebraMap}(x) \in B$ is integral over $R$ if and only if $x$ is integral over $R$.

isIntegral_iff_isIntegral_closure_finite theorem

{r : B} : IsIntegral R r ↔ ∃ s : Set R, s.Finite ∧ IsIntegral (Subring.closure s) r

Full source

theorem isIntegral_iff_isIntegral_closure_finite {r : B} :
    IsIntegralIsIntegral R r ↔ ∃ s : Set R, s.Finite ∧ IsIntegral (Subring.closure s) r := by
  constructor <;> intro hr
  · rcases hr with ⟨p, hmp, hpr⟩
    refine ⟨_, Finset.finite_toSet _, p.restriction, monic_restriction.2 hmp, ?_⟩
    rw [← aeval_def, ← aeval_map_algebraMap R r p.restriction, map_restriction, aeval_def, hpr]
  rcases hr with ⟨s, _, hsr⟩
  exact hsr.of_subring _

Integrality Criterion via Finite Subring Generation

Informal description

An element $r$ in an $R$-algebra $B$ is integral over $R$ if and only if there exists a finite subset $s \subseteq R$ such that $r$ is integral over the subring generated by $s$.

fg_adjoin_of_finite theorem

{s : Set A} (hfs : s.Finite) (his : ∀ x ∈ s, IsIntegral R x) : (Algebra.adjoin R s).toSubmodule.FG

Full source

@[stacks 09GH]
theorem fg_adjoin_of_finite {s : Set A} (hfs : s.Finite) (his : ∀ x ∈ s, IsIntegral R x) :
    (Algebra.adjoin R s).toSubmodule.FG := by
  induction s, hfs using Set.Finite.induction_on with
  | empty =>
    refine ⟨{1}, Submodule.ext fun x => ?_⟩
    rw [Algebra.adjoin_empty, Finset.coe_singleton, ← one_eq_span, Algebra.toSubmodule_bot]
  | @insert a s _ _ ih =>
    rw [← Set.union_singleton, Algebra.adjoin_union_coe_submodule]
    exact FG.mul
      (ih fun i hi => his i <| Set.mem_insert_of_mem a hi)
      (his a <| Set.mem_insert a s).fg_adjoin_singleton

Finitely Generated Adjoint Submodule for Finite Sets of Integral Elements

Informal description

For any finite subset $s$ of an $R$-algebra $A$ where every element of $s$ is integral over $R$, the submodule corresponding to the $R$-algebra generated by $s$ is finitely generated.

Algebra.finite_adjoin_of_finite_of_isIntegral theorem

{s : Set A} (hf : s.Finite) (hi : ∀ x ∈ s, IsIntegral R x) : Module.Finite R (adjoin R s)

Full source

theorem Algebra.finite_adjoin_of_finite_of_isIntegral {s : Set A} (hf : s.Finite)
    (hi : ∀ x ∈ s, IsIntegral R x) : Module.Finite R (adjoin R s) :=
  Module.Finite.iff_fg.mpr <| fg_adjoin_of_finite hf hi

Finite Generation of Adjoint Algebra for Finite Sets of Integral Elements

Informal description

For any finite subset $s$ of an $R$-algebra $A$ where every element of $s$ is integral over $R$, the $R$-algebra generated by $s$ is finitely generated as an $R$-module.

Algebra.finite_adjoin_simple_of_isIntegral theorem

{x : A} (hi : IsIntegral R x) : Module.Finite R (adjoin R { x })

Full source

theorem Algebra.finite_adjoin_simple_of_isIntegral {x : A} (hi : IsIntegral R x) :
    Module.Finite R (adjoin R {x}) :=
  Module.Finite.iff_fg.mpr hi.fg_adjoin_singleton

Finite Generation of Adjoint Algebra for Integral Elements

Informal description

Let $R$ be a commutative ring and $A$ an $R$-algebra. For any element $x \in A$ that is integral over $R$, the $R$-algebra generated by $\{x\}$ is finitely generated as an $R$-module.

isNoetherian_adjoin_finset theorem

[IsNoetherianRing R] (s : Finset A) (hs : ∀ x ∈ s, IsIntegral R x) : IsNoetherian R (Algebra.adjoin R (s : Set A))

Full source

theorem isNoetherian_adjoin_finset [IsNoetherianRing R] (s : Finset A)
    (hs : ∀ x ∈ s, IsIntegral R x) : IsNoetherian R (Algebra.adjoin R (s : Set A)) :=
  isNoetherian_of_fg_of_noetherian _ (fg_adjoin_of_finite s.finite_toSet hs)

Noetherian Property of Adjoint Algebra for Finite Sets of Integral Elements

Informal description

Let $R$ be a Noetherian ring and $A$ an $R$-algebra. For any finite subset $s$ of $A$ where every element of $s$ is integral over $R$, the $R$-algebra generated by $s$ is a Noetherian $R$-module.

IsIntegral.pair theorem

{x : A × B} (hx₁ : IsIntegral R x.1) (hx₂ : IsIntegral R x.2) : IsIntegral R x

Full source

/-- An element of a product algebra is integral if each component is integral. -/
theorem IsIntegral.pair {x : A × B} (hx₁ : IsIntegral R x.1) (hx₂ : IsIntegral R x.2) :
    IsIntegral R x := by
  obtain ⟨p₁, ⟨hp₁Monic, hp₁Eval⟩⟩ := hx₁
  obtain ⟨p₂, ⟨hp₂Monic, hp₂Eval⟩⟩ := hx₂
  refine ⟨p₁ * p₂, ⟨hp₁Monic.mul hp₂Monic, ?_⟩⟩
  rw [← aeval_def] at *
  rw [aeval_prod_apply, aeval_mul, hp₁Eval, zero_mul, aeval_mul, hp₂Eval, mul_zero,
    Prod.zero_eq_mk]

Integrality of Product Algebra Elements

Informal description

Let $R$ be a commutative ring and $A$, $B$ be $R$-algebras. For any element $x = (x_1, x_2)$ in the product algebra $A \times B$, if $x_1$ is integral over $R$ and $x_2$ is integral over $R$, then $x$ is integral over $R$.

IsIntegral.pair_iff theorem

{x : A × B} : IsIntegral R x ↔ IsIntegral R x.1 ∧ IsIntegral R x.2

Full source

/-- An element of a product algebra is integral iff each component is integral. -/
theorem IsIntegral.pair_iff {x : A × B} : IsIntegralIsIntegral R x ↔ IsIntegral R x.1 ∧ IsIntegral R x.2 :=
  ⟨fun h ↦ ⟨h.map (AlgHom.fst R A B), h.map (AlgHom.snd R A B)⟩, fun h ↦ h.1.pair h.2⟩

Integrality in Product Algebra Components

Informal description

An element $x = (x_1, x_2)$ in the product algebra $A \times B$ is integral over $R$ if and only if both components $x_1$ and $x_2$ are integral over $R$.