Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic

IsIntegral.isUnit theorem

[Field R] [Ring S] [IsDomain S] [Algebra R S] {x : S} (int : IsIntegral R x) (h0 : x ≠ 0) : IsUnit x

Full source

/-- A nonzero element in a domain integral over a field is a unit. -/
theorem IsIntegral.isUnit [Field R] [Ring S] [IsDomain S] [Algebra R S] {x : S}
    (int : IsIntegral R x) (h0 : x ≠ 0) : IsUnit x :=
  have : FiniteDimensional R (adjoin R {x}) := ⟨(Submodule.fg_top _).mpr int.fg_adjoin_singleton⟩
  (FiniteDimensional.isUnit R (K := adjoin R {x})
    (x := ⟨x, subset_adjoin rfl⟩) <| mt Subtype.ext_iff.mp h0).map (adjoin R {x}).val

Nonzero integral elements over a field are units

Informal description

Let $R$ be a field and $S$ be a domain with an $R$-algebra structure. For any nonzero element $x \in S$ that is integral over $R$, $x$ is a unit in $S$.

isField_of_isIntegral_of_isField' theorem

[CommRing R] [CommRing S] [IsDomain S] [Algebra R S] [Algebra.IsIntegral R S] (hR : IsField R) : IsField S

Full source

/-- A commutative domain that is an integral algebra over a field is a field. -/
theorem isField_of_isIntegral_of_isField' [CommRing R] [CommRing S] [IsDomain S]
    [Algebra R S] [Algebra.IsIntegral R S] (hR : IsField R) : IsField S where
  exists_pair_ne := ⟨0, 1, zero_ne_one⟩
  mul_comm := mul_comm
  mul_inv_cancel {x} hx := by
    letI := hR.toField
    obtain ⟨y, rfl⟩ := (Algebra.IsIntegral.isIntegral (R := R) x).isUnit hx
    exact ⟨y.inv, y.val_inv⟩

Integral domain algebra over a field is a field

Informal description

Let $R$ be a commutative ring and $S$ be a commutative domain with an $R$-algebra structure. If $S$ is integral over $R$ and $R$ is a field, then $S$ is also a field.

IsIntegral.inv_mem_adjoin theorem

(int : IsIntegral R x) : x⁻¹ ∈ adjoin R { x }

Full source

theorem IsIntegral.inv_mem_adjoin (int : IsIntegral R x) : x⁻¹x⁻¹ ∈ adjoin R {x} := by
  obtain rfl | h0 := eq_or_ne x 0
  · rw [inv_zero]; exact Subalgebra.zero_mem _
  have : FiniteDimensional R (adjoin R {x}) := ⟨(Submodule.fg_top _).mpr int.fg_adjoin_singleton⟩
  obtain ⟨⟨y, hy⟩, h1⟩ := FiniteDimensional.exists_mul_eq_one R
    (K := adjoin R {x}) (x := ⟨x, subset_adjoin rfl⟩) (mt Subtype.ext_iff.mp h0)
  rwa [← mul_left_cancel₀ h0 ((Subtype.ext_iff.mp h1).trans (mul_inv_cancel₀ h0).symm)]

Inverse of Integral Element Lies in Adjoint Algebra

Informal description

Let $R$ be a commutative ring and $x$ be an element of an $R$-algebra that is integral over $R$. Then the multiplicative inverse $x^{-1}$ of $x$ is contained in the $R$-algebra adjoint of the singleton set $\{x\}$.

IsIntegral.inv_mem theorem

(int : IsIntegral R x) (hx : x ∈ A) : x⁻¹ ∈ A

Full source

/-- The inverse of an integral element in a subalgebra of a division ring over a field
  also lies in that subalgebra. -/
theorem IsIntegral.inv_mem (int : IsIntegral R x) (hx : x ∈ A) : x⁻¹x⁻¹ ∈ A :=
  adjoin_le (Set.singleton_subset_iff.mpr hx) int.inv_mem_adjoin

Inverse of Integral Element in Subalgebra

Informal description

Let $R$ be a commutative ring and $A$ be a subalgebra of an $R$-algebra. If an element $x \in A$ is integral over $R$, then its multiplicative inverse $x^{-1}$ also lies in $A$.

Algebra.IsIntegral.inv_mem theorem

[Algebra.IsIntegral R A] (hx : x ∈ A) : x⁻¹ ∈ A

Full source

/-- An integral subalgebra of a division ring over a field is closed under inverses. -/
theorem Algebra.IsIntegral.inv_mem [Algebra.IsIntegral R A] (hx : x ∈ A) : x⁻¹x⁻¹ ∈ A :=
  ((isIntegral_algHom_iff A.val Subtype.val_injective).mpr <|
    Algebra.IsIntegral.isIntegral (⟨x, hx⟩ : A)).inv_mem hx

Inverse of an element in an integral algebra remains in the algebra

Informal description

Let $R$ be a commutative ring and $A$ be an integral $R$-algebra. For any element $x \in A$, its multiplicative inverse $x^{-1}$ also lies in $A$.

IsIntegral.inv theorem

(int : IsIntegral R x) : IsIntegral R x⁻¹

Full source

/-- The inverse of an integral element in a division ring over a field is also integral. -/
theorem IsIntegral.inv (int : IsIntegral R x) : IsIntegral R x⁻¹ :=
  .of_mem_of_fg _ int.fg_adjoin_singleton _ int.inv_mem_adjoin

Integrality of Inverses: $x$ integral implies $x^{-1}$ integral

Informal description

Let $R$ be a commutative ring and $A$ be an $R$-algebra. If an element $x \in A$ is integral over $R$, then its multiplicative inverse $x^{-1}$ is also integral over $R$.

IsIntegral.mem_of_inv_mem theorem

(int : IsIntegral R x) (inv_mem : x⁻¹ ∈ A) : x ∈ A

Full source

theorem IsIntegral.mem_of_inv_mem (int : IsIntegral R x) (inv_mem : x⁻¹x⁻¹ ∈ A) : x ∈ A := by
  rw [← inv_inv x]; exact int.inv.inv_mem inv_mem

Membership of Integral Element via Inverse Membership

Informal description

Let $R$ be a commutative ring and $A$ be an $R$-algebra. If an element $x$ is integral over $R$ and its inverse $x^{-1}$ belongs to $A$, then $x$ itself belongs to $A$.

Algebra.IsIntegral.finite theorem

[Algebra.IsIntegral R A] [h' : Algebra.FiniteType R A] : Module.Finite R A

Full source

/-- The [Kurosh problem](https://en.wikipedia.org/wiki/Kurosh_problem) asks to show that
  this is still true when `A` is not necessarily commutative and `R` is a field, but it has
  been solved in the negative. See https://arxiv.org/pdf/1706.02383.pdf for criteria for a
  finitely generated algebraic (= integral) algebra over a field to be finite dimensional.

This could be an `instance`, but we tend to go from `Module.Finite` to `IsIntegral`/`IsAlgebraic`,
and making it an instance will cause the search to be complicated a lot.
-/
theorem Algebra.IsIntegral.finite [Algebra.IsIntegral R A] [h' : Algebra.FiniteType R A] :
    Module.Finite R A :=
  have ⟨s, hs⟩ := h'
  ⟨by apply hs ▸ fg_adjoin_of_finite s.finite_toSet fun x _ ↦ Algebra.IsIntegral.isIntegral x⟩

Finiteness of Integral and Finitely Generated Algebras as Modules

Informal description

If $A$ is an integral $R$-algebra and is finitely generated as an $R$-algebra, then $A$ is finitely generated as an $R$-module.

Algebra.finite_iff_isIntegral_and_finiteType theorem

: Module.Finite R A ↔ Algebra.IsIntegral R A ∧ Algebra.FiniteType R A

Full source

/-- finite = integral + finite type -/
theorem Algebra.finite_iff_isIntegral_and_finiteType :
    Module.FiniteModule.Finite R A ↔ Algebra.IsIntegral R A ∧ Algebra.FiniteType R A :=
  ⟨fun _ ↦ ⟨⟨.of_finite R⟩, inferInstance⟩, fun ⟨h, _⟩ ↦ h.finite⟩

Finiteness Criterion for Algebras: Finite Module iff Integral and Finite Type

Informal description

An $R$-algebra $A$ is finitely generated as an $R$-module if and only if $A$ is integral over $R$ and finitely generated as an $R$-algebra.

RingHom.IsIntegral.to_finite theorem

(h : f.IsIntegral) (h' : f.FiniteType) : f.Finite

Full source

theorem RingHom.IsIntegral.to_finite (h : f.IsIntegral) (h' : f.FiniteType) : f.Finite :=
  let _ := f.toAlgebra
  let _ : Algebra.IsIntegral R S := ⟨h⟩
  Algebra.IsIntegral.finite (h' := h')

Integral and Finitely Generated Implies Finite Module Extension

Informal description

Let $f: R \to A$ be a ring homomorphism. If $f$ is integral and $A$ is finitely generated as an $R$-algebra via $f$, then $A$ is finitely generated as an $R$-module via $f$.

RingHom.finite_iff_isIntegral_and_finiteType theorem

: f.Finite ↔ f.IsIntegral ∧ f.FiniteType

Full source

/-- finite = integral + finite type -/
theorem RingHom.finite_iff_isIntegral_and_finiteType : f.Finite ↔ f.IsIntegral ∧ f.FiniteType :=
  ⟨fun h ↦ ⟨h.to_isIntegral, h.to_finiteType⟩, fun ⟨h, h'⟩ ↦ h.to_finite h'⟩

Finite iff Integral and Finite Type for Ring Homomorphisms

Informal description

A ring homomorphism $f \colon R \to A$ is finite (i.e., $A$ is finitely generated as an $R$-module via $f$) if and only if $f$ is integral (i.e., every element of $A$ is integral over $R$ via $f$) and $A$ is finitely generated as an $R$-algebra via $f$.

mem_integralClosure_iff_mem_fg theorem

{r : A} : r ∈ integralClosure R A ↔ ∃ M : Subalgebra R A, M.toSubmodule.FG ∧ r ∈ M

Full source

theorem mem_integralClosure_iff_mem_fg {r : A} :
    r ∈ integralClosure R Ar ∈ integralClosure R A ↔ ∃ M : Subalgebra R A, M.toSubmodule.FG ∧ r ∈ M :=
  ⟨fun hr =>
    ⟨Algebra.adjoin R {r}, hr.fg_adjoin_singleton, Algebra.subset_adjoin rfl⟩,
    fun ⟨M, Hf, hrM⟩ => .of_mem_of_fg M Hf _ hrM⟩

Characterization of Integral Closure via Finitely Generated Subalgebras

Informal description

An element $r$ of an $R$-algebra $A$ is in the integral closure of $R$ in $A$ if and only if there exists a finitely generated $R$-subalgebra $M$ of $A$ containing $r$.

adjoin_le_integralClosure theorem

{x : A} (hx : IsIntegral R x) : Algebra.adjoin R { x } ≤ integralClosure R A

Full source

theorem adjoin_le_integralClosure {x : A} (hx : IsIntegral R x) :
    Algebra.adjoin R {x} ≤ integralClosure R A := by
  rw [Algebra.adjoin_le_iff]
  simp only [SetLike.mem_coe, Set.singleton_subset_iff]
  exact hx

Integrality of Adjoined Element Implies Integrality of Generated Algebra

Informal description

For any element $x$ in an $R$-algebra $A$ that is integral over $R$, the $R$-algebra generated by $x$ is contained in the integral closure of $R$ in $A$. In other words, if $x$ satisfies a monic polynomial with coefficients in $R$, then every element of the algebra $R[x]$ is integral over $R$.

le_integralClosure_iff_isIntegral theorem

{S : Subalgebra R A} : S ≤ integralClosure R A ↔ Algebra.IsIntegral R S

Full source

theorem le_integralClosure_iff_isIntegral {S : Subalgebra R A} :
    S ≤ integralClosure R A ↔ Algebra.IsIntegral R S :=
  SetLike.forall.symm.trans <|
    (forall_congr' fun x =>
      show IsIntegralIsIntegral R (algebraMap S A x) ↔ IsIntegral R x from
        isIntegral_algebraMap_iff Subtype.coe_injective).trans
      Algebra.isIntegral_def.symm

Subalgebra Inclusion in Integral Closure iff All Elements are Integral

Informal description

For any subalgebra $S$ of an $R$-algebra $A$, the inclusion $S \subseteq \text{integralClosure}(R, A)$ holds if and only if every element of $S$ is integral over $R$.

Algebra.IsIntegral.adjoin theorem

{S : Set A} (hS : ∀ x ∈ S, IsIntegral R x) : Algebra.IsIntegral R (adjoin R S)

Full source

theorem Algebra.IsIntegral.adjoin {S : Set A} (hS : ∀ x ∈ S, IsIntegral R x) :
    Algebra.IsIntegral R (adjoin R S) :=
  le_integralClosure_iff_isIntegral.mp <| adjoin_le hS

Integrality of Adjoined Set Implies Integrality of Generated Algebra

Informal description

For any subset $S$ of an $R$-algebra $A$ where every element $x \in S$ is integral over $R$, the $R$-algebra generated by $S$ (denoted $\text{adjoin}_R(S)$) is integral over $R$.

integralClosure_eq_top_iff theorem

: integralClosure R A = ⊤ ↔ Algebra.IsIntegral R A

Full source

theorem integralClosure_eq_top_iff : integralClosureintegralClosure R A = ⊤ ↔ Algebra.IsIntegral R A := by
  rw [← top_le_iff, le_integralClosure_iff_isIntegral,
      (Subalgebra.topEquiv (R := R) (A := A)).isIntegral_iff]

Integral Closure Equals Top iff Algebra is Integral

Informal description

The integral closure of a commutative ring $R$ in an $R$-algebra $A$ is equal to the entire algebra (i.e., $\text{integralClosure}(R, A) = \top$) if and only if every element of $A$ is integral over $R$.

Algebra.isIntegral_sup theorem

 {S T : Subalgebra R A} :
  Algebra.IsIntegral R (S ⊔ T : Subalgebra R A) ↔ Algebra.IsIntegral R S ∧ Algebra.IsIntegral R T

Full source

theorem Algebra.isIntegral_sup {S T : Subalgebra R A} :
    Algebra.IsIntegralAlgebra.IsIntegral R (S ⊔ T : Subalgebra R A) ↔
      Algebra.IsIntegral R S ∧ Algebra.IsIntegral R T := by
  simp_rw [← le_integralClosure_iff_isIntegral, sup_le_iff]

Integrality of Join of Subalgebras

Informal description

For any two subalgebras $S$ and $T$ of an $R$-algebra $A$, the join $S \sqcup T$ is integral over $R$ if and only if both $S$ and $T$ are integral over $R$.

Algebra.isIntegral_iSup theorem

{ι} (S : ι → Subalgebra R A) : Algebra.IsIntegral R ↑(iSup S) ↔ ∀ i, Algebra.IsIntegral R (S i)

Full source

theorem Algebra.isIntegral_iSup {ι} (S : ι → Subalgebra R A) :
    Algebra.IsIntegralAlgebra.IsIntegral R ↑(iSup S) ↔ ∀ i, Algebra.IsIntegral R (S i) := by
  simp_rw [← le_integralClosure_iff_isIntegral, iSup_le_iff]

Integrality of Supremum of Subalgebras

Informal description

Let $R$ be a commutative ring and $A$ an $R$-algebra. For a family of subalgebras $(S_i)_{i \in \iota}$ of $A$, the supremum $\bigsqcup_{i \in \iota} S_i$ is integral over $R$ if and only if each $S_i$ is integral over $R$.

integralClosure_map_algEquiv theorem

[Algebra R S] (f : A ≃ₐ[R] S) : (integralClosure R A).map (f : A →ₐ[R] S) = integralClosure R S

Full source

/-- Mapping an integral closure along an `AlgEquiv` gives the integral closure. -/
theorem integralClosure_map_algEquiv [Algebra R S] (f : A ≃ₐ[R] S) :
    (integralClosure R A).map (f : A →ₐ[R] S) = integralClosure R S := by
  ext y
  rw [Subalgebra.mem_map]
  constructor
  · rintro ⟨x, hx, rfl⟩
    exact hx.map f
  · intro hy
    use f.symm y, hy.map (f.symm : S →ₐ[R] A)
    simp

Integral Closure Preservation under Algebra Isomorphism

Informal description

Let $R$ be a commutative ring, and let $A$ and $S$ be $R$-algebras. Given an $R$-algebra isomorphism $f \colon A \to S$, the image of the integral closure of $R$ in $A$ under $f$ is equal to the integral closure of $R$ in $S$. That is, \[ f(\text{integralClosure}(R, A)) = \text{integralClosure}(R, S). \]

AlgHom.mapIntegralClosure definition

[Algebra R S] (f : A →ₐ[R] S) : integralClosure R A →ₐ[R] integralClosure R S

Full source

/-- An `AlgHom` between two rings restrict to an `AlgHom` between the integral closures inside
them. -/
def AlgHom.mapIntegralClosure [Algebra R S] (f : A →ₐ[R] S) :
    integralClosureintegralClosure R A →ₐ[R] integralClosure R S :=
  (f.restrictDomain (integralClosure R A)).codRestrict (integralClosure R S) (fun ⟨_, h⟩ => h.map f)

Restriction of an algebra homomorphism to integral closures

Informal description

Given an algebra homomorphism $f \colon A \to S$ over a commutative ring $R$, the function maps an element of the integral closure of $R$ in $A$ to its image under $f$ in the integral closure of $R$ in $S$.

AlgHom.coe_mapIntegralClosure theorem

[Algebra R S] (f : A →ₐ[R] S) (x : integralClosure R A) : (f.mapIntegralClosure x : S) = f (x : A)

Full source

@[simp]
theorem AlgHom.coe_mapIntegralClosure [Algebra R S] (f : A →ₐ[R] S)
    (x : integralClosure R A) : (f.mapIntegralClosure x : S) = f (x : A) := rfl

Equality of Images under Algebra Homomorphism and its Restriction to Integral Closure

Informal description

Let $R$ be a commutative ring, and let $A$ and $S$ be $R$-algebras. Given an $R$-algebra homomorphism $f \colon A \to S$ and an element $x$ in the integral closure of $R$ in $A$, the image of $x$ under the restriction of $f$ to the integral closure of $R$ in $A$ is equal to the image of $x$ under $f$ in $S$. In other words, \[ f_{\text{mapIntegralClosure}}(x) = f(x). \]

AlgEquiv.mapIntegralClosure definition

[Algebra R S] (f : A ≃ₐ[R] S) : integralClosure R A ≃ₐ[R] integralClosure R S

Full source

/-- An `AlgEquiv` between two rings restrict to an `AlgEquiv` between the integral closures inside
them. -/
def AlgEquiv.mapIntegralClosure [Algebra R S] (f : A ≃ₐ[R] S) :
    integralClosureintegralClosure R A ≃ₐ[R] integralClosure R S :=
  AlgEquiv.ofAlgHom (f : A →ₐ[R] S).mapIntegralClosure (f.symm : S →ₐ[R] A).mapIntegralClosure
    (AlgHom.ext fun _ ↦ Subtype.ext (f.right_inv _))
    (AlgHom.ext fun _ ↦ Subtype.ext (f.left_inv _))

Restriction of an algebra equivalence to integral closures

Informal description

Given an algebra equivalence $f \colon A \simeq_{\text{Alg}[R]} S$ between two $R$-algebras, the function restricts to an algebra equivalence between the integral closures of $R$ in $A$ and $S$ respectively. Specifically, it maps an element of the integral closure of $R$ in $A$ to its image under $f$ in the integral closure of $R$ in $S$, and vice versa under the inverse of $f$.

AlgEquiv.coe_mapIntegralClosure theorem

[Algebra R S] (f : A ≃ₐ[R] S) (x : integralClosure R A) : (f.mapIntegralClosure x : S) = f (x : A)

Full source

@[simp]
theorem AlgEquiv.coe_mapIntegralClosure [Algebra R S] (f : A ≃ₐ[R] S)
    (x : integralClosure R A) : (f.mapIntegralClosure x : S) = f (x : A) := rfl

Equality of Images under Algebra Equivalence and its Restriction to Integral Closure

Informal description

Let $R$ be a commutative ring, and let $A$ and $S$ be $R$-algebras. Given an $R$-algebra equivalence $f \colon A \simeq_{\text{Alg}[R]} S$ and an element $x$ in the integral closure of $R$ in $A$, the image of $x$ under the restriction of $f$ to the integral closure of $R$ in $A$ is equal to the image of $x$ under $f$ in $S$. In other words, \[ f_{\text{mapIntegralClosure}}(x) = f(x). \]

integralClosure.isIntegral theorem

(x : integralClosure R A) : IsIntegral R x

Full source

theorem integralClosure.isIntegral (x : integralClosure R A) : IsIntegral R x :=
  let ⟨p, hpm, hpx⟩ := x.2
  ⟨p, hpm,
    Subtype.eq <| by
      rwa [← aeval_def, ← Subalgebra.val_apply, aeval_algHom_apply] at hpx⟩

Integrality of Elements in the Integral Closure

Informal description

For any element $x$ in the integral closure of $R$ in $A$, $x$ is integral over $R$.

integralClosure.AlgebraIsIntegral instance

: Algebra.IsIntegral R (integralClosure R A)

Full source

instance integralClosure.AlgebraIsIntegral : Algebra.IsIntegral R (integralClosure R A) :=
  ⟨integralClosure.isIntegral⟩

Integral Closure is an Integral Algebra

Informal description

The integral closure of a commutative ring $R$ in an $R$-algebra $A$ is an integral $R$-algebra. That is, every element of the integral closure is integral over $R$.

IsIntegral.of_mul_unit theorem

{x y : B} {r : R} (hr : algebraMap R B r * y = 1) (hx : IsIntegral R (x * y)) : IsIntegral R x

Full source

theorem IsIntegral.of_mul_unit {x y : B} {r : R} (hr : algebraMap R B r * y = 1)
    (hx : IsIntegral R (x * y)) : IsIntegral R x := by
  obtain ⟨p, p_monic, hp⟩ := hx
  refine ⟨scaleRoots p r, (monic_scaleRoots_iff r).2 p_monic, ?_⟩
  convert scaleRoots_aeval_eq_zero hp
  rw [Algebra.commutes] at hr ⊢
  rw [mul_assoc, hr, mul_one]; rfl

Integrality of an element via multiplicative unit condition

Informal description

Let $R$ be a commutative ring and $B$ an $R$-algebra. For elements $x, y \in B$ and $r \in R$, if $y$ is a multiplicative inverse of $\text{algebraMap}(r)$ (i.e., $\text{algebraMap}(r) \cdot y = 1$) and $x \cdot y$ is integral over $R$, then $x$ is integral over $R$.

RingHom.IsIntegralElem.of_mul_unit theorem

(x y : S) (r : R) (hr : f r * y = 1) (hx : f.IsIntegralElem (x * y)) : f.IsIntegralElem x

Full source

theorem RingHom.IsIntegralElem.of_mul_unit (x y : S) (r : R) (hr : f r * y = 1)
    (hx : f.IsIntegralElem (x * y)) : f.IsIntegralElem x :=
  letI : Algebra R S := f.toAlgebra
  IsIntegral.of_mul_unit hr hx

Integrality via Multiplicative Unit Condition for Ring Homomorphisms

Informal description

Let $R$ and $S$ be commutative rings, and let $f: R \to S$ be a ring homomorphism. For elements $x, y \in S$ and $r \in R$, if $y$ is a multiplicative inverse of $f(r)$ (i.e., $f(r) \cdot y = 1$) and $x \cdot y$ is integral over $R$ with respect to $f$, then $x$ is integral over $R$ with respect to $f$.

IsIntegral.of_mem_closure' theorem

(G : Set A) (hG : ∀ x ∈ G, IsIntegral R x) : ∀ x ∈ Subring.closure G, IsIntegral R x

Full source

/-- Generalization of `IsIntegral.of_mem_closure` bootstrapped up from that lemma -/
theorem IsIntegral.of_mem_closure' (G : Set A) (hG : ∀ x ∈ G, IsIntegral R x) :
    ∀ x ∈ Subring.closure G, IsIntegral R x := fun _ hx ↦
  Subring.closure_induction hG isIntegral_zero isIntegral_one (fun _ _ _ _ ↦ IsIntegral.add)
    (fun _ _ ↦ IsIntegral.neg) (fun _ _ _ _ ↦ IsIntegral.mul) hx

Integrality of elements in subring closure of integral elements

Informal description

Let $R$ be a commutative ring and $A$ an $R$-algebra. Given a subset $G \subseteq A$ where every element of $G$ is integral over $R$, then every element in the subring generated by $G$ is also integral over $R$.

IsIntegral.of_mem_closure'' theorem

 {S : Type*} [CommRing S] {f : R →+* S} (G : Set S) (hG : ∀ x ∈ G, f.IsIntegralElem x) :
  ∀ x ∈ Subring.closure G, f.IsIntegralElem x

Full source

theorem IsIntegral.of_mem_closure'' {S : Type*} [CommRing S] {f : R →+* S} (G : Set S)
    (hG : ∀ x ∈ G, f.IsIntegralElem x) : ∀ x ∈ Subring.closure G, f.IsIntegralElem x := fun x hx =>
  @IsIntegral.of_mem_closure' R S _ _ f.toAlgebra G hG x hx

Integrality of Elements in Subring Closure with Respect to Ring Homomorphism

Informal description

Let $R$ and $S$ be commutative rings, and let $f: R \to S$ be a ring homomorphism. Given a subset $G \subseteq S$ where every element of $G$ is integral over $R$ with respect to $f$, then every element in the subring generated by $G$ is also integral over $R$ with respect to $f$.

IsIntegral.pow theorem

{x : B} (h : IsIntegral R x) (n : ℕ) : IsIntegral R (x ^ n)

Full source

theorem IsIntegral.pow {x : B} (h : IsIntegral R x) (n : ℕ) : IsIntegral R (x ^ n) :=
  .of_mem_of_fg _ h.fg_adjoin_singleton _ <|
    Subalgebra.pow_mem _ (by exact Algebra.subset_adjoin rfl) _

Powers of integral elements are integral

Informal description

Let $R$ be a commutative ring and $B$ an $R$-algebra. For any element $x \in B$ that is integral over $R$ and any natural number $n$, the power $x^n$ is also integral over $R$.

IsIntegral.nsmul theorem

{x : B} (h : IsIntegral R x) (n : ℕ) : IsIntegral R (n • x)

Full source

theorem IsIntegral.nsmul {x : B} (h : IsIntegral R x) (n : ℕ) : IsIntegral R (n • x) :=
  h.smul n

Natural scalar multiples of integral elements are integral

Informal description

Let $R$ be a commutative ring and $B$ an $R$-algebra. For any element $x \in B$ that is integral over $R$ and any natural number $n$, the scalar multiple $n \cdot x$ is also integral over $R$.

IsIntegral.zsmul theorem

{x : B} (h : IsIntegral R x) (n : ℤ) : IsIntegral R (n • x)

Full source

theorem IsIntegral.zsmul {x : B} (h : IsIntegral R x) (n : ℤ) : IsIntegral R (n • x) :=
  h.smul n

Integrality is preserved under integer scalar multiplication

Informal description

Let $R$ be a commutative ring and $B$ an $R$-algebra. For any element $x \in B$ that is integral over $R$ and any integer $n$, the scalar multiple $n \cdot x$ is also integral over $R$.

IsIntegral.multiset_prod theorem

{s : Multiset A} (h : ∀ x ∈ s, IsIntegral R x) : IsIntegral R s.prod

Full source

theorem IsIntegral.multiset_prod {s : Multiset A} (h : ∀ x ∈ s, IsIntegral R x) :
    IsIntegral R s.prod :=
  (integralClosure R A).multiset_prod_mem h

Product of Integral Elements in Multiset is Integral

Informal description

Let $R$ be a commutative ring and $A$ an $R$-algebra. For any multiset $s$ of elements in $A$, if every element $x \in s$ is integral over $R$, then the product of all elements in $s$ is also integral over $R$.

IsIntegral.multiset_sum theorem

{s : Multiset A} (h : ∀ x ∈ s, IsIntegral R x) : IsIntegral R s.sum

Full source

theorem IsIntegral.multiset_sum {s : Multiset A} (h : ∀ x ∈ s, IsIntegral R x) :
    IsIntegral R s.sum :=
  (integralClosure R A).multiset_sum_mem h

Sum of Integral Elements in Multiset is Integral

Informal description

Let $R$ be a commutative ring and $A$ an $R$-algebra. For any multiset $s$ of elements in $A$, if every element $x \in s$ is integral over $R$, then the sum of all elements in $s$ is also integral over $R$.

IsIntegral.prod theorem

{α : Type*} {s : Finset α} (f : α → A) (h : ∀ x ∈ s, IsIntegral R (f x)) : IsIntegral R (∏ x ∈ s, f x)

Full source

theorem IsIntegral.prod {α : Type*} {s : Finset α} (f : α → A) (h : ∀ x ∈ s, IsIntegral R (f x)) :
    IsIntegral R (∏ x ∈ s, f x) :=
  (integralClosure R A).prod_mem h

Product of Integral Elements is Integral

Informal description

Let $R$ be a commutative ring and $A$ an $R$-algebra. For any finite set $s$ indexed by a type $\alpha$ and any function $f: \alpha \to A$, if $f(x)$ is integral over $R$ for every $x \in s$, then the product $\prod_{x \in s} f(x)$ is also integral over $R$.

IsIntegral.sum theorem

{α : Type*} {s : Finset α} (f : α → A) (h : ∀ x ∈ s, IsIntegral R (f x)) : IsIntegral R (∑ x ∈ s, f x)

Full source

theorem IsIntegral.sum {α : Type*} {s : Finset α} (f : α → A) (h : ∀ x ∈ s, IsIntegral R (f x)) :
    IsIntegral R (∑ x ∈ s, f x) :=
  (integralClosure R A).sum_mem h

Sum of Integral Elements in Finite Set is Integral

Informal description

Let $R$ be a commutative ring and $A$ an $R$-algebra. For any finite set $s$ indexed by a type $\alpha$ and any function $f \colon \alpha \to A$, if every element $f(x)$ with $x \in s$ is integral over $R$, then the sum $\sum_{x \in s} f(x)$ is also integral over $R$.

IsIntegral.det theorem

{n : Type*} [Fintype n] [DecidableEq n] {M : Matrix n n A} (h : ∀ i j, IsIntegral R (M i j)) : IsIntegral R M.det

Full source

theorem IsIntegral.det {n : Type*} [Fintype n] [DecidableEq n] {M : Matrix n n A}
    (h : ∀ i j, IsIntegral R (M i j)) : IsIntegral R M.det := by
  rw [Matrix.det_apply]
  exact IsIntegral.sum _ fun σ _hσ ↦ (IsIntegral.prod _ fun i _hi => h _ _).zsmul _

Integrality of Determinant of Matrix with Integral Entries

Informal description

Let $R$ be a commutative ring and $A$ an $R$-algebra. For any finite type $n$ and any $n \times n$ matrix $M$ with entries in $A$, if each entry $M_{ij}$ is integral over $R$, then the determinant $\det M$ is also integral over $R$.

IsIntegral.pow_iff theorem

{x : A} {n : ℕ} (hn : 0 < n) : IsIntegral R (x ^ n) ↔ IsIntegral R x

Full source

@[simp]
theorem IsIntegral.pow_iff {x : A} {n : ℕ} (hn : 0 < n) : IsIntegralIsIntegral R (x ^ n) ↔ IsIntegral R x :=
  ⟨IsIntegral.of_pow hn, fun hx ↦ hx.pow n⟩

Integrality of Element and its Powers: $x^n$ integral iff $x$ integral for $n > 0$

Informal description

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

IsIntegral.tmul theorem

(x : A) {y : B} (h : IsIntegral R y) : IsIntegral A (x ⊗ₜ[R] y)

Full source

theorem IsIntegral.tmul (x : A) {y : B} (h : IsIntegral R y) : IsIntegral A (x ⊗ₜ[R] y) := by
  rw [← mul_one x, ← smul_eq_mul, ← smul_tmul']
  exact smul _ (h.map_of_comp_eq (algebraMap R A)
    (Algebra.TensorProduct.includeRight (R := R) (A := A) (B := B)).toRingHom
    Algebra.TensorProduct.includeLeftRingHom_comp_algebraMap)

Integrality of Tensor Product Element over Base Algebra

Informal description

Let $A$ and $B$ be $R$-algebras, and let $y \in B$ be an element integral over $R$. Then for any $x \in A$, the tensor product element $x \otimes_{R} y$ in $A \otimes_{R} B$ is integral over $A$.

RingHom.isIntegralElem_leadingCoeff_mul theorem

(h : p.eval₂ f x = 0) : f.IsIntegralElem (f p.leadingCoeff * x)

Full source

/-- Given a `p : R[X]` and a `x : S` such that `p.eval₂ f x = 0`,
`f p.leadingCoeff * x` is integral. -/
theorem RingHom.isIntegralElem_leadingCoeff_mul (h : p.eval₂ f x = 0) :
    f.IsIntegralElem (f p.leadingCoeff * x) := by
  by_cases h' : 1 ≤ p.natDegree
  · use integralNormalization p
    have : p ≠ 0 := fun h'' => by
      rw [h'', natDegree_zero] at h'
      exact Nat.not_succ_le_zero 0 h'
    use monic_integralNormalization this
    rw [integralNormalization_eval₂_leadingCoeff_mul h' f x, h, mul_zero]
  · by_cases hp : p.map f = 0
    · apply_fun fun q => coeff q p.natDegree at hp
      rw [coeff_map, coeff_zero, coeff_natDegree] at hp
      rw [hp, zero_mul]
      exact f.isIntegralElem_zero
    · rw [Nat.one_le_iff_ne_zero, Classical.not_not] at h'
      rw [eq_C_of_natDegree_eq_zero h', eval₂_C] at h
      suffices p.map f = 0 by exact (hp this).elim
      rw [eq_C_of_natDegree_eq_zero h', map_C, h, C_eq_zero]

Integrality of Leading Coefficient Multiple under Polynomial Evaluation

Informal description

Let $R$ and $A$ be commutative rings with a ring homomorphism $f: R \to A$. Given a polynomial $p \in R[X]$ and an element $x \in A$ such that $p$ evaluated at $x$ via $f$ is zero (i.e., $p.eval₂ f x = 0$), then the element $f(p.leadingCoeff) \cdot x$ is integral over $R$ with respect to $f$.

isIntegral_leadingCoeff_smul theorem

[Algebra R S] (h : aeval x p = 0) : IsIntegral R (p.leadingCoeff • x)

Full source

/-- Given a `p : R[X]` and a root `x : S`,
then `p.leadingCoeff • x : S` is integral over `R`. -/
theorem isIntegral_leadingCoeff_smul [Algebra R S] (h : aeval x p = 0) :
    IsIntegral R (p.leadingCoeff • x) := by
  rw [aeval_def] at h
  rw [Algebra.smul_def]
  exact (algebraMap R S).isIntegralElem_leadingCoeff_mul p x h

Integrality of Leading Coefficient Scalar Multiple under Polynomial Evaluation

Informal description

Let $R$ and $S$ be commutative rings with an $R$-algebra structure on $S$. Given a polynomial $p \in R[X]$ and an element $x \in S$ such that the evaluation of $p$ at $x$ via the algebra map is zero (i.e., $\text{aeval}(x)(p) = 0$), then the element $p.\text{leadingCoeff} \cdot x$ is integral over $R$.

Polynomial.Monic.quotient_isIntegralElem theorem

 {g : S[X]} (mon : g.Monic) {I : Ideal S[X]} (h : g ∈ I) :
  ((Ideal.Quotient.mk I).comp (algebraMap S S[X])).IsIntegralElem (Ideal.Quotient.mk I X)

Full source

lemma Polynomial.Monic.quotient_isIntegralElem {g : S[X]} (mon : g.Monic) {I : Ideal S[X]}
    (h : g ∈ I) :
    ((Ideal.Quotient.mk I).comp (algebraMap S S[X])).IsIntegralElem (Ideal.Quotient.mk I X) := by
  exact ⟨g, mon, by
  rw [← (Ideal.Quotient.eq_zero_iff_mem.mpr h), eval₂_eq_sum_range]
  nth_rw 3 [(as_sum_range_C_mul_X_pow g)]
  simp only [map_sum, algebraMap_eq, RingHom.coe_comp, Function.comp_apply, map_mul, map_pow]⟩

Integrality of $ X $ in Quotient Ring by Monic Polynomial Ideal

Informal description

Let $ S $ be a commutative ring, $ g \in S[X] $ a monic polynomial, and $ I $ an ideal of $ S[X] $ containing $ g $. Then the image of $ X $ in the quotient ring $ S[X]/I $ is integral over $ S $ with respect to the composition of the quotient map $ S[X] \to S[X]/I $ with the canonical algebra map $ S \to S[X] $.

Polynomial.Monic.quotient_isIntegral theorem

 {g : S[X]} (mon : g.Monic) {I : Ideal S[X]} (h : g ∈ I) :
  ((Ideal.Quotient.mkₐ S I).comp (Algebra.ofId S S[X])).IsIntegral

Full source

lemma Polynomial.Monic.quotient_isIntegral {g : S[X]} (mon : g.Monic) {I : Ideal S[X]} (h : g ∈ I) :
    ((Ideal.Quotient.mkₐ S I).comp (Algebra.ofId S S[X])).IsIntegral := by
  have eq_top : Algebra.adjoin S {(Ideal.Quotient.mkₐ S I) X} = ⊤ := by
    ext g
    constructor
    · simp only [Algebra.mem_top, implies_true]
    · intro _
      obtain ⟨g', hg⟩ := Ideal.Quotient.mkₐ_surjective S I g
      have : g = (Polynomial.aeval ((Ideal.Quotient.mkₐ S I) X)) g' := by
        nth_rw 1 [← hg, aeval_eq_sum_range' (lt_add_one _),
          as_sum_range_C_mul_X_pow g', map_sum]
        simp only [Polynomial.C_mul', ← map_pow, map_smul]
      exact this ▸ (aeval_mem_adjoin_singleton S ((Ideal.Quotient.mk I) Polynomial.X))
  exact fun a ↦ (eq_top ▸ adjoin_le_integralClosure <| mon.quotient_isIntegralElem h)
    Algebra.mem_top

Integrality of Quotient Algebra Map for Monic Polynomial Ideal

Informal description

Let $S$ be a commutative ring, $g \in S[X]$ a monic polynomial, and $I$ an ideal of $S[X]$ containing $g$. Then the composition of the quotient algebra map $S[X]/I$ with the canonical algebra map $S \to S[X]$ is an integral ring homomorphism.

integralClosure.isIntegralClosure instance

(R A : Type*) [CommRing R] [CommRing A] [Algebra R A] : IsIntegralClosure (integralClosure R A) R A

Full source

instance integralClosure.isIntegralClosure (R A : Type*) [CommRing R] [CommRing A] [Algebra R A] :
    IsIntegralClosure (integralClosure R A) R A where
  algebraMap_injective' := Subtype.coe_injective
  isIntegral_iff {x} := ⟨fun h => ⟨⟨x, h⟩, rfl⟩, by rintro ⟨⟨_, h⟩, rfl⟩; exact h⟩

Integral Closure as Integral Closure

Informal description

For any commutative rings $R$ and $A$ with an algebra structure $R \to A$, the integral closure of $R$ in $A$ is indeed the integral closure of $R$ in $A$. That is, the subalgebra consisting of all elements of $A$ that are integral over $R$ satisfies the property that an element of $A$ is integral over $R$ if and only if it lies in this subalgebra.

IsIntegralClosure.algebraMap_injective theorem

 (A R B : Type*) [CommRing R] [CommSemiring A] [CommRing B] [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] :
  Function.Injective (algebraMap A B)

Full source

theorem algebraMap_injective (A R B : Type*) [CommRing R] [CommSemiring A] [CommRing B]
    [Algebra R B] [Algebra A B] [IsIntegralClosure A R B] : Function.Injective (algebraMap A B) :=
  algebraMap_injective' R

Injectivity of the Algebra Map in Integral Closure

Informal description

Let $A$, $R$, and $B$ be commutative rings with $A$ being a commutative semiring, equipped with algebra structures $A \to B$ and $R \to B$. If $A$ is the integral closure of $R$ in $B$, then the algebra map $\text{algebraMap}: A \to B$ is injective.

IsIntegralClosure.isIntegral theorem

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

Full source

protected theorem isIntegral [Algebra R A] [IsScalarTower R A B] (x : A) : IsIntegral R x :=
  (isIntegral_algebraMap_iff (algebraMap_injective A R B)).mp <|
    show IsIntegral R (algebraMap A B x) from isIntegral_iff.mpr ⟨x, rfl⟩

Integrality of Elements in Integral Closure

Informal description

Let $R$, $A$, and $B$ be commutative rings with algebra structures forming a tower $R \to A \to B$, and suppose $A$ is the integral closure of $R$ in $B$. Then every element $x \in A$ is integral over $R$.

IsIntegralClosure.isIntegral_algebra theorem

[Algebra R A] [IsScalarTower R A B] : Algebra.IsIntegral R A

Full source

theorem isIntegral_algebra [Algebra R A] [IsScalarTower R A B] : Algebra.IsIntegral R A :=
  ⟨fun x => IsIntegralClosure.isIntegral R B x⟩

Integrality of the Integral Closure Algebra

Informal description

Let $R$, $A$, and $B$ be commutative rings with algebra structures forming a tower $R \to A \to B$, and suppose $A$ is the integral closure of $R$ in $B$. Then the $R$-algebra $A$ is integral, meaning every element of $A$ is integral over $R$.

IsIntegralClosure.noZeroSMulDivisors theorem

[SMul R A] [IsScalarTower R A B] [NoZeroSMulDivisors R B] : NoZeroSMulDivisors R A

Full source

theorem noZeroSMulDivisors [SMul R A] [IsScalarTower R A B] [NoZeroSMulDivisors R B] :
    NoZeroSMulDivisors R A := by
  refine
    Function.Injective.noZeroSMulDivisors _ (IsIntegralClosure.algebraMap_injective A R B)
      (map_zero _) fun _ _ => ?_
  simp only [Algebra.algebraMap_eq_smul_one, IsScalarTower.smul_assoc]

Integral Closure Preserves No Zero Scalar Divisors Property

Informal description

Let $R$, $A$, and $B$ be commutative rings with $A$ being the integral closure of $R$ in $B$. Suppose $B$ has no zero scalar divisors over $R$ (i.e., for any $r \in R$ and $b \in B$, $r \cdot b = 0$ implies $r = 0$ or $b = 0$). Then $A$ also has no zero scalar divisors over $R$.

IsIntegralClosure.mk' definition

(x : B) (hx : IsIntegral R x) : A

Full source

/-- If `x : B` is integral over `R`, then it is an element of the integral closure of `R` in `B`. -/
noncomputable def mk' (x : B) (hx : IsIntegral R x) : A :=
  Classical.choose (isIntegral_iff.mp hx)

Construction of integral closure element from integral element

Informal description

Given an element $ x $ of $ B $ that is integral over $ R $, the function `mk'` constructs the corresponding element in the integral closure $ A $ of $ R $ in $ B $. This satisfies the property that the algebra map from $ A $ to $ B $ applied to `mk' A x hx` returns $ x $.

IsIntegralClosure.algebraMap_mk' theorem

(x : B) (hx : IsIntegral R x) : algebraMap A B (mk' A x hx) = x

Full source

@[simp]
theorem algebraMap_mk' (x : B) (hx : IsIntegral R x) : algebraMap A B (mk' A x hx) = x :=
  Classical.choose_spec (isIntegral_iff.mp hx)

Algebra Map Preserves Integral Closure Construction

Informal description

Let $A$ be the integral closure of a commutative ring $R$ in a commutative ring $B$, with algebra structures $R \to B$ and $A \to B$. For any element $x \in B$ that is integral over $R$, the algebra map $\text{algebraMap}_{A \to B}$ applied to the constructed element $\text{mk'}_A(x, hx)$ equals $x$, i.e., \[ \text{algebraMap}_{A \to B}(\text{mk'}_A(x, hx)) = x. \]

IsIntegralClosure.mk'_add theorem

(x y : B) (hx : IsIntegral R x) (hy : IsIntegral R y) : mk' A (x + y) (hx.add hy) = mk' A x hx + mk' A y hy

Full source

theorem mk'_add (x y : B) (hx : IsIntegral R x) (hy : IsIntegral R y) :
    mk' A (x + y) (hx.add hy) = mk' A x hx + mk' A y hy :=
  algebraMap_injective A R B <| by simp only [algebraMap_mk', RingHom.map_add]

Additivity of Integral Closure Construction: $\text{mk'}_A(x+y) = \text{mk'}_A(x) + \text{mk'}_A(y)$

Informal description

Let $A$ be the integral closure of a commutative ring $R$ in a commutative ring $B$, with algebra structures $R \to B$ and $A \to B$. For any elements $x, y \in B$ that are integral over $R$, the construction of their sum in $A$ via `mk'` satisfies: \[ \text{mk'}_A(x + y, hx + hy) = \text{mk'}_A(x, hx) + \text{mk'}_A(y, hy), \] where $hx$ and $hy$ are proofs that $x$ and $y$ are integral over $R$, respectively.

IsIntegralClosure.mk'_mul theorem

(x y : B) (hx : IsIntegral R x) (hy : IsIntegral R y) : mk' A (x * y) (hx.mul hy) = mk' A x hx * mk' A y hy

Full source

theorem mk'_mul (x y : B) (hx : IsIntegral R x) (hy : IsIntegral R y) :
    mk' A (x * y) (hx.mul hy) = mk' A x hx * mk' A y hy :=
  algebraMap_injective A R B <| by simp only [algebraMap_mk', RingHom.map_mul]

Multiplicativity of Integral Closure Construction

Informal description

Let $A$ be the integral closure of a commutative ring $R$ in a commutative ring $B$, with algebra structures $R \to B$ and $A \to B$. For any elements $x, y \in B$ that are integral over $R$, the constructed element $\text{mk'}_A(x \cdot y, hx \cdot hy)$ in $A$ equals the product of the constructed elements $\text{mk'}_A(x, hx)$ and $\text{mk'}_A(y, hy)$, i.e., \[ \text{mk'}_A(x \cdot y, hx \cdot hy) = \text{mk'}_A(x, hx) \cdot \text{mk'}_A(y, hy). \]

IsIntegralClosure.isField theorem

[Algebra R A] [IsScalarTower R A B] [IsDomain A] (hR : IsField R) : IsField A

Full source

/-- The integral closure of a field in a commutative domain is always a field. -/
theorem isField [Algebra R A] [IsScalarTower R A B] [IsDomain A] (hR : IsField R) :
    IsField A :=
  have := IsIntegralClosure.isIntegral_algebra R (A := A) B
  isField_of_isIntegral_of_isField' hR

Integral closure of a field is a field

Informal description

Let $R$ be a commutative ring, $A$ be a commutative domain, and $B$ be a commutative ring with algebra structures forming a tower $R \to A \to B$. If $A$ is the integral closure of $R$ in $B$ and $R$ is a field, then $A$ is also a field.

IsIntegralClosure.lift definition

: S →ₐ[R] A

Full source

/-- If `B / S / R` is a tower of ring extensions where `S` is integral over `R`,
then `S` maps (uniquely) into an integral closure `B / A / R`. -/
noncomputable def lift : S →ₐ[R] A where
  toFun x := mk' A (algebraMap S B x) (IsIntegral.algebraMap
    (Algebra.IsIntegral.isIntegral (R := R) x))
  map_one' := by simp only [RingHom.map_one, mk'_one]
  map_zero' := by simp only [RingHom.map_zero, mk'_zero]
  map_add' x y := by simp_rw [← mk'_add, map_add]
  map_mul' x y := by simp_rw [← mk'_mul, RingHom.map_mul]
  commutes' x := by simp_rw [← IsScalarTower.algebraMap_apply, mk'_algebraMap]

Lift of integral elements to integral closure

Informal description

Given a tower of ring extensions $ B / S / R $ where $ S $ is integral over $ R $, the function `lift` constructs a unique $ R $-algebra homomorphism from $ S $ to the integral closure $ A $ of $ R $ in $ B $. This homomorphism satisfies the property that the composition of the algebra map from $ A $ to $ B $ with `lift` equals the algebra map from $ S $ to $ B $.

IsIntegralClosure.algebraMap_lift theorem

(x : S) : algebraMap A B (lift R A B x) = algebraMap S B x

Full source

@[simp]
theorem algebraMap_lift (x : S) : algebraMap A B (lift R A B x) = algebraMap S B x :=
  algebraMap_mk' A (algebraMap S B x) (IsIntegral.algebraMap
    (Algebra.IsIntegral.isIntegral (R := R) x))

Commutativity of Integral Closure Lift with Algebra Maps

Informal description

Let $R$, $A$, $B$, and $S$ be commutative rings with appropriate algebra structures such that $A$ is the integral closure of $R$ in $B$. For any element $x \in S$, the following diagram commutes: \[ \text{algebraMap}_{A \to B}(\text{lift}_{R,A,B}(x)) = \text{algebraMap}_{S \to B}(x). \]

IsIntegralClosure.equiv definition

: A ≃ₐ[R] A'

Full source

/-- Integral closures are all isomorphic to each other. -/
noncomputable def equiv : A ≃ₐ[R] A' :=
  AlgEquiv.ofAlgHom
    (lift R A' B (isIntegral := isIntegral_algebra R B))
    (lift R A B (isIntegral := isIntegral_algebra R B))
    (by ext x; apply algebraMap_injective A' R B; simp)
    (by ext x; apply algebraMap_injective A R B; simp)

Equivalence of Integral Closures

Informal description

The equivalence of integral closures states that if $ A $ and $ A' $ are both integral closures of a commutative ring $ R $ in a commutative ring $ B $, then there exists an $ R $-algebra isomorphism between $ A $ and $ A' $. This isomorphism is constructed using the lift maps from $ A $ to $ A' $ and vice versa, and it commutes with the respective algebra maps into $ B $.

IsIntegralClosure.algebraMap_equiv theorem

(x : A) : algebraMap A' B (equiv R A B A' x) = algebraMap A B x

Full source

@[simp]
theorem algebraMap_equiv (x : A) : algebraMap A' B (equiv R A B A' x) = algebraMap A B x :=
  algebraMap_lift R A' B (isIntegral := isIntegral_algebra R B) x

Commutativity of Integral Closure Equivalence with Algebra Maps

Informal description

Let $R$, $A$, $A'$, and $B$ be commutative rings with appropriate algebra structures such that both $A$ and $A'$ are integral closures of $R$ in $B$. For any element $x \in A$, the following diagram commutes: \[ \text{algebraMap}_{A' \to B}(\text{equiv}_{R,A,B,A'}(x)) = \text{algebraMap}_{A \to B}(x). \]

isIntegral_trans theorem

[Algebra.IsIntegral R A] (x : B) (hx : IsIntegral A x) : IsIntegral R x

Full source

/-- If A is an R-algebra all of whose elements are integral over R,
and x is an element of an A-algebra that is integral over A, then x is integral over R. -/
theorem isIntegral_trans [Algebra.IsIntegral R A] (x : B) (hx : IsIntegral A x) :
    IsIntegral R x := by
  rcases hx with ⟨p, pmonic, hp⟩
  let S := adjoin R (p.coeffs : Set A)
  have : Module.Finite R S := ⟨(Subalgebra.toSubmodule S).fg_top.mpr <|
    fg_adjoin_of_finite p.coeffs.finite_toSet fun a _ ↦ Algebra.IsIntegral.isIntegral a⟩
  let p' : S[X] := p.toSubring S.toSubring subset_adjoin
  have hSx : IsIntegral S x := ⟨p', (p.monic_toSubring _ _).mpr pmonic, by
    rw [IsScalarTower.algebraMap_eq S A B, ← eval₂_map]
    convert hp; apply p.map_toSubring S.toSubring⟩
  let Sx := Subalgebra.toSubmodule (adjoin S {x})
  let MSx : Module S Sx := SMulMemClass.toModule _ -- the next line times out without this
  have : Module.Finite S Sx := ⟨(Submodule.fg_top _).mpr hSx.fg_adjoin_singleton⟩
  refine .of_mem_of_fg ((adjoin S {x}).restrictScalars R) ?_ _
    ((Subalgebra.mem_restrictScalars R).mpr <| subset_adjoin rfl)
  rw [← Submodule.fg_top, ← Module.finite_def]
  letI : SMul S Sx := { MSx with } -- need this even though MSx is there
  have : IsScalarTower R S Sx :=
    Submodule.isScalarTower Sx -- Lean looks for `Module A Sx` without this
  exact Module.Finite.trans S Sx

Transitivity of Integral Elements: $A/R$ integral and $x$ integral over $A$ implies $x$ integral over $R$

Informal description

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

Algebra.IsIntegral.trans theorem

[Algebra.IsIntegral R A] [Algebra.IsIntegral A B] : Algebra.IsIntegral R B

Full source

/-- If A is an R-algebra all of whose elements are integral over R,
and B is an A-algebra all of whose elements are integral over A,
then all elements of B are integral over R. -/
protected theorem Algebra.IsIntegral.trans
    [Algebra.IsIntegral R A] [Algebra.IsIntegral A B] : Algebra.IsIntegral R B :=
  ⟨fun x ↦ isIntegral_trans x (Algebra.IsIntegral.isIntegral (R := A) x)⟩

Transitivity of Integral Algebras: $A/R$ and $B/A$ integral implies $B/R$ integral

Informal description

Let $R$ be a commutative ring, $A$ an $R$-algebra where every element is integral over $R$, and $B$ an $A$-algebra where every element is integral over $A$. Then every element of $B$ is integral over $R$.

RingHom.IsIntegral.trans theorem

(hf : f.IsIntegral) (hg : g.IsIntegral) : (g.comp f).IsIntegral

Full source

protected theorem RingHom.IsIntegral.trans
    (hf : f.IsIntegral) (hg : g.IsIntegral) : (g.comp f).IsIntegral :=
  let _ := f.toAlgebra; let _ := g.toAlgebra; let _ := (g.comp f).toAlgebra
  have : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq fun _ ↦ rfl
  have : Algebra.IsIntegral R S := ⟨hf⟩
  have : Algebra.IsIntegral S T := ⟨hg⟩
  have : Algebra.IsIntegral R T := Algebra.IsIntegral.trans S
  Algebra.IsIntegral.isIntegral

Transitivity of Integral Ring Homomorphisms: $ g \circ f $ is integral when $ f $ and $ g $ are integral

Informal description

Let $ f: R \to A $ and $ g: A \to B $ be integral ring homomorphisms. Then the composition $ g \circ f: R \to B $ is also an integral ring homomorphism.

IsIntegralClosure.tower_top theorem

 {B C : Type*} [CommSemiring C] [CommRing B] [Algebra R B] [Algebra A B] [Algebra C B] [IsScalarTower R A B]
  [IsIntegralClosure C R B] [Algebra.IsIntegral R A] : IsIntegralClosure C A B

Full source

/-- If `R → A → B` is an algebra tower, `C` is the integral closure of `R` in `B`
and `A` is integral over `R`, then `C` is the integral closure of `A` in `B`. -/
lemma IsIntegralClosure.tower_top {B C : Type*} [CommSemiring C] [CommRing B]
    [Algebra R B] [Algebra A B] [Algebra C B] [IsScalarTower R A B]
    [IsIntegralClosure C R B] [Algebra.IsIntegral R A] :
    IsIntegralClosure C A B :=
  ⟨IsIntegralClosure.algebraMap_injective _ R _,
   fun hx => (IsIntegralClosure.isIntegral_iff).mp (isIntegral_trans (R := R) _ hx),
   fun hx => ((IsIntegralClosure.isIntegral_iff (R := R)).mpr hx).tower_top⟩

Integral Closure in Tower: $C$ is Integral Closure of $A$ in $B$ when $A$ is Integral over $R$

Informal description

Let $R \to A \to B$ be an algebra tower, where $A$ is an integral $R$-algebra and $C$ is the integral closure of $R$ in $B$. Then $C$ is also the integral closure of $A$ in $B$.

RingHom.isIntegral_of_surjective theorem

(hf : Function.Surjective f) : f.IsIntegral

Full source

theorem RingHom.isIntegral_of_surjective (hf : Function.Surjective f) : f.IsIntegral :=
  fun x ↦ (hf x).recOn fun _y hy ↦ hy ▸ f.isIntegralElem_map

Surjective Ring Homomorphisms are Integral

Informal description

If a ring homomorphism $f: R \to A$ is surjective, then $f$ is integral, meaning every element of $A$ is integral over $R$ with respect to $f$.

Algebra.isIntegral_of_surjective theorem

(h : Function.Surjective (algebraMap R A)) : Algebra.IsIntegral R A

Full source

theorem Algebra.isIntegral_of_surjective (h : Function.Surjective (algebraMap R A)) :
    Algebra.IsIntegral R A :=
  ⟨(algebraMap R A).isIntegral_of_surjective h⟩

Integrality of Surjective Algebra Maps

Informal description

If the algebra map from $R$ to $A$ is surjective, then every element of $A$ is integral over $R$.

IsIntegral.tower_bot theorem

(H : Function.Injective (algebraMap A B)) {x : A} (h : IsIntegral R (algebraMap A B x)) : IsIntegral R x

Full source

/-- If `R → A → B` is an algebra tower with `A → B` injective,
then if the entire tower is an integral extension so is `R → A` -/
theorem IsIntegral.tower_bot (H : Function.Injective (algebraMap A B)) {x : A}
    (h : IsIntegral R (algebraMap A B x)) : IsIntegral R x :=
  (isIntegral_algHom_iff (IsScalarTower.toAlgHom R A B) H).mp h

Integrality descends in injective algebra towers ($R \to A \to B$)

Informal description

Let $R \to A \to B$ be a tower of algebra maps where $A \to B$ is injective. If an element $x \in A$ has the property that its image in $B$ is integral over $R$, then $x$ itself is integral over $R$.

RingHom.IsIntegral.tower_bot theorem

(hg : Function.Injective g) (hfg : (g.comp f).IsIntegral) : f.IsIntegral

Full source

nonrec theorem RingHom.IsIntegral.tower_bot (hg : Function.Injective g)
    (hfg : (g.comp f).IsIntegral) : f.IsIntegral :=
  letI := f.toAlgebra; letI := g.toAlgebra; letI := (g.comp f).toAlgebra
  haveI : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq fun _ ↦ rfl
  fun x ↦ IsIntegral.tower_bot hg (hfg (g x))

Integrality descends through injective ring homomorphisms

Informal description

Let $f \colon R \to S$ and $g \colon S \to T$ be ring homomorphisms with $g$ injective. If the composition $g \circ f \colon R \to T$ is integral, then $f$ is integral.

Algebra.IsIntegral.tower_bot theorem

 [Algebra R S] [Algebra R T] [Algebra S T] [NoZeroSMulDivisors S T] [Nontrivial T] [IsScalarTower R S T]
  [h : Algebra.IsIntegral R T] : Algebra.IsIntegral R S

Full source

/-- Let `T / S / R` be a tower of algebras, `T` is non-trivial and is a torsion free `S`-module,
  then if `T` is an integral `R`-algebra, then `S` is an integral `R`-algebra. -/
theorem Algebra.IsIntegral.tower_bot [Algebra R S] [Algebra R T] [Algebra S T]
    [NoZeroSMulDivisors S T] [Nontrivial T] [IsScalarTower R S T]
    [h : Algebra.IsIntegral R T] : Algebra.IsIntegral R S where
  isIntegral := by
    apply RingHom.IsIntegral.tower_bot (algebraMap R S) (algebraMap S T)
      (FaithfulSMul.algebraMap_injective S T)
    rw [← IsScalarTower.algebraMap_eq R S T]
    exact h.isIntegral

Integrality descends in scalar towers ($R \to S \to T$)

Informal description

Let $R \to S \to T$ be a tower of algebra maps, where $T$ is a nontrivial $S$-algebra with no zero divisors under scalar multiplication by $S$, and the composition forms a scalar tower. If $T$ is integral over $R$, then $S$ is integral over $R$.

IsIntegral.tower_bot_of_field theorem

 {R A B : Type*} [CommRing R] [Field A] [Ring B] [Nontrivial B] [Algebra R A] [Algebra A B] [Algebra R B]
  [IsScalarTower R A B] {x : A} (h : IsIntegral R (algebraMap A B x)) : IsIntegral R x

Full source

theorem IsIntegral.tower_bot_of_field {R A B : Type*} [CommRing R] [Field A]
    [Ring B] [Nontrivial B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B]
    {x : A} (h : IsIntegral R (algebraMap A B x)) : IsIntegral R x :=
  h.tower_bot (algebraMap A B).injective

Integrality descends in field extensions of scalar towers

Informal description

Let $R$ be a commutative ring, $A$ a field, and $B$ a nontrivial ring, with algebra structures $R \to A \to B$ forming a scalar tower. For any element $x \in A$, if the image of $x$ in $B$ is integral over $R$, then $x$ itself is integral over $R$.

RingHom.isIntegralElem.of_comp theorem

{x : T} (h : (g.comp f).IsIntegralElem x) : g.IsIntegralElem x

Full source

theorem RingHom.isIntegralElem.of_comp {x : T} (h : (g.comp f).IsIntegralElem x) :
    g.IsIntegralElem x :=
  let ⟨p, hp, hp'⟩ := h
  ⟨p.map f, hp.map f, by rwa [← eval₂_map] at hp'⟩

Integrality through Composition of Ring Homomorphisms

Informal description

Let $ f: R \to S $ and $ g: S \to T $ be ring homomorphisms. For any element $ x \in T $, if $ x $ is integral over $ R $ with respect to the composition $ g \circ f $, then $ x $ is integral over $ S $ with respect to $ g $.

RingHom.IsIntegral.tower_top theorem

(h : (g.comp f).IsIntegral) : g.IsIntegral

Full source

theorem RingHom.IsIntegral.tower_top (h : (g.comp f).IsIntegral) : g.IsIntegral :=
  fun x ↦ RingHom.isIntegralElem.of_comp f g (h x)

Integrality of Composition Implies Integrality of Second Homomorphism

Informal description

Let $ f: R \to S $ and $ g: S \to T $ be ring homomorphisms. If the composition $ g \circ f $ is integral, then $ g $ is integral.

Algebra.IsIntegral.tower_top theorem

[Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] [h : Algebra.IsIntegral R T] : Algebra.IsIntegral S T

Full source

/-- Let `T / S / R` be a tower of algebras, `T` is an integral `R`-algebra, then it is integral
  as an `S`-algebra. -/
theorem Algebra.IsIntegral.tower_top [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T]
    [h : Algebra.IsIntegral R T] : Algebra.IsIntegral S T where
  isIntegral := by
    apply RingHom.IsIntegral.tower_top (algebraMap R S) (algebraMap S T)
    rw [← IsScalarTower.algebraMap_eq R S T]
    exact h.isIntegral

Integrality in Tower of Algebras: Top Extension Preserves Integrality

Informal description

Let $R \to S \to T$ be a tower of algebras where $T$ is integral over $R$. Then $T$ is also integral over $S$.

RingHom.IsIntegral.quotient theorem

{I : Ideal S} (hf : f.IsIntegral) : (Ideal.quotientMap I f le_rfl).IsIntegral

Full source

theorem RingHom.IsIntegral.quotient {I : Ideal S} (hf : f.IsIntegral) :
    (Ideal.quotientMap I f le_rfl).IsIntegral := by
  rintro ⟨x⟩
  obtain ⟨p, p_monic, hpx⟩ := hf x
  refine ⟨p.map (Ideal.Quotient.mk _), p_monic.map _, ?_⟩
  simpa only [hom_eval₂, eval₂_map] using congr_arg (Ideal.Quotient.mk I) hpx

Integrality is preserved under quotient maps

Informal description

Let $f: R \to S$ be an integral ring homomorphism and $I$ be an ideal of $S$. Then the quotient map $\bar{f}: R \to S/I$ induced by $f$ is also integral.

instIsIntegralQuotientIdeal instance

{I : Ideal A} [Algebra.IsIntegral R A] : Algebra.IsIntegral R (A ⧸ I)

Full source

instance {I : Ideal A} [Algebra.IsIntegral R A] : Algebra.IsIntegral R (A ⧸ I) :=
  Algebra.IsIntegral.trans A

Integrality of Quotient Algebras over Base Rings

Informal description

For any commutative ring $R$ and $R$-algebra $A$ that is integral over $R$, and any ideal $I$ of $A$, the quotient algebra $A/I$ is integral over $R$.

Algebra.IsIntegral.quotient instance

{I : Ideal A} [Algebra.IsIntegral R A] : Algebra.IsIntegral (R ⧸ I.comap (algebraMap R A)) (A ⧸ I)

Full source

instance Algebra.IsIntegral.quotient {I : Ideal A} [Algebra.IsIntegral R A] :
    Algebra.IsIntegral (R ⧸ I.comap (algebraMap R A)) (A ⧸ I) :=
  ⟨RingHom.IsIntegral.quotient (algebraMap R A) Algebra.IsIntegral.isIntegral⟩

Integrality of Quotient Algebras over Quotient Rings

Informal description

Let $R$ be a commutative ring and $A$ an $R$-algebra that is integral over $R$. For any ideal $I$ of $A$, the quotient algebra $A/I$ is integral over the quotient ring $R/(I \cap R)$, where $I \cap R$ denotes the contraction of $I$ under the algebra map $R \to A$.

isIntegral_quotientMap_iff theorem

 {I : Ideal S} : (Ideal.quotientMap I f le_rfl).IsIntegral ↔ ((Ideal.Quotient.mk I).comp f : R →+* S ⧸ I).IsIntegral

Full source

theorem isIntegral_quotientMap_iff {I : Ideal S} :
    (Ideal.quotientMap I f le_rfl).IsIntegral ↔
      ((Ideal.Quotient.mk I).comp f : R →+* S ⧸ I).IsIntegral := by
  let g := Ideal.Quotient.mk (I.comap f)
  -- Porting note: added type ascription
  have : (Ideal.quotientMap I f le_rfl).comp g = (Ideal.Quotient.mk I).comp f :=
    Ideal.quotientMap_comp_mk le_rfl
  refine ⟨fun h => ?_, fun h => RingHom.IsIntegral.tower_top g _ (this ▸ h)⟩
  refine this ▸ RingHom.IsIntegral.trans g (Ideal.quotientMap I f le_rfl) ?_ h
  exact g.isIntegral_of_surjective Ideal.Quotient.mk_surjective

Integrality of Quotient Map vs. Composition with Quotient

Informal description

Let $f: R \to S$ be a ring homomorphism and $I$ an ideal of $S$. The quotient map $\text{quotientMap}_I f$ is integral if and only if the composition of $f$ with the canonical quotient map $S \to S/I$ is integral.

isField_of_isIntegral_of_isField theorem

 {R S : Type*} [CommRing R] [CommRing S] [Algebra R S] [Algebra.IsIntegral R S]
  (hRS : Function.Injective (algebraMap R S)) (hS : IsField S) : IsField R

Full source

/-- If the integral extension `R → S` is injective, and `S` is a field, then `R` is also a field. -/
theorem isField_of_isIntegral_of_isField {R S : Type*} [CommRing R] [CommRing S]
    [Algebra R S] [Algebra.IsIntegral R S]
    (hRS : Function.Injective (algebraMap R S)) (hS : IsField S) : IsField R := by
  have := hS.nontrivial; have := Module.nontrivial R S
  refine ⟨⟨0, 1, zero_ne_one⟩, mul_comm, fun {a} ha ↦ ?_⟩
  -- Let `a_inv` be the inverse of `algebraMap R S a`,
  -- then we need to show that `a_inv` is of the form `algebraMap R S b`.
  obtain ⟨a_inv, ha_inv⟩ := hS.mul_inv_cancel fun h ↦ ha (hRS (h.trans (RingHom.map_zero _).symm))
  letI : Invertible a_inv := (Units.mkOfMulEqOne a_inv _ <| mul_comm _ a_inv ▸ ha_inv).invertible
  -- Let `p : R[X]` be monic with root `a_inv`,
  obtain ⟨p, p_monic, hp⟩ := Algebra.IsIntegral.isIntegral (R := R) a_inv
  -- and `q` be `p` with coefficients reversed (so `q(a) = q'(a) * a + 1`).
  -- We have `q(a) = 0`, so `-q'(a)` is the inverse of `a`.
  use -p.reverse.divX.eval a -- -q'(a)
  nth_rewrite 1 [mul_neg, ← eval_X (x := a), ← eval_mul, ← p_monic, ← coeff_zero_reverse,
    ← add_eq_zero_iff_neg_eq, ← eval_C (a := p.reverse.coeff 0), ← eval_add, X_mul_divX_add,
    ← (injective_iff_map_eq_zero' _).mp hRS, ← aeval_algebraMap_apply_eq_algebraMap_eval]
  rwa [← eval₂_reverse_eq_zero_iff] at hp

Field Property Lifting via Injective Integral Extension

Informal description

Let $R$ and $S$ be commutative rings with $S$ being an integral extension of $R$ via an injective algebra map $R \to S$. If $S$ is a field, then $R$ is also a field.

Algebra.IsIntegral.isField_iff_isField theorem

 {R S : Type*} [CommRing R] [CommRing S] [IsDomain S] [Algebra R S] [Algebra.IsIntegral R S]
  (hRS : Function.Injective (algebraMap R S)) : IsField R ↔ IsField S

Full source

theorem Algebra.IsIntegral.isField_iff_isField {R S : Type*} [CommRing R]
    [CommRing S] [IsDomain S] [Algebra R S] [Algebra.IsIntegral R S]
    (hRS : Function.Injective (algebraMap R S)) : IsFieldIsField R ↔ IsField S :=
  ⟨isField_of_isIntegral_of_isField', isField_of_isIntegral_of_isField hRS⟩

Equivalence of Field Properties in Integral Extensions with Injective Maps

Informal description

Let $R$ and $S$ be commutative rings with $S$ being an integral domain and an integral $R$-algebra via an injective algebra map $R \to S$. Then $R$ is a field if and only if $S$ is a field.

integralClosure_idem theorem

{R A : Type*} [CommRing R] [CommRing A] [Algebra R A] : integralClosure (integralClosure R A) A = ⊥

Full source

theorem integralClosure_idem {R A : Type*} [CommRing R] [CommRing A] [Algebra R A] :
    integralClosure (integralClosure R A) A = ⊥ :=
  letI := (integralClosure R A).algebra
  eq_bot_iff.2 fun x hx ↦ Algebra.mem_bot.2
    ⟨⟨x, isIntegral_trans (A := integralClosure R A) x hx⟩, rfl⟩

Idempotence of Integral Closure: $\text{integralClosure}(\text{integralClosure}(R, A), A) = \bot$

Informal description

Let $R$ be a commutative ring and $A$ an $R$-algebra. The integral closure of the integral closure of $R$ in $A$ (i.e., $\text{integralClosure}(\text{integralClosure}(R, A), A)$) is equal to the bottom subalgebra $\bot$ (the smallest subalgebra containing only the images of the algebra maps from $R$).

instIsDomainSubtypeMemSubalgebraIntegralClosure instance

: IsDomain (integralClosure R S)

Full source

instance : IsDomain (integralClosure R S) :=
  inferInstance

Integral Closure is an Integral Domain

Informal description

The integral closure of a commutative ring $R$ in an $R$-algebra $S$ is an integral domain.

roots_mem_integralClosure theorem

{f : R[X]} (hf : f.Monic) {a : S} (ha : a ∈ f.aroots S) : a ∈ integralClosure R S

Full source

theorem roots_mem_integralClosure {f : R[X]} (hf : f.Monic) {a : S}
    (ha : a ∈ f.aroots S) : a ∈ integralClosure R S :=
  ⟨f, hf, (eval₂_eq_eval_map _).trans <| (mem_roots <| (hf.map _).ne_zero).1 ha⟩

Roots of monic polynomials are integral

Informal description

Let $R$ be a commutative ring and $S$ an $R$-algebra. For any monic polynomial $f \in R[X]$ and any element $a \in S$ that is a root of $f$ in $S$ (i.e., $a$ belongs to the multiset of roots of $f$ in $S$), $a$ is integral over $R$ (i.e., $a$ belongs to the integral closure of $R$ in $S$).