Documentation

TauCeti.RingTheory.Discriminant.BaseChange

Discriminants under base change #

The trace matrix of an arbitrary family, and the discriminant of a finite family, in a finite free algebra commute with scalar extension. In particular, for a basis b of S over R and an R-algebra A, the discriminant of the base-changed basis of A ⊗[R] S over A is the image of the discriminant of b. This lets statements about discriminants pass to residue fields and localizations.

Main results #

References #

source
@[simp]
theorem TauCeti.Algebra.traceMatrix_baseChange {R : Type u_1} {S : Type u_2} {A : Type u_3} {ι : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [Algebra R A] [Module.Free R S] [Module.Finite R S] (b : ι → S) :
(Algebra.traceMatrix A fun (i : ι) => 1 ⊗ₜ[R] b i) = (Algebra.traceMatrix R b).map ⇑(algebraMap R A)

The trace matrix of a base-changed family is the image of its original trace matrix.

source
@[simp]
theorem TauCeti.Algebra.discr_baseChange {R : Type u_1} {S : Type u_2} {A : Type u_3} {ι : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [Algebra R A] [Module.Free R S] [Module.Finite R S] [Fintype ι] [DecidableEq ι] (b : ι → S) :
(Algebra.discr A fun (i : ι) => 1 ⊗ₜ[R] b i) = (algebraMap R A) (Algebra.discr R b)

The discriminant of a base-changed finite family is the image of its original discriminant.

source
@[simp]
theorem TauCeti.Algebra.discr_basis_baseChange {R : Type u_1} {S : Type u_2} {A : Type u_3} {ι : Type u_4} [CommRing R] [CommRing S] [Algebra R S] [CommRing A] [Algebra R A] [Fintype ι] [DecidableEq ι] (b : Module.Basis ι R S) :
Algebra.discr A ⇑(Algebra.TensorProduct.basis A b) = (algebraMap R A) (Algebra.discr R ⇑b)

The discriminant of a base-changed basis is the image of its original discriminant.