The diagonal of an unramified algebra

For an essentially finite type, formally unramified algebra S over R, the kernel of the multiplication map S ⊗[R] S → S is generated by an idempotent. This is the algebraic form of the fact that the diagonal of an unramified morphism of affine schemes is both open and closed.

Consequently, two algebra maps f, g : S → T become equal after any further map inverting the complement of the image of this idempotent under f ⊗ g. If they agree modulo an ideal in the Jacobson radical of T, then they agree already in T. In particular, residue sections over a henselian pair have at most one lift, without any completeness or nilpotence hypothesis.

The complementary idempotent, Mathlib's Algebra.FormallyUnramified.elem, is characterised by the two properties defining it: it annihilates every 1 ⊗ s - s ⊗ 1 and multiplies to 1 (TauCeti.Algebra.FormallyUnramified.eq_elem). This makes it computable in examples, and shows that it is invariant under the swap of the two tensor factors. For the split algebra κ → R it is ∑ₖ eₖ ⊗ eₖ, the indicator of the diagonal of κ × κ.

For an unramified quotient S = W ⧸ I over R, Mathlib's diagonal element of S ⊗[R] S lifts to some t ∈ S ⊗[R] W which annihilates the difference of the two images 1 ⊗ w and (w mod I) ⊗ 1 of every w ∈ W modulo the extension of I to S ⊗[R] W. Thus these images become congruent modulo this ideal after inverting t (exists_mul_tmul_sub_mem_map_includeRight).

References

• Stacks Project, Tag 02FL
• The Stacks Project, Lemma 15.11.5 (uniqueness of sections over a henselian pair).
• exists_isIdempotentElem_ker_lmul_eq_span extracts, as a standalone statement, the idempotent-generator step at the start of the proof of Mathlib's Algebra.FormallyUnramified.exists_algEquiv_prod, and follows the same argument.

theorem TauCeti.Algebra.FormallyUnramified.exists_isIdempotentElem_ker_lmul_eq_span (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [Algebra.EssFiniteType R S] [Algebra.FormallyUnramified R S] : ∃ (e : TensorProduct R S S), IsIdempotentElem e ∧ RingHom.ker (Algebra.TensorProduct.lmul' R).toRingHom = Ideal.span {e}

The kernel of multiplication on the self-tensor product of an essentially finite type, formally unramified algebra is generated by an idempotent.

This is the first step of the proof of Mathlib's Algebra.FormallyUnramified.exists_algEquiv_prod, stated on its own.

theorem TauCeti.Algebra.FormallyUnramified.comp_eq_comp_of_isUnit_one_sub_productMap {R : Type u_1} {S : Type u_2} {T : Type u_3} {U : Type u_4} [CommSemiring R] [CommRing S] [CommRing T] [Ring U] [Algebra R S] [Algebra R T] [Algebra R U] {e : TensorProduct R S S} (he : IsIdempotentElem e) (hker : RingHom.ker (Algebra.TensorProduct.lmul' R).toRingHom ≤ Ideal.span {e}) (f g : S →ₐ[R] T) (h : T →ₐ[R] U) (hu : IsUnit (h (1 - (Algebra.TensorProduct.productMap f g) e))) : h.comp f = h.comp g

If the kernel of multiplication S ⊗[R] S → S is contained in the ideal generated by an idempotent e, then two algebra maps f, g : S → T agree after composing with any map h that inverts 1 - (f ⊗ g) e. The target of h need not be commutative.

theorem TauCeti.Algebra.FormallyUnramified.ext_of_quotient_eq (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [Algebra.EssFiniteType R S] [Algebra.FormallyUnramified R S] {T : Type u_3} [CommRing T] [Algebra R T] (J : Ideal T) (hJ : J ≤ ⊥.jacobson) {f g : S →ₐ[R] T} (hfg : (Ideal.Quotient.mkₐ R J).comp f = (Ideal.Quotient.mkₐ R J).comp g) : f = g

Maps out of an essentially finite type unramified algebra are determined modulo any ideal contained in the target's Jacobson radical.

theorem TauCeti.Algebra.FormallyUnramified.eq_elem {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Algebra.EssFiniteType R S] [Algebra.FormallyUnramified R S] {t : TensorProduct R S S} (ht : ∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * t = 0) (h1 : (Algebra.TensorProduct.lmul' R) t = 1) : t = Algebra.FormallyUnramified.elem R S

The diagonal idempotent of an essentially finite type, formally unramified algebra is the only element of S ⊗[R] S that annihilates every 1 ⊗ s - s ⊗ 1 and maps to 1 under multiplication. Mathlib's Algebra.FormallyUnramified.elem is a choice of such an element; this shows that the choice does not matter.

@[simp]

theorem TauCeti.Algebra.FormallyUnramified.comm_elem (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [Algebra.EssFiniteType R S] [Algebra.FormallyUnramified R S] : (Algebra.TensorProduct.comm R S S) (Algebra.FormallyUnramified.elem R S) = Algebra.FormallyUnramified.elem R S

The diagonal idempotent of an essentially finite type, formally unramified algebra is invariant under exchanging the two tensor factors.

theorem TauCeti.Algebra.FormallyUnramified.elem_pi (R : Type u_1) (κ : Type u_2) [CommRing R] [Fintype κ] [DecidableEq κ] : Algebra.FormallyUnramified.elem R (κ → R) = ∑ k : κ, Pi.single k 1 ⊗ₜ[R] Pi.single k 1

The diagonal idempotent of the split algebra κ → R is ∑ₖ eₖ ⊗ eₖ, for the standard idempotents eₖ of κ → R.

theorem TauCeti.Algebra.FormallyUnramified.exists_mul_tmul_sub_mem_map_includeRight (A : Type u_1) {W : Type u_2} [CommRing A] [CommRing W] [Algebra A W] (I : Ideal W) [Algebra.FormallyUnramified A (W ⧸ I)] [Algebra.EssFiniteType A (W ⧸ I)] : ∃ (t : TensorProduct A (W ⧸ I) W), (Algebra.TensorProduct.lmul' A) ((Algebra.TensorProduct.map (AlgHom.id A (W ⧸ I)) (Ideal.Quotient.mkₐ A I)) t) = 1 ∧ ∀ (w : W), (1 ⊗ₜ[A] w - (Ideal.Quotient.mk I) w ⊗ₜ[A] 1) * t ∈ Ideal.map Algebra.TensorProduct.includeRight I

For a quotient S = W ⧸ I unramified over A, some t ∈ S ⊗[A] W maps to 1 on the diagonal and such that, for every w ∈ W, the product of t with the difference 1 ⊗ w - (w mod I) ⊗ 1 lies in the extension of I along includeRight. So the two images become congruent modulo this ideal after inverting t. It lifts the element of S ⊗[A] S given by Mathlib's Algebra.FormallyUnramified.iff_exists_tensorProduct.