Nondegeneracy of trace forms

Nondegeneracy of the trace form Algebra.traceForm K B is invariant under algebra isomorphisms, holds on a finite product exactly when it holds on every factor, and forces B to be reduced when the base ring is reduced. These are the inputs that reduce the trace-form criterion for étaleness over a field to finite separable field extensions.

Main results

• TauCeti.Algebra.traceForm_nondegenerate_congr: nondegeneracy of the trace form is invariant under algebra isomorphisms.
• TauCeti.Algebra.traceForm_pi_nondegenerate_iff: the trace form of a finite product is nondegenerate iff the trace form of every factor is.
• TauCeti.Algebra.discr_ne_zero_iff_traceForm_nondegenerate: over a domain, the discriminant of a basis is nonzero iff the trace form is nondegenerate.
• TauCeti.Algebra.isReduced_of_traceForm_nondegenerate: an algebra over a reduced ring with nondegenerate trace form is reduced.
• TauCeti.Algebra.finite_of_traceForm_nondegenerate: an algebra over a commutative ring with nondegenerate trace form is a finite module.

References

• Ported from T. Dupuy, T. Tucker and Z. Wang, pcfawd-formalization at commit 9a20b3f351446d64e6015d704198bc71c7002008 (Apache-2.0), lean/Pcf/Stacks/Purity/DiscriminantFiber.lean and lean/Pcf/Stacks/Purity/DiscriminantGlobal.lean, namespace Pcf.Stacks: traceForm_nondegenerate_congr is its Algebra.traceForm_nondegenerate_of_algEquiv; traceForm_pi_nondegenerate_iff combines its Algebra.traceForm_pi_nondegenerate and Algebra.traceForm_pi_nondegenerate_factors; isReduced_of_traceForm_nondegenerate is the trace-pairing step of its Algebra.isReduced_of_discr_ne_zero_of_basis; and the source proves discr_ne_zero_iff_traceForm_nondegenerate inline (in its Algebra.discr_ne_zero_of_formallyEtale_of_basis).

theorem TauCeti.Algebra.traceForm_nondegenerate_congr {K : Type u_1} [CommRing K] {S : Type u_2} {T : Type u_3} [CommRing S] [CommRing T] [Algebra K S] [Algebra K T] (e : S ≃ₐ[K] T) : (Algebra.traceForm K S).Nondegenerate ↔ (Algebra.traceForm K T).Nondegenerate

Nondegeneracy of the trace form is invariant under algebra isomorphisms.

@[simp]

theorem TauCeti.Algebra.traceForm_pi_nondegenerate_iff {K : Type u_1} [CommRing K] {ι : Type u_2} [Finite ι] (L : ι → Type u_3) [(i : ι) → CommRing (L i)] [(i : ι) → Algebra K (L i)] [∀ (i : ι), Module.Free K (L i)] [∀ (i : ι), Module.Finite K (L i)] : (Algebra.traceForm K ((i : ι) → L i)).Nondegenerate ↔ ∀ (i : ι), (Algebra.traceForm K (L i)).Nondegenerate

The trace form of a finite product of finite free algebras is nondegenerate iff the trace form of every factor is.

theorem TauCeti.Algebra.isReduced_of_traceForm_nondegenerate {K : Type u_1} [CommRing K] {B : Type u_2} [IsReduced K] [CommRing B] [Algebra K B] (h : (Algebra.traceForm K B).Nondegenerate) : IsReduced B

An algebra over a reduced ring with nondegenerate trace form is reduced.

theorem TauCeti.Algebra.finite_of_traceForm_nondegenerate {F : Type u_2} {B : Type u_3} [CommRing F] [CommRing B] [Algebra F B] (h : (Algebra.traceForm F B).Nondegenerate) : Module.Finite F B

An algebra over a commutative ring with nondegenerate trace form is a finite module: otherwise the trace vanishes, so nondegeneracy forces the algebra to be trivial, hence finite.

theorem TauCeti.Algebra.discr_ne_zero_iff_traceForm_nondegenerate {F : Type u_2} {B : Type u_3} {ι : Type u_4} [CommRing F] [IsDomain F] [CommRing B] [Algebra F B] [Fintype ι] [DecidableEq ι] (b : Module.Basis ι F B) : Algebra.discr F ⇑b ≠ 0 ↔ (Algebra.traceForm F B).Nondegenerate

The discriminant of a basis of a finite free algebra over a domain is nonzero iff the trace form is nondegenerate.