Theorems · Definition · commutative algebra

Algebra.FormallyUnramified.elem

(R : Type u_1) →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] → [Algebra.FormallyUnramified R S] → [Algebra.EssFiniteType R S] → TensorProduct R S S

A finite-type R-algebra S is (formally) unramified iff there exists a t : S ⊗[R] S satisfying 1. t annihilates every 1 ⊗ s - s ⊗ 1. 2. the image of t is 1 under the map S ⊗[R] S → S. See Algebra.FormallyUnramified.iff_exists_tensorProduct. This is the choice of such a t.

Defined in

Mathlib.RingTheory.Unramified.Finite

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraAlgebra.FormallyUnramifiedAlgebra.EssFiniteType