Almost integral elements

def IsAlmostIntegral (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (s : S) : Prop

An element s in an R-algebra is almost integral if there exists r ∈ R⁰ such that r • s ^ n ∈ R for all n.

def completeIntegralClosure (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] : Subalgebra R S

The complete integral closure is the subalgebra of almost integral elements.

theorem mem_completeIntegralClosure {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {x : S} : x ∈ completeIntegralClosure R S ↔ IsAlmostIntegral R x

theorem IsIntegral.isAlmostIntegral_of_exists_smul_mem_range {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {s : S} (H : IsIntegral R s) (h : ∃ t ∈ nonZeroDivisors R, t • s ∈ (algebraMap R S).range) : IsAlmostIntegral R s

theorem IsIntegral.isAlmostIntegral_of_isLocalization {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {s : S} (H : IsIntegral R s) (M : Submonoid R) (hM : M ≤ nonZeroDivisors R) [IsLocalization M S] : IsAlmostIntegral R s

theorem IsIntegral.isAlmostIntegral {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsFractionRing R S] {s : S} (H : IsIntegral R s) : IsAlmostIntegral R s

Stacks Tag 00GX (Part 2)

theorem integralClosure_le_completeIntegralClosure {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsFractionRing R S] : integralClosure R S ≤ completeIntegralClosure R S

theorem IsAlmostIntegral.isIntegral_of_nonZeroDivisors_le_comap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {s : S} (H : IsAlmostIntegral R s) [IsNoetherianRing R] (H' : nonZeroDivisors R ≤ Submonoid.comap (algebraMap R S) (nonZeroDivisors S)) : IsIntegral R s

theorem IsAlmostIntegral.isIntegral {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsNoetherianRing R] [IsDomain S] [FaithfulSMul R S] {s : S} (H : IsAlmostIntegral R s) : IsIntegral R s

Stacks Tag 00GX (Part 3)

theorem isAlmostIntegral_iff_isIntegral {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsNoetherianRing R] [IsDomain R] [IsFractionRing R S] {s : S} : IsAlmostIntegral R s ↔ IsIntegral R s

theorem completeIntegralClosure_eq_integralClosure {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [IsNoetherianRing R] [IsDomain R] [IsFractionRing R S] : completeIntegralClosure R S = integralClosure R S