Mathlib.RingTheory.IntegralClosure.Algebra.Basic

Subalgebra.isIntegral_iff theorem

(S : Subalgebra R A) : Algebra.IsIntegral R S ↔ ∀ x ∈ S, IsIntegral R x

Full source

theorem Subalgebra.isIntegral_iff (S : Subalgebra R A) :
    Algebra.IsIntegralAlgebra.IsIntegral R S ↔ ∀ x ∈ S, IsIntegral R x :=
  Algebra.isIntegral_def.trans <| .trans
    (forall_congr' fun _ ↦ (isIntegral_algHom_iff S.val Subtype.val_injective).symm) Subtype.forall

Characterization of Integral Subalgebras: $S$ is integral over $R$ iff all elements of $S$ are integral over $R$

Informal description

For any subalgebra $S$ of an $R$-algebra $A$, the algebra $S$ is integral over $R$ if and only if every element $x \in S$ is integral over $R$.

Algebra.IsIntegral.of_injective theorem

(f : A →ₐ[R] B) (hf : Function.Injective f) [Algebra.IsIntegral R B] : Algebra.IsIntegral R A

Full source

theorem Algebra.IsIntegral.of_injective (f : A →ₐ[R] B) (hf : Function.Injective f)
    [Algebra.IsIntegral R B] : Algebra.IsIntegral R A :=
  ⟨fun _ ↦ (isIntegral_algHom_iff f hf).mp (isIntegral _)⟩

Inheritance of Integrality via Injective Algebra Homomorphism

Informal description

Let $A$ and $B$ be $R$-algebras, and let $f: A \to B$ be an injective $R$-algebra homomorphism. If $B$ is integral over $R$, then $A$ is also integral over $R$.

Algebra.IsIntegral.of_surjective theorem

[Algebra.IsIntegral R A] (f : A →ₐ[R] B) (hf : Function.Surjective f) : Algebra.IsIntegral R B

Full source

/-- Homomorphic image of an integral algebra is an integral algebra. -/
theorem Algebra.IsIntegral.of_surjective [Algebra.IsIntegral R A]
    (f : A →ₐ[R] B) (hf : Function.Surjective f) : Algebra.IsIntegral R B :=
  isIntegral_def.mpr fun b ↦ let ⟨a, ha⟩ := hf b; ha ▸ (isIntegral_def.mp ‹_› a).map f

Integrality is Preserved Under Surjective Algebra Homomorphism

Informal description

Let $A$ and $B$ be $R$-algebras, and let $f: A \to B$ be a surjective $R$-algebra homomorphism. If $A$ is integral over $R$, then $B$ is also integral over $R$.

AlgEquiv.isIntegral_iff theorem

(e : A ≃ₐ[R] B) : Algebra.IsIntegral R A ↔ Algebra.IsIntegral R B

Full source

theorem AlgEquiv.isIntegral_iff (e : A ≃ₐ[R] B) : Algebra.IsIntegralAlgebra.IsIntegral R A ↔ Algebra.IsIntegral R B :=
  ⟨fun h ↦ h.of_injective e.symm e.symm.injective, fun h ↦ h.of_injective e e.injective⟩

Integrality is Preserved Under Algebra Isomorphism

Informal description

Let $A$ and $B$ be $R$-algebras, and let $e: A \simeq B$ be an $R$-algebra isomorphism. Then $A$ is integral over $R$ if and only if $B$ is integral over $R$.

Module.End.isIntegral instance

{M : Type*} [AddCommGroup M] [Module R M] [Module.Finite R M] : Algebra.IsIntegral R (Module.End R M)

Full source

instance Module.End.isIntegral {M : Type*} [AddCommGroup M] [Module R M] [Module.Finite R M] :
    Algebra.IsIntegral R (Module.End R M) :=
  ⟨LinearMap.exists_monic_and_aeval_eq_zero R⟩

Integrality of Endomorphism Algebra for Finite Modules

Informal description

For any commutative ring $R$ and finite $R$-module $M$, the $R$-algebra of $R$-linear endomorphisms of $M$ is integral over $R$. That is, every endomorphism $f \in \text{End}_R(M)$ satisfies a monic polynomial equation with coefficients in $R$.

IsIntegral.of_finite theorem

[Module.Finite R B] (x : B) : IsIntegral R x

Full source

@[nontriviality]
theorem IsIntegral.of_finite [Module.Finite R B] (x : B) : IsIntegral R x :=
  (isIntegral_algHom_iff (Algebra.lmul R B) Algebra.lmul_injective).mp
    (Algebra.IsIntegral.isIntegral _)

Finite Module Elements are Integral Over Base Ring

Informal description

Let $R$ be a commutative ring and $B$ be an $R$-algebra that is finite as an $R$-module. Then every element $x \in B$ is integral over $R$, meaning there exists a monic polynomial with coefficients in $R$ that annihilates $x$.

isIntegral_of_noetherian theorem

(_ : IsNoetherian R B) (x : B) : IsIntegral R x

Full source

theorem isIntegral_of_noetherian (_ : IsNoetherian R B) (x : B) : IsIntegral R x :=
  .of_finite R x

Noetherian Module Elements are Integral Over Base Ring

Informal description

Let $R$ be a commutative ring and $B$ be an $R$-algebra that is Noetherian as an $R$-module. Then every element $x \in B$ is integral over $R$, meaning there exists a monic polynomial with coefficients in $R$ that annihilates $x$.

Algebra.IsIntegral.of_finite instance

[Module.Finite R B] : Algebra.IsIntegral R B

Full source

instance Algebra.IsIntegral.of_finite [Module.Finite R B] : Algebra.IsIntegral R B :=
  ⟨.of_finite R⟩

Finite Algebras are Integral Over Their Base Ring

Informal description

If an $R$-algebra $B$ is finite as an $R$-module, then every element of $B$ is integral over $R$.

IsIntegral.of_mem_of_fg theorem

(S : Subalgebra R B) (HS : S.toSubmodule.FG) (x : B) (hx : x ∈ S) : IsIntegral R x

Full source

/-- If `S` is a sub-`R`-algebra of `A` and `S` is finitely-generated as an `R`-module,
  then all elements of `S` are integral over `R`. -/
theorem IsIntegral.of_mem_of_fg (S : Subalgebra R B)
    (HS : S.toSubmodule.FG) (x : B) (hx : x ∈ S) : IsIntegral R x :=
  have : Module.Finite R S := ⟨(fg_top _).mpr HS⟩
  (isIntegral_algHom_iff S.val Subtype.val_injective).mpr (.of_finite R (⟨x, hx⟩ : S))

Integrality of Elements in Finitely Generated Subalgebras

Informal description

Let $R$ be a commutative ring and $B$ an $R$-algebra. For any subalgebra $S \subseteq B$ that is finitely generated as an $R$-module, every element $x \in S$ is integral over $R$.

isIntegral_of_submodule_noetherian theorem

(S : Subalgebra R B) (H : IsNoetherian R (Subalgebra.toSubmodule S)) (x : B) (hx : x ∈ S) : IsIntegral R x

Full source

theorem isIntegral_of_submodule_noetherian (S : Subalgebra R B)
    (H : IsNoetherian R (Subalgebra.toSubmodule S)) (x : B) (hx : x ∈ S) : IsIntegral R x :=
  .of_mem_of_fg _ ((fg_top _).mp <| H.noetherian _) _ hx

Integrality of Elements in Noetherian Subalgebras

Informal description

Let $R$ be a commutative ring and $B$ an $R$-algebra. For any subalgebra $S \subseteq B$ such that $S$ is finitely generated as an $R$-module (i.e., $S$ is Noetherian as an $R$-module), every element $x \in S$ is integral over $R$.

isIntegral_of_smul_mem_submodule theorem

 {M : Type*} [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M] [NoZeroSMulDivisors A M]
  (N : Submodule R M) (hN : N ≠ ⊥) (hN' : N.FG) (x : A) (hx : ∀ n ∈ N, x • n ∈ N) : IsIntegral R x

Full source

/-- Suppose `A` is an `R`-algebra, `M` is an `A`-module such that `a • m ≠ 0` for all non-zero `a`
and `m`. If `x : A` fixes a nontrivial f.g. `R`-submodule `N` of `M`, then `x` is `R`-integral. -/
theorem isIntegral_of_smul_mem_submodule {M : Type*} [AddCommGroup M] [Module R M] [Module A M]
    [IsScalarTower R A M] [NoZeroSMulDivisors A M] (N : Submodule R M) (hN : N ≠ ⊥) (hN' : N.FG)
    (x : A) (hx : ∀ n ∈ N, x • n ∈ N) : IsIntegral R x := by
  let A' : Subalgebra R A :=
    { carrier := { x | ∀ n ∈ N, x • n ∈ N }
      mul_mem' := fun {a b} ha hb n hn => smul_smul a b n ▸ ha _ (hb _ hn)
      one_mem' := fun n hn => (one_smul A n).symm ▸ hn
      add_mem' := fun {a b} ha hb n hn => (add_smul a b n).symm ▸ N.add_mem (ha _ hn) (hb _ hn)
      zero_mem' := fun n _hn => (zero_smul A n).symm ▸ N.zero_mem
      algebraMap_mem' := fun r n hn => (algebraMap_smul A r n).symm ▸ N.smul_mem r hn }
  let f : A' →ₐ[R] Module.End R N :=
    AlgHom.ofLinearMap
      { toFun := fun x => (DistribMulAction.toLinearMap R M x).restrict x.prop
        -- Porting note: was
                -- `fun x y => LinearMap.ext fun n => Subtype.ext <| add_smul x y n`
        map_add' := by intros x y; ext; exact add_smul _ _ _
        -- Porting note: was
                --  `fun r s => LinearMap.ext fun n => Subtype.ext <| smul_assoc r s n`
        map_smul' := by intros r s; ext; apply smul_assoc }
      -- Porting note: the next two lines were
      --`(LinearMap.ext fun n => Subtype.ext <| one_smul _ _) fun x y =>`
      --`LinearMap.ext fun n => Subtype.ext <| mul_smul x y n`
      (by ext; apply one_smul)
      (by intros x y; ext; apply mul_smul)
  obtain ⟨a, ha₁, ha₂⟩ : ∃ a ∈ N, a ≠ (0 : M) := by
    by_contra! h'
    apply hN
    rwa [eq_bot_iff]
  have : Function.Injective f := by
    show Function.Injective f.toLinearMap
    rw [← LinearMap.ker_eq_bot, eq_bot_iff]
    intro s hs
    have : s.1 • a = 0 := congr_arg Subtype.val (LinearMap.congr_fun hs ⟨a, ha₁⟩)
    exact Subtype.ext ((eq_zero_or_eq_zero_of_smul_eq_zero this).resolve_right ha₂)
  show IsIntegral R (A'.val ⟨x, hx⟩)
  rw [isIntegral_algHom_iff A'.val Subtype.val_injective, ← isIntegral_algHom_iff f this]
  haveI : Module.Finite R N := by rwa [Module.finite_def, Submodule.fg_top]
  apply Algebra.IsIntegral.isIntegral

Integrality via Submodule Stabilization

Informal description

Let $R$ be a commutative ring, $A$ an $R$-algebra, and $M$ an $A$-module with no zero divisors (i.e., $a \cdot m \neq 0$ for all nonzero $a \in A$ and $m \in M$). Suppose $N$ is a nontrivial finitely generated $R$-submodule of $M$ and $x \in A$ satisfies $x \cdot n \in N$ for all $n \in N$. Then $x$ is integral over $R$.

RingHom.Finite.to_isIntegral theorem

(h : f.Finite) : f.IsIntegral

Full source

@[stacks 00GK]
theorem RingHom.Finite.to_isIntegral (h : f.Finite) : f.IsIntegral :=
  letI := f.toAlgebra
  fun _ ↦ IsIntegral.of_mem_of_fg ⊤ h.1 _ trivial

Finite Ring Homomorphisms are Integral

Informal description

If a ring homomorphism $f \colon R \to S$ is finite (i.e., $S$ is finitely generated as an $R$-module via $f$), then $f$ is integral (i.e., every element of $S$ is integral over $R$ via $f$).

RingHom.IsIntegralElem.of_mem_closure theorem

 {x y z : S} (hx : f.IsIntegralElem x) (hy : f.IsIntegralElem y) (hz : z ∈ Subring.closure ({ x, y } : Set S)) :
  f.IsIntegralElem z

Full source

theorem RingHom.IsIntegralElem.of_mem_closure {x y z : S} (hx : f.IsIntegralElem x)
    (hy : f.IsIntegralElem y) (hz : z ∈ Subring.closure ({x, y} : Set S)) : f.IsIntegralElem z := by
  letI : Algebra R S := f.toAlgebra
  have := (IsIntegral.fg_adjoin_singleton hx).mul (IsIntegral.fg_adjoin_singleton hy)
  rw [← Algebra.adjoin_union_coe_submodule, Set.singleton_union] at this
  exact
    IsIntegral.of_mem_of_fg (Algebra.adjoin R {x, y}) this z
      (Algebra.mem_adjoin_iff.2 <| Subring.closure_mono Set.subset_union_right hz)

Integrality is preserved under subring generation by integral elements

Informal description

Let $R$ and $S$ be commutative rings, and let $f : R \to S$ be a ring homomorphism. For any elements $x, y \in S$ that are integral over $R$ via $f$, any element $z$ in the subring generated by $\{x, y\}$ is also integral over $R$ via $f$.

IsIntegral.of_mem_closure theorem

 {x y z : A} (hx : IsIntegral R x) (hy : IsIntegral R y) (hz : z ∈ Subring.closure ({ x, y } : Set A)) : IsIntegral R z

Full source

nonrec theorem IsIntegral.of_mem_closure {x y z : A} (hx : IsIntegral R x) (hy : IsIntegral R y)
    (hz : z ∈ Subring.closure ({x, y} : Set A)) : IsIntegral R z :=
  hx.of_mem_closure (algebraMap R A) hy hz

Integrality is preserved under subring generation by integral elements in an $R$-algebra

Informal description

Let $R$ be a commutative ring and $A$ an $R$-algebra. For any elements $x, y \in A$ that are integral over $R$, any element $z$ in the subring generated by $\{x, y\}$ is also integral over $R$.

RingHom.IsIntegralElem.add theorem

(f : R →+* S) {x y : S} (hx : f.IsIntegralElem x) (hy : f.IsIntegralElem y) : f.IsIntegralElem (x + y)

Full source

theorem RingHom.IsIntegralElem.add (f : R →+* S) {x y : S}
    (hx : f.IsIntegralElem x) (hy : f.IsIntegralElem y) :
    f.IsIntegralElem (x + y) :=
  hx.of_mem_closure f hy <|
    Subring.add_mem _ (Subring.subset_closure (Or.inl rfl)) (Subring.subset_closure (Or.inr rfl))

Sum of Integral Elements is Integral

Informal description

Let $R$ and $S$ be commutative rings, and let $f : R \to S$ be a ring homomorphism. For any elements $x, y \in S$ that are integral over $R$ via $f$, their sum $x + y$ is also integral over $R$ via $f$.

IsIntegral.add theorem

{x y : A} (hx : IsIntegral R x) (hy : IsIntegral R y) : IsIntegral R (x + y)

Full source

nonrec theorem IsIntegral.add {x y : A} (hx : IsIntegral R x) (hy : IsIntegral R y) :
    IsIntegral R (x + y) :=
  hx.add (algebraMap R A) hy

Sum of Integral Elements is Integral over $R$

Informal description

Let $R$ be a commutative ring and $A$ an $R$-algebra. For any elements $x, y \in A$ that are integral over $R$, their sum $x + y$ is also integral over $R$.

RingHom.IsIntegralElem.neg theorem

{x : S} (hx : f.IsIntegralElem x) : f.IsIntegralElem (-x)

Full source

theorem RingHom.IsIntegralElem.neg {x : S} (hx : f.IsIntegralElem x) : f.IsIntegralElem (-x) :=
  hx.of_mem_closure f hx (Subring.neg_mem _ (Subring.subset_closure (Or.inl rfl)))

Integrality is preserved under negation

Informal description

Let $R$ and $S$ be commutative rings, and let $f : R \to S$ be a ring homomorphism. For any element $x \in S$ that is integral over $R$ via $f$, its additive inverse $-x$ is also integral over $R$ via $f$.

RingHom.IsIntegralElem.of_neg theorem

{x : S} (h : f.IsIntegralElem (-x)) : f.IsIntegralElem x

Full source

theorem RingHom.IsIntegralElem.of_neg {x : S} (h : f.IsIntegralElem (-x)) : f.IsIntegralElem x :=
  neg_neg x ▸ h.neg

Integrality of an element implies integrality of its negation

Informal description

Let $R$ and $S$ be commutative rings, and let $f : R \to S$ be a ring homomorphism. For any element $x \in S$, if $-x$ is integral over $R$ via $f$, then $x$ is also integral over $R$ via $f$.

RingHom.IsIntegralElem.neg_iff theorem

{x : S} : f.IsIntegralElem (-x) ↔ f.IsIntegralElem x

Full source

@[simp]
theorem RingHom.IsIntegralElem.neg_iff {x : S} : f.IsIntegralElem (-x) ↔ f.IsIntegralElem x :=
  ⟨fun h => h.of_neg, fun h => h.neg⟩

Integrality of an Element is Equivalent to Integrality of its Negation

Informal description

Let $R$ and $S$ be commutative rings, and let $f : R \to S$ be a ring homomorphism. For any element $x \in S$, $-x$ is integral over $R$ via $f$ if and only if $x$ is integral over $R$ via $f$.

IsIntegral.neg theorem

{x : B} (hx : IsIntegral R x) : IsIntegral R (-x)

Full source

theorem IsIntegral.neg {x : B} (hx : IsIntegral R x) : IsIntegral R (-x) :=
  .of_mem_of_fg _ hx.fg_adjoin_singleton _ (Subalgebra.neg_mem _ <| Algebra.subset_adjoin rfl)

Integrality is preserved under negation

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 negation $-x$ is also integral over $R$.

IsIntegral.of_neg theorem

{x : B} (hx : IsIntegral R (-x)) : IsIntegral R x

Full source

theorem IsIntegral.of_neg {x : B} (hx : IsIntegral R (-x)) : IsIntegral R x :=
  neg_neg x ▸ hx.neg

Integrality of $x$ from integrality of $-x$

Informal description

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

IsIntegral.neg_iff theorem

{x : B} : IsIntegral R (-x) ↔ IsIntegral R x

Full source

@[simp]
theorem IsIntegral.neg_iff {x : B} : IsIntegralIsIntegral R (-x) ↔ IsIntegral R x :=
  ⟨IsIntegral.of_neg, IsIntegral.neg⟩

Integrality of $x$ is equivalent to integrality of $-x$

Informal description

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

RingHom.IsIntegralElem.sub theorem

{x y : S} (hx : f.IsIntegralElem x) (hy : f.IsIntegralElem y) : f.IsIntegralElem (x - y)

Full source

theorem RingHom.IsIntegralElem.sub {x y : S} (hx : f.IsIntegralElem x) (hy : f.IsIntegralElem y) :
    f.IsIntegralElem (x - y) := by
  simpa only [sub_eq_add_neg] using hx.add f (hy.neg f)

Difference of Integral Elements is Integral

Informal description

Let $R$ and $S$ be commutative rings, and let $f : R \to S$ be a ring homomorphism. For any elements $x, y \in S$ that are integral over $R$ via $f$, their difference $x - y$ is also integral over $R$ via $f$.

IsIntegral.sub theorem

{x y : A} (hx : IsIntegral R x) (hy : IsIntegral R y) : IsIntegral R (x - y)

Full source

nonrec theorem IsIntegral.sub {x y : A} (hx : IsIntegral R x) (hy : IsIntegral R y) :
    IsIntegral R (x - y) :=
  hx.sub (algebraMap R A) hy

Difference of Integral Elements in an $R$-algebra is Integral

Informal description

Let $R$ be a commutative ring and $A$ an $R$-algebra. For any elements $x, y \in A$ that are integral over $R$, their difference $x - y$ is also integral over $R$.

RingHom.IsIntegralElem.mul theorem

{x y : S} (hx : f.IsIntegralElem x) (hy : f.IsIntegralElem y) : f.IsIntegralElem (x * y)

Full source

theorem RingHom.IsIntegralElem.mul {x y : S} (hx : f.IsIntegralElem x) (hy : f.IsIntegralElem y) :
    f.IsIntegralElem (x * y) :=
  hx.of_mem_closure f hy
    (Subring.mul_mem _ (Subring.subset_closure (Or.inl rfl)) (Subring.subset_closure (Or.inr rfl)))

Integrality is preserved under multiplication

Informal description

Let $R$ and $S$ be commutative rings, and let $f : R \to S$ be a ring homomorphism. For any elements $x, y \in S$ that are integral over $R$ via $f$, their product $x \cdot y$ is also integral over $R$ via $f$.

IsIntegral.mul theorem

{x y : A} (hx : IsIntegral R x) (hy : IsIntegral R y) : IsIntegral R (x * y)

Full source

nonrec theorem IsIntegral.mul {x y : A} (hx : IsIntegral R x) (hy : IsIntegral R y) :
    IsIntegral R (x * y) :=
  hx.mul (algebraMap R A) hy

Integrality is preserved under multiplication in $R$-algebras

Informal description

Let $R$ be a commutative ring and $A$ an $R$-algebra. For any elements $x, y \in A$ that are integral over $R$, their product $x \cdot y$ is also integral over $R$.

IsIntegral.smul theorem

 {R} [CommSemiring R] [Algebra R B] [Algebra S B] [Algebra R S] [IsScalarTower R S B] {x : B} (r : R)
  (hx : IsIntegral S x) : IsIntegral S (r • x)

Full source

theorem IsIntegral.smul {R} [CommSemiring R] [Algebra R B] [Algebra S B] [Algebra R S]
    [IsScalarTower R S B] {x : B} (r : R) (hx : IsIntegral S x) : IsIntegral S (r • x) :=
  .of_mem_of_fg _ hx.fg_adjoin_singleton _ <| by
    rw [← algebraMap_smul S]; apply Subalgebra.smul_mem; exact Algebra.subset_adjoin rfl

Scalar Multiplication Preserves Integrality in Tower of Algebras

Informal description

Let $R$ be a commutative semiring and $B$ an $S$-algebra, where $S$ is also an $R$-algebra, with a scalar tower structure $R \to S \to B$. For any element $x \in B$ that is integral over $S$ and any scalar $r \in R$, the element $r \cdot x$ is integral over $S$.

integralClosure definition

: Subalgebra R A

Full source

/-- The integral closure of `R` in an `R`-algebra `A`. -/
def integralClosure : Subalgebra R A where
  carrier := { r | IsIntegral R r }
  zero_mem' := isIntegral_zero
  one_mem' := isIntegral_one
  add_mem' := IsIntegral.add
  mul_mem' := IsIntegral.mul
  algebraMap_mem' _ := isIntegral_algebraMap

Integral closure of $R$ in $A$

Informal description

The integral closure of a commutative ring $R$ in an $R$-algebra $A$ is the subalgebra consisting of all elements of $A$ that are integral over $R$. Specifically, it is the set $\{x \in A \mid x \text{ is integral over } R\}$, which is closed under addition, multiplication, and contains the images of the algebra maps from $R$.

mem_integralClosure_iff theorem

{a : A} : a ∈ integralClosure R A ↔ IsIntegral R a

Full source

theorem mem_integralClosure_iff {a : A} : a ∈ integralClosure R Aa ∈ integralClosure R A ↔ IsIntegral R a :=
  Iff.rfl

Characterization of Integral Elements in the Integral Closure

Informal description

An element $a$ of an $R$-algebra $A$ belongs to the integral closure of $R$ in $A$ if and only if $a$ is integral over $R$.

Algebra.IsIntegral.prod instance

[Algebra.IsIntegral R A] [Algebra.IsIntegral R B] : Algebra.IsIntegral R (A × B)

Full source

/-- Product of two integral algebras is an integral algebra. -/
instance Algebra.IsIntegral.prod [Algebra.IsIntegral R A] [Algebra.IsIntegral R B] :
    Algebra.IsIntegral R (A × B) :=
  Algebra.isIntegral_def.mpr fun x ↦
    (Algebra.isIntegral_def.mp ‹_› x.1).pair (Algebra.isIntegral_def.mp ‹_› x.2)

Product of Integral Algebras is Integral

Informal description

For any commutative ring $R$ and $R$-algebras $A$ and $B$, if both $A$ and $B$ are integral over $R$, then their product $A \times B$ is also integral over $R$.

Main definitions