Theorems · Definition · commutative algebra

Ideal.tensorCotangentEquiv

(R : Type u_1) →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (T : Type u_3) →
            [inst_3 : CommRing T] →
              [inst_4 : Algebra R T] →
                (I : Ideal S) →
                  [Module.Flat R T] →
                    TensorProduct R T I.Cotangent ≃ₗ[T]
                      (Ideal.map Algebra.TensorProduct.includeRight.toRingHom I).Cotangent

If T is a flat R-module, the base change of the cotangent space of I is linearly equivalent to the cotangent space of the extended ideal I · (T ⊗[R] S).

Defined in

Mathlib.RingTheory.Ideal.CotangentBaseChange

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraCommRingAlgebraModule.Flat