Theorems · Definition · commutative algebra

TensorProduct.toIntegralClosure

(R : Type u_1) →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (B : Type u_4) →
            [inst_3 : CommRing B] →
              [inst_4 : Algebra R B] →
                TensorProduct R S ↥(integralClosure R B) →ₐ[S] ↥(integralClosure S (TensorProduct R S B))

The comparison map from S ⊗[R] integralClosure R B to integralClosure S (S ⊗[R] B). This is injective when S is R-flat, and (TODO) bijective when S is R-smooth.

Defined in

Mathlib.RingTheory.Smooth.IntegralClosure

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraCommRingAlgebra