Base change of an unramified algebra to a field

If S is a formally unramified R-algebra of essentially finite type and K is a field with an R-algebra structure, then K ⊗[R] S is a finite reduced K-algebra, in particular an Artinian reduced ring, and so is S ⊗[R] K via the commutativity isomorphism. For K the fraction field of a domain R this is the generic fibre of S.

Main results

• TauCeti.Algebra.FormallyUnramified.finite_field_tensorProduct, isArtinianRing_field_tensorProduct and isReduced_field_tensorProduct: K ⊗[R] S is finite over K, Artinian and reduced.
• TauCeti.Algebra.FormallyUnramified.isSemisimpleRing_field_tensorProduct: K ⊗[R] S is a semisimple ring, so each of its ideals is generated by an idempotent.
• TauCeti.Algebra.FormallyUnramified.isArtinianRing_tensorProduct_field and isReduced_tensorProduct_field: S ⊗[R] K is Artinian and reduced.

All are instances.

References

• Ported from T. Dupuy, T. Tucker and Z. Wang, pcfawd-formalization at commit 9a20b3f351446d64e6015d704198bc71c7002008 (Apache-2.0), lean/Pcf/Stacks/Common/EtaleNormal.lean: the instances for S ⊗[R] K generalize its Pcf.Stacks.isArtinianRing_isReduced_tensor_fractionRing_of_etale from étale algebras and the fraction field of a domain to unramified algebras and any field.

instance TauCeti.Algebra.FormallyUnramified.finite_field_tensorProduct {R : Type u_1} {S : Type u_2} {K : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [Algebra.FormallyUnramified R S] [Algebra.EssFiniteType R S] [Field K] [Algebra R K] : Module.Finite K (TensorProduct R K S)

The base change K ⊗[R] S of an unramified algebra to a field is a finite K-algebra.

instance TauCeti.Algebra.FormallyUnramified.isArtinianRing_field_tensorProduct {R : Type u_1} {S : Type u_2} {K : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [Algebra.FormallyUnramified R S] [Algebra.EssFiniteType R S] [Field K] [Algebra R K] : IsArtinianRing (TensorProduct R K S)

The base change K ⊗[R] S of an unramified algebra to a field is an Artinian ring.

instance TauCeti.Algebra.FormallyUnramified.isReduced_field_tensorProduct {R : Type u_1} {S : Type u_2} {K : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [Algebra.FormallyUnramified R S] [Algebra.EssFiniteType R S] [Field K] [Algebra R K] : IsReduced (TensorProduct R K S)

The base change K ⊗[R] S of an unramified algebra to a field is a reduced ring.

instance TauCeti.Algebra.FormallyUnramified.isSemisimpleRing_field_tensorProduct {R : Type u_1} {S : Type u_2} {K : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [Algebra.FormallyUnramified R S] [Algebra.EssFiniteType R S] [Field K] [Algebra R K] : IsSemisimpleRing (TensorProduct R K S)

The base change K ⊗[R] S of an unramified algebra to a field is a semisimple ring, being Artinian and reduced.

instance TauCeti.Algebra.FormallyUnramified.isArtinianRing_tensorProduct_field {R : Type u_1} {S : Type u_2} {K : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [Algebra.FormallyUnramified R S] [Algebra.EssFiniteType R S] [Field K] [Algebra R K] : IsArtinianRing (TensorProduct R S K)

The base change S ⊗[R] K of an unramified algebra to a field is an Artinian ring.

instance TauCeti.Algebra.FormallyUnramified.isReduced_tensorProduct_field {R : Type u_1} {S : Type u_2} {K : Type u_3} [CommRing R] [CommRing S] [Algebra R S] [Algebra.FormallyUnramified R S] [Algebra.EssFiniteType R S] [Field K] [Algebra R K] : IsReduced (TensorProduct R S K)

The base change S ⊗[R] K of an unramified algebra to a field is a reduced ring.