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_2} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Algebra.EssFiniteType R S] : Algebra.FormallyUnramified R S ↔ ∃ (t : TensorProduct R S S), (∀ (s : S), (1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) * t = 0) ∧ (Algebra.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.

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

Equations

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

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

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

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

theorem Algebra.FormallyUnramified.finite_of_free_aux {R : Type u_3} {S : Type u_3} [CommRing R] [CommRing S] [Algebra R S] (I : Type u_2) [DecidableEq I] (b : 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

theorem Algebra.FormallyUnramified.finite_of_free (R : Type u_2) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [Algebra.FormallyUnramified R S] [Algebra.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_2) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (M : Type u_1) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] [Algebra.FormallyUnramified R S] [Algebra.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_2) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (M : Type u_1) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] [Algebra.FormallyUnramified R S] [Algebra.EssFiniteType R S] : TensorProduct.AlgebraTensorModule.lift (↑R (Algebra.lsmul S S M).toLinearMap.flip).flip ∘ₗ Algebra.FormallyUnramified.sec R S M = LinearMap.id

theorem Algebra.FormallyUnramified.flat_of_restrictScalars (R : Type u_2) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (M : Type u_1) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] [Algebra.FormallyUnramified R S] [Algebra.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_2) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] (M : Type u_1) [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] [Algebra.FormallyUnramified R S] [Algebra.EssFiniteType R S] [Module.Projective R M] : Module.Projective S M

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