One trace-dual lattice bounds every overorder

Let R be an integrally closed domain with fraction field F and E a finite-dimensional F-algebra whose regular trace form (x, y) ↦ Tr_F (x * y) is nondegenerate. Fix an R-order Λ in E and an F-basis e of E inside Λ, and let r = det (Tr_F (e i * e j)) be its Gram determinant, which is nonzero. Every element of an overorder Γ ⊇ Λ is integral over R, so the regular traces Tr_F (x * e j) for x ∈ Γ lie in R; Cramer's rule in the fixed Gram matrix then puts r • x in the R-span of e. Hence every overorder of Λ lies in the single module r⁻¹ • span R e, which depends on Λ and e but not on Γ.

Over a noetherian R this module is noetherian, so the overorders of Λ satisfy the ascending chain condition. This is the finiteness input for the existence of maximal orders containing a given order.

Main results

• TauCeti.IntegralOrder.det_smul_mem_span: if Γ is an R-subalgebra of integral elements containing the F-basis e, then r • x ∈ span R e for every x ∈ Γ.
• TauCeti.IntegralOrder.toSubmodule_le_inv_det_smul_span: for a nondegenerate regular trace form, every such Γ lies in r⁻¹ • span R e.
• TauCeti.IntegralOrder.IsOrder.wellFoundedGT_overorder: over a noetherian integrally closed R, the orders containing a given order satisfy the ascending chain condition.

References

• J. Voight, Quaternion algebras, proof of Lemma 10.3.7 and paragraph 10.4.2; Voight uses the reduced trace of a separable algebra, and here the regular trace is used instead.

theorem TauCeti.IntegralOrder.det_smul_mem_span {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] {ι : Type u_4} [Fintype ι] [DecidableEq ι] (e : Module.Basis ι F E) {Γ : Subalgebra R E} (he : ∀ (i : ι), e i ∈ Γ) (hint : ∀ x ∈ Γ, IsIntegral R x) {x : E} (hx : x ∈ Γ) : ((LinearMap.BilinForm.toMatrix e) (Algebra.regularTraceForm F E)).det • x ∈ Submodule.span R (Set.range ⇑e)

Cramer's bound for subalgebras of integral elements. Let e be an F-basis of E lying in an R-subalgebra Γ all of whose elements are integral over the integrally closed domain R, and let r = det (Tr_F (e i * e j)) be the Gram determinant of the regular trace form. Then r • x lies in the R-span of e for every x ∈ Γ.

theorem TauCeti.IntegralOrder.toSubmodule_le_inv_det_smul_span {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} [Fintype ι] [DecidableEq ι] (e : Module.Basis ι F E) {Γ : Subalgebra R E} (he : ∀ (i : ι), e i ∈ Γ) (hint : ∀ x ∈ Γ, IsIntegral R x) : Subalgebra.toSubmodule Γ ≤ ((LinearMap.BilinForm.toMatrix e) (Algebra.regularTraceForm F E)).det⁻¹ • Submodule.span R (Set.range ⇑e)

One trace-dual lattice bounds every overorder. Let R be integrally closed, let the regular trace form of E be nondegenerate, and let e be an F-basis of E with Gram determinant r = det (Tr_F (e i * e j)). Every R-subalgebra Γ of integral elements containing e lies in r⁻¹ • span R e. Taking e inside an order Λ, this applies to every overorder Γ ⊇ Λ, and the bound does not depend on Γ.

theorem TauCeti.IntegralOrder.IsOrder.wellFoundedGT_overorder {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} (hΛ : IsOrder F Λ) : WellFoundedGT { Γ : Subalgebra R E // Λ ≤ Γ ∧ IsOrder F Γ }

Ascending chain condition for overorders. Let R be an integrally closed noetherian domain and let the regular trace form of E be nondegenerate. For an R-order Λ in E, the R-orders in E containing Λ satisfy the ascending chain condition: they all lie in one finitely generated R-module, the trace-dual lattice of an F-basis of E inside Λ.