Various results about unramified algebras

We prove various theorems about unramified algebras. In fact we work in the more general setting of formally unramified algebras which are essentially of finite type.

Main results

• Algebra.FormallyUnramified.iff_exists_tensorProduct: 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.
• Algebra.FormallyUnramified.finite_of_free: An unramified free algebra is finitely generated.
• Algebra.FormallyUnramified.flat_of_restrictScalars: If S is an unramified R-algebra, then R-flat implies S-flat.

References

• [B. Iversen, Generic Local Structure of the Morphisms in Commutative Algebra][iversen]

theorem Algebra.FormallyUnramified.iff_exists_tensorProduct {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [EssFiniteType R S] : FormallyUnramified R S ↔ ∃ (t : TensorProduct R S S), (∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * t = 0) ∧ (TensorProduct.lmul' R) t = 1

Proposition I.2.3 + I.2.6 of [iversen] 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.

theorem Algebra.FormallyUnramified.finite_of_free_aux {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (I : Type u_4) [DecidableEq I] (b : Module.Basis I R S) (f : I →₀ S) (x : S) (a : I → I →₀ R) (ha : a = fun (i : I) => b.repr (b i * x)) : (1 ⊗ₜ[R] x * f.sum fun (i : I) (y : S) => y ⊗ₜ[R] b i) = ∑ k ∈ f.support.biUnion fun (i : I) => (a i).support, (b.repr (f.sum fun (i : I) (y : S) => (a i) k • y)).sum fun (j : I) (c : R) => c • b j ⊗ₜ[R] b k

noncomputable def Algebra.FormallyUnramified.elem (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [FormallyUnramified R S] [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.

Equations

• Algebra.FormallyUnramified.elem R S = ⋯.choose

theorem Algebra.FormallyUnramified.one_tmul_sub_tmul_one_mul_elem {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [FormallyUnramified R S] [EssFiniteType R S] (s : S) : (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * elem R S = 0

theorem Algebra.FormallyUnramified.one_tmul_mul_elem {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [FormallyUnramified R S] [EssFiniteType R S] (s : S) : 1 ⊗ₜ[R] s * elem R S = s ⊗ₜ[R] 1 * elem R S

theorem Algebra.FormallyUnramified.lmul_elem {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [FormallyUnramified R S] [EssFiniteType R S] : (TensorProduct.lmul' R) (elem R S) = 1

theorem Algebra.FormallyUnramified.finite_of_free (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [FormallyUnramified R S] [EssFiniteType R S] [Module.Free R S] : Module.Finite R S

An unramified free algebra is finitely generated. Iversen I.2.8

noncomputable def Algebra.FormallyUnramified.sec (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (M : Type u_3) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] [FormallyUnramified R S] [EssFiniteType R S] : M →ₗ[S] TensorProduct R S M

Proposition I.2.3 of [iversen] If S is an unramified R-algebra, and M is a S-module, then the map S ⊗[R] M →ₗ[S] M taking (b, m) ↦ b • m admits a S-linear section.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebra.FormallyUnramified.comp_sec (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (M : Type u_3) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] [FormallyUnramified R S] [EssFiniteType R S] : TensorProduct.AlgebraTensorModule.lift (↑R (lsmul S S M).toLinearMap.flip).flip ∘ₗ sec R S M = LinearMap.id

theorem Algebra.FormallyUnramified.flat_of_restrictScalars (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (M : Type u_3) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] [FormallyUnramified R S] [EssFiniteType R S] [Module.Flat R M] : Module.Flat S M

If S is an unramified R-algebra, then R-flat implies S-flat. Iversen I.2.7

theorem Algebra.FormallyUnramified.projective_of_restrictScalars (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (M : Type u_3) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] [FormallyUnramified R S] [EssFiniteType R S] [Module.Projective R M] : Module.Projective S M

If S is an unramified R-algebra, then R-projective implies S-projective.