Orders in finite-dimensional algebras

Let R be a domain with fraction field F and E a finite-dimensional F-algebra, not necessarily commutative. An R-order in E is an R-subalgebra Λ of E which is an R-lattice in E in the sense of Submodule.IsLattice: it is finitely generated as an R-module and spans E over F. Orders are the integral structures on which arithmetic of E is done: the ring of integers of a number field, group rings R[G] ⊆ F[G], and M_n(R) ⊆ M_n(F) are orders.

Every element of an order is integral over R. Conversely, over an integrally closed noetherian R, a spanning subalgebra all of whose elements are integral is an order provided the regular trace form of E is nondegenerate: the regular traces of products of its elements lie in R, so the subalgebra lies in the R-span of the dual basis of an F-basis chosen inside it. Some hypothesis of this kind is needed: if R is not a field, then in E = F[ε]/(ε²) the subalgebra R + F ε spans E and consists of integral elements, but is not finitely generated over R. The regular-trace hypothesis is stronger than necessary: it excludes M_p(F) in characteristic p, whose regular trace form vanishes, although the conclusion holds there via the reduced trace.

Main definitions

• TauCeti.IntegralOrder.IsOrder F Λ: the R-subalgebra Λ of E is an R-order in E.
• TauCeti.IntegralOrder.groupRingSubalgebra R F G: the group ring R[G] as an R-subalgebra of F[G].

Main results

• TauCeti.IntegralOrder.isOrder_iff: Λ is an order iff it is finite over R and spans E.
• TauCeti.IntegralOrder.isOrder_op_iff: Λᵒᵖ is an order in Eᵐᵒᵖ iff Λ is an order in E.
• TauCeti.IntegralOrder.IsOrder.isIntegral: every element of an order is integral over R.
• TauCeti.IntegralOrder.IsOrder.le_integralClosure: in a commutative algebra, every order lies in the integral closure of R.
• TauCeti.IntegralOrder.toSubmodule_le_dualSubmodule_regularTraceForm: over an integrally closed R, a subalgebra of integral elements lies in its own dual for the regular trace form.
• TauCeti.IntegralOrder.toSubmodule_le_span_dualBasis: such a subalgebra containing an F-basis b of E lies in the R-span of the regular-trace dual basis of b.
• TauCeti.IntegralOrder.isOrder_of_isIntegral: a spanning subalgebra of integral elements is an order when R is integrally closed and noetherian and the regular trace form is nondegenerate.
• TauCeti.IntegralOrder.mem_groupRingSubalgebra: x ∈ F[G] lies in R[G] iff all its coefficients come from R.
• TauCeti.IntegralOrder.groupRing_isOrder: R[G] is an order in F[G] for a finite monoid G.
• TauCeti.IntegralOrder.integralClosure_isOrder: the integral closure of an integrally closed noetherian R in a finite separable extension of F is an order.

References

• H. Johnston, Notes on Galois modules, Definition 3.8 and Examples 3.10.
• J. Voight, Quaternion algebras, Definition 10.2.1 and Lemma 10.3.7; the integrality criterion is proved there for separable algebras with the reduced trace, and here with the regular trace.

TauCeti.IntegralOrder.toSubmodule_le_span_dualBasis and the proof of TauCeti.IntegralOrder.isOrder_of_isIntegral follow Mathlib's IsIntegralClosure.range_le_span_dualBasis and IsIntegralClosure.isNoetherian, which carry out the dual-basis bound for the integral closure in a finite separable field extension.

def TauCeti.IntegralOrder.IsOrder {R : Type u_1} (F : Type u_2) {E : Type u_3} [CommRing R] [CommRing F] [Ring E] [Algebra R F] [Algebra F E] [Algebra R E] [IsScalarTower R F E] (Λ : Subalgebra R E) : Prop

An R-subalgebra Λ of an F-algebra E is an R-order in E if it is an R-lattice in E: finitely generated as an R-module, with F-span all of E.

theorem TauCeti.IntegralOrder.isOrder_iff_isLattice {R : Type u_1} {F : Type u_2} {E : Type u_3} [CommRing R] [CommRing F] [Ring E] [Algebra R F] [Algebra F E] [Algebra R E] [IsScalarTower R F E] {Λ : Subalgebra R E} : IsOrder F Λ ↔ Submodule.IsLattice F (Subalgebra.toSubmodule Λ)

Being an order is being an R-lattice in E (this is the definition of IsOrder).

theorem TauCeti.IntegralOrder.isOrder_iff {R : Type u_1} {F : Type u_2} {E : Type u_3} [CommRing R] [CommRing F] [Ring E] [Algebra R F] [Algebra F E] [Algebra R E] [IsScalarTower R F E] {Λ : Subalgebra R E} : IsOrder F Λ ↔ Module.Finite R ↥Λ ∧ Submodule.span F ↑Λ = ⊤

An R-subalgebra is an order exactly when it is finite over R and spans E over F.

theorem TauCeti.IntegralOrder.IsOrder.finite {R : Type u_1} {F : Type u_2} {E : Type u_3} [CommRing R] [CommRing F] [Ring E] [Algebra R F] [Algebra F E] [Algebra R E] [IsScalarTower R F E] {Λ : Subalgebra R E} (h : IsOrder F Λ) : Module.Finite R ↥Λ

An order is finite as an R-module.

theorem TauCeti.IntegralOrder.IsOrder.span_eq_top {R : Type u_1} {F : Type u_2} {E : Type u_3} [CommRing R] [CommRing F] [Ring E] [Algebra R F] [Algebra F E] [Algebra R E] [IsScalarTower R F E] {Λ : Subalgebra R E} (h : IsOrder F Λ) : Submodule.span F ↑Λ = ⊤

An order spans its ambient algebra over F.

theorem TauCeti.IntegralOrder.IsOrder.isIntegral {R : Type u_1} {F : Type u_2} {E : Type u_3} [CommRing R] [CommRing F] [Ring E] [Algebra R F] [Algebra F E] [Algebra R E] [IsScalarTower R F E] {Λ : Subalgebra R E} (h : IsOrder F Λ) {x : E} (hx : x ∈ Λ) : IsIntegral R x

Elements of orders are integral. Every element of an R-order is integral over R, since the order is a finitely generated R-module.

theorem TauCeti.IntegralOrder.IsOrder.of_le {R : Type u_1} {F : Type u_2} {E : Type u_3} [CommRing R] [CommRing F] [Ring E] [Algebra R F] [Algebra F E] [Algebra R E] [IsScalarTower R F E] {Λ Γ : Subalgebra R E} (h : IsOrder F Λ) (hle : Λ ≤ Γ) [Module.Finite R ↥Γ] : IsOrder F Γ

A finitely generated subalgebra containing an order is an order.

theorem TauCeti.IntegralOrder.isOrder_op_iff {R : Type u_1} {F : Type u_2} {E : Type u_3} [CommRing R] [CommRing F] [Ring E] [Algebra R F] [Algebra F E] [Algebra R E] [IsScalarTower R F E] {Λ : Subalgebra R E} : IsOrder F Λ.op ↔ IsOrder F Λ

Opposite orders. Λᵒᵖ is an R-order in Eᵐᵒᵖ exactly when Λ is an R-order in E.

theorem TauCeti.IntegralOrder.isOrder_bot {R : Type u_1} {F : Type u_2} [CommRing R] [CommRing F] [Algebra R F] : IsOrder F ⊥

The image of R is an R-order in F.

theorem TauCeti.IntegralOrder.IsOrder.le_integralClosure {R : Type u_1} {F : Type u_2} {E : Type u_3} [CommRing R] [CommRing F] [CommRing E] [Algebra R F] [Algebra F E] [Algebra R E] [IsScalarTower R F E] {Λ : Subalgebra R E} (h : IsOrder F Λ) : Λ ≤ integralClosure R E

In a commutative algebra, every R-order lies in the integral closure of R.

theorem TauCeti.IntegralOrder.toSubmodule_le_dualSubmodule_regularTraceForm {R : Type u_1} {F : Type u_2} {E : Type u_3} [CommRing R] [Field F] [Ring E] [Algebra R F] [IsFractionRing R F] [Algebra F E] [Algebra R E] [IsScalarTower R F E] [FiniteDimensional F E] [IsIntegrallyClosed R] {Γ : Subalgebra R E} (hint : ∀ x ∈ Γ, IsIntegral R x) : Subalgebra.toSubmodule Γ ≤ (Algebra.regularTraceForm F E).dualSubmodule (Subalgebra.toSubmodule Γ)

Integral subalgebras lie in their own trace dual. If every element of the R-subalgebra Γ is integral over the integrally closed domain R, then the regular trace Tr_F (x * y) of a product of two elements of Γ lies in R: Γ lies in its dual for the regular trace form.

theorem TauCeti.IntegralOrder.toSubmodule_le_span_dualBasis {R : Type u_1} {F : Type u_2} {E : Type u_3} [CommRing R] [Field F] [Ring E] [Algebra R F] [IsFractionRing R F] [Algebra F E] [Algebra R E] [IsScalarTower R F E] [FiniteDimensional F E] [IsIntegrallyClosed R] (hB : (Algebra.regularTraceForm F E).Nondegenerate) {ι : Type u_4} [Finite ι] [DecidableEq ι] (b : Module.Basis ι F E) {Γ : Subalgebra R E} (hb : ∀ (i : ι), b i ∈ Γ) (hint : ∀ x ∈ Γ, IsIntegral R x) : Subalgebra.toSubmodule Γ ≤ Submodule.span R (Set.range ⇑((Algebra.regularTraceForm F E).dualBasis hB b))

The trace-dual bound. Let R be integrally closed and let b be an F-basis of E lying in an R-subalgebra Γ of integral elements. Then Γ lies in the R-span of the basis dual to b for the (nondegenerate) regular trace form. The bound depends only on b, so it holds simultaneously for every such Γ containing b.

theorem TauCeti.IntegralOrder.isOrder_of_isIntegral {R : Type u_1} {F : Type u_2} {E : Type u_3} [CommRing R] [Field F] [Ring E] [Algebra R F] [IsFractionRing R F] [Algebra F E] [Algebra R E] [IsScalarTower R F E] [FiniteDimensional F E] [IsIntegrallyClosed R] [IsNoetherianRing R] (hB : (Algebra.regularTraceForm F E).Nondegenerate) {Λ : Subalgebra R E} (hint : ∀ x ∈ Λ, IsIntegral R x) (hspan : Submodule.span F ↑Λ = ⊤) : IsOrder F Λ

Integral spanning subalgebras are orders. Let R be an integrally closed noetherian domain with fraction field F, and E a finite-dimensional F-algebra whose regular trace form (x, y) ↦ Tr_F (x * y) is nondegenerate. An R-subalgebra of E spanning E over F and consisting of elements integral over R is an R-order in E.

theorem TauCeti.IntegralOrder.integralClosure_isOrder {R : Type u_1} {F : Type u_2} [CommRing R] [Field F] [Algebra R F] [IsFractionRing R F] [IsDomain R] [IsIntegrallyClosed R] [IsNoetherianRing R] (L : Type u_4) [Field L] [Algebra F L] [Algebra R L] [IsScalarTower R F L] [FiniteDimensional F L] [Algebra.IsSeparable F L] : IsOrder F (integralClosure R L)

Integral closures are orders. The integral closure of an integrally closed noetherian domain R in a finite separable extension L of its fraction field F is an R-order in L.

noncomputable def TauCeti.IntegralOrder.groupRingSubalgebra (R : Type u_1) (F : Type u_2) (G : Type u_3) [CommRing R] [CommRing F] [Algebra R F] [Monoid G] : Subalgebra R (MonoidAlgebra F G)

The group ring R[G] as an R-subalgebra of F[G]: the image of the map R[G] → F[G] applying algebraMap R F to every coefficient.

@[simp]

theorem TauCeti.IntegralOrder.mem_groupRingSubalgebra {R : Type u_1} {F : Type u_2} {G : Type u_3} [CommRing R] [CommRing F] [Algebra R F] [Monoid G] {x : MonoidAlgebra F G} : x ∈ groupRingSubalgebra R F G ↔ ∀ (g : G), x.coeff g ∈ (algebraMap R F).range

An element of F[G] lies in R[G] exactly when all its coefficients come from R.

theorem TauCeti.IntegralOrder.single_one_mem_groupRingSubalgebra {R : Type u_1} {F : Type u_2} {G : Type u_3} [CommRing R] [CommRing F] [Algebra R F] [Monoid G] (g : G) : MonoidAlgebra.single g 1 ∈ groupRingSubalgebra R F G

The basis element g of F[G] lies in R[G].

theorem TauCeti.IntegralOrder.toSubmodule_groupRingSubalgebra (R : Type u_1) (F : Type u_2) (G : Type u_3) [CommRing R] [CommRing F] [Algebra R F] [Monoid G] : Subalgebra.toSubmodule (groupRingSubalgebra R F G) = Submodule.span R (Set.range fun (g : G) => MonoidAlgebra.single g 1)

As an R-module, R[G] is spanned by the basis elements g of F[G].

theorem TauCeti.IntegralOrder.groupRing_isOrder (R : Type u_1) (F : Type u_2) (G : Type u_3) [CommRing R] [CommRing F] [Algebra R F] [Monoid G] [Finite G] : IsOrder F (groupRingSubalgebra R F G)

Group rings are orders. For a finite monoid G, the group ring R[G] is an R-order in F[G].