Theorems · Theorem · commutative algebra

mem_adjoin_map_integralClosure_of_isStandardEtale

∀ {R : Type u_1} {S : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [Algebra.IsStandardEtale R S] (a : TensorProduct R S B),
  IsIntegral S a → a ∈ Algebra.adjoin S ↑(Subalgebra.map Algebra.TensorProduct.includeRight (integralClosure R B))

[Stacks Tag 03GE](https://stacks.math.columbia.edu/tag/03GE) (without the generalization to arbitrary etale algebra)

Defined in

Mathlib.RingTheory.Smooth.IntegralClosure

Cited by

0 results in Mathlib

Foundations

Depth 144 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraCommRingAlgebraAlgebra.IsStandardEtale