Scalar extension of isometry classes

Extension of scalars along a field extension K → L carries a diagonal presentation to the presentation of the same rank whose weights are the images of the original weights. That operation descends to isometry classes as TauCeti.RegularFormClass.baseChange, and the discriminant commutes with it: the discriminant of an extended class is the image of the original discriminant under the functorial map on square-class groups induced by the field homomorphism.

The diagonal descent principle is natural for this operation: an equality between invariants of a presentation and its scalar extension induces the same equality on their isometry classes.

Everything here is about field extensions in characteristic different from two. That restriction is not an artefact: QuadraticForm.baseChange is only defined when two is invertible in the base field, and TauCeti.RegularFormClass.discr is only defined over a field in which two is invertible, so both hypotheses are needed already to state the results.

These results let invariants computed over a global field be read after passing to any such field extension, in particular to the completions of a number field.

Main definitions

• TauCeti.RegularFormPresentation.baseChange: the presentation whose weights are the images of the original weights.
• TauCeti.RegularFormClass.baseChange: scalar extension of isometry classes.
• TauCeti.RegularFormClass.liftDiagonal_baseChange: compatible diagonal invariants remain compatible after descent and scalar extension.

Main results

• TauCeti.presentedFormBaseChange: extending a presented form presents the extended weights.
• TauCeti.RegularFormClass.rank_baseChange, TauCeti.RegularFormClass.baseChange_add and TauCeti.RegularFormClass.baseChange_mul: scalar extension preserves the rank and commutes with the orthogonal sum and the tensor product of classes.
• TauCeti.RegularFormClass.baseChange_self and TauCeti.RegularFormClass.baseChange_baseChange: scalar extension along the identity is the identity, and iterated scalar extension along a tower is scalar extension along the composite.
• TauCeti.RegularFormClass.baseChange_hyperbolicClass: scalar extension preserves the hyperbolic class.
• QuadraticForm.formClass_baseChange: the class of an extended form is the extension of its class.
• QuadraticForm.discr_formClass_baseChange_eq_zero: a form acquires square discriminant over a field containing a square root of its discriminant.
• TauCeti.RegularFormClass.discr_baseChange, TauCeti.RegularFormClass.signedDiscr_baseChange: the discriminant and the signed discriminant commute with scalar extension.

Scalar extension of presentations

def TauCeti.RegularFormPresentation.baseChange {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] (p : RegularFormPresentation K) : RegularFormPresentation L

The presentation obtained by mapping every weight into the extension field L. The rank is unchanged.

theorem TauCeti.RegularFormPresentation.baseChange_def {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] (p : RegularFormPresentation K) : baseChange L p = ⟨p.fst, fun (i : Fin p.fst) => (Units.map ↑(algebraMap K L)) (p.snd i)⟩

Scalar extension of a presentation keeps its rank and maps its weights into L.

@[simp]

theorem TauCeti.RegularFormPresentation.fst_baseChange {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] (p : RegularFormPresentation K) : (baseChange L p).fst = p.fst

Mapping the weights into L leaves the rank unchanged.

@[simp]

theorem TauCeti.RegularFormPresentation.baseChange_apply {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] (p : RegularFormPresentation K) (i : Fin (baseChange L p).fst) : (baseChange L p).snd i = (Units.map ↑(algebraMap K L)) (p.snd (Fin.cast ⋯ i))

Every weight of the mapped presentation is the image of the weight of p at the same index, read through TauCeti.RegularFormPresentation.fst_baseChange.

theorem TauCeti.RegularFormPresentation.prod_baseChange {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] (p : RegularFormPresentation K) : ∏ i : Fin (baseChange L p).fst, (baseChange L p).snd i = (Units.map ↑(algebraMap K L)) (∏ i : Fin p.fst, p.snd i)

The weight product of a mapped presentation is the image of the original weight product.

@[simp]

theorem TauCeti.RegularFormPresentation.baseChange_self {K : Type u} [Field K] (p : RegularFormPresentation K) : baseChange K p = p

Mapping the weights into the base field itself leaves a presentation unchanged.

@[simp]

theorem TauCeti.RegularFormPresentation.baseChange_baseChange {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] (M : Type u_1) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (p : RegularFormPresentation K) : baseChange M (baseChange L p) = baseChange M p

Mapping the weights into L and then into M is mapping them into M in one step.

@[simp]

theorem TauCeti.RegularFormPresentation.baseChange_one {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] : baseChange L one = one

Mapping the weights into L fixes the rank-one presentation with weight one.

@[simp]

theorem TauCeti.RegularFormPresentation.baseChange_append {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] (p q : RegularFormPresentation K) : baseChange L (p.append q) = (baseChange L p).append (baseChange L q)

Mapping the weights into L commutes with concatenation of presentations.

@[simp]

theorem TauCeti.RegularFormPresentation.baseChange_tmul {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] (p q : RegularFormPresentation K) : baseChange L (p.tmul q) = (baseChange L p).tmul (baseChange L q)

Mapping the weights into L commutes with the tensor product of presentations.

Scalar extension of presented forms

noncomputable def TauCeti.presentedFormBaseChange {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L] [Invertible 2] (p : RegularFormPresentation K) : QuadraticMap.IsometryEquiv (QuadraticForm.baseChange L (presentedForm p)) (presentedForm (RegularFormPresentation.baseChange L p))

The canonical coordinate equivalence identifies scalar extension of a presented form with the presentation obtained by mapping every weight into the larger field.

@[simp]

theorem TauCeti.presentedFormBaseChange_apply {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L] [Invertible 2] (p : RegularFormPresentation K) (x : TensorProduct K L (Fin p.fst → K)) (i : Fin (RegularFormPresentation.baseChange L p).fst) : (presentedFormBaseChange p) x i = (TensorProduct.piScalarRightHom K L L (Fin p.fst)) x (Fin.cast ⋯ i)

The presentation base-change isometry uses the canonical linear equivalence distributing the tensor product over the finite coordinate space.

Scalar extension of isometry classes

def TauCeti.RegularFormClass.baseChange {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] [Invertible 2] : RegularFormClass K → RegularFormClass L

Scalar extension of isometry classes: the class over L presented by the images of the weights of any presentation over K.

@[simp]

theorem TauCeti.RegularFormClass.baseChange_mk {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] [Invertible 2] (p : RegularFormPresentation K) : baseChange L ⟦p⟧ = ⟦RegularFormPresentation.baseChange L p⟧

Scalar extension of classes is computed on presentations by mapping the weights.

theorem TauCeti.RegularFormClass.liftDiagonal_baseChange {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L] [Invertible 2] [Invertible 2] {X : Type u_2} (f : RegularFormPresentation K → X) (g : RegularFormPresentation L → X) (hfperm : ∀ {n : ℕ} {w w' : Fin n → Kˣ}, PermutationStep w w' → f ⟨n, w⟩ = f ⟨n, w'⟩) (hfbin : ∀ {n : ℕ} {w w' : Fin n → Kˣ}, BinaryStep w w' → f ⟨n, w⟩ = f ⟨n, w'⟩) (hfone : ∀ (a b : Kˣ), IsSquare (a * b) → f ⟨1, fun (x : Fin 1) => a⟩ = f ⟨1, fun (x : Fin 1) => b⟩) (hgperm : ∀ {n : ℕ} {w w' : Fin n → Lˣ}, PermutationStep w w' → g ⟨n, w⟩ = g ⟨n, w'⟩) (hgbin : ∀ {n : ℕ} {w w' : Fin n → Lˣ}, BinaryStep w w' → g ⟨n, w⟩ = g ⟨n, w'⟩) (hgone : ∀ (a b : Lˣ), IsSquare (a * b) → g ⟨1, fun (x : Fin 1) => a⟩ = g ⟨1, fun (x : Fin 1) => b⟩) (hfg : ∀ (p : RegularFormPresentation K), g (RegularFormPresentation.baseChange L p) = f p) (x : RegularFormClass K) : liftDiagonal g ⋯ ⋯ hgone (baseChange L x) = liftDiagonal f ⋯ ⋯ hfone x

A diagonal invariant compatible with scalar extension before descent remains compatible after descending to isometry classes.

@[simp]

theorem TauCeti.RegularFormClass.baseChange_self {K : Type u} [Field K] [Invertible 2] (x : RegularFormClass K) : baseChange K x = x

Scalar extension along the identity extension is the identity.

@[simp]

theorem TauCeti.RegularFormClass.baseChange_baseChange {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] (M : Type u_1) [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [Invertible 2] [Invertible 2] (x : RegularFormClass K) : baseChange M (baseChange L x) = baseChange M x

Scalar extension along a tower K → L → M is scalar extension along the composite. Two is assumed invertible in L because extension of scalars out of L is only defined then.

@[simp]

theorem TauCeti.RegularFormClass.rank_baseChange {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] [Invertible 2] (x : RegularFormClass K) : (baseChange L x).rank = x.rank

Scalar extension preserves the rank of a class.

@[simp]

theorem TauCeti.RegularFormClass.baseChange_add {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] [Invertible 2] (x y : RegularFormClass K) : baseChange L (x + y) = baseChange L x + baseChange L y

Scalar extension commutes with the orthogonal sum of classes.

@[simp]

theorem TauCeti.RegularFormClass.baseChange_zero {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] [Invertible 2] : baseChange L 0 = 0

Scalar extension takes the rank-zero class to the rank-zero class.

theorem TauCeti.RegularFormClass.baseChange_nsmul {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L] [Invertible 2] (n : ℕ) (x : RegularFormClass K) : baseChange L (n • x) = n • baseChange L x

Scalar extension preserves finite orthogonal sums.

@[simp]

theorem TauCeti.RegularFormClass.baseChange_one {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] [Invertible 2] : baseChange L 1 = 1

Scalar extension takes the multiplicative unit to the multiplicative unit.

@[simp]

theorem TauCeti.RegularFormClass.baseChange_hyperbolicClass {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L] [Invertible 2] [Invertible 2] : baseChange L (hyperbolicClass K) = hyperbolicClass L

Base change preserves the hyperbolic class, for any choice of Invertible (2 : L).

@[simp]

theorem TauCeti.RegularFormClass.baseChange_mul {K : Type u} (L : Type v) [Field K] [Field L] [Algebra K L] [Invertible 2] [Invertible 2] (x y : RegularFormClass K) : baseChange L (x * y) = baseChange L x * baseChange L y

Scalar extension commutes with the tensor product of classes.

def TauCeti.RegularFormClass.baseChangeHom {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L] [Invertible 2] [Invertible 2] : RegularFormClass K →+* RegularFormClass L

Scalar extension of regular form classes as a ring homomorphism.

@[simp]

theorem TauCeti.RegularFormClass.baseChangeHom_apply {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L] [Invertible 2] [Invertible 2] (x : RegularFormClass K) : baseChangeHom x = baseChange L x

The ring homomorphism acts by the existing scalar extension of form classes.

@[simp]

theorem TauCeti.RegularFormClass.baseChangeHom_self {K : Type u} [Field K] [Invertible 2] : baseChangeHom = RingHom.id (RegularFormClass K)

Scalar extension to the same field is the identity ring homomorphism on form classes.

@[simp]

theorem TauCeti.RegularFormClass.baseChangeHom_comp {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L] {M : Type u_1} [Field M] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [Invertible 2] [Invertible 2] [Invertible 2] : baseChangeHom.comp baseChangeHom = baseChangeHom

Scalar extension through a tower composes as ring homomorphisms on form classes.

Scalar extension of the discriminants

@[simp]

theorem TauCeti.RegularFormClass.discr_baseChange {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L] [Invertible 2] [Invertible 2] (x : RegularFormClass K) : (baseChange L x).discr = (algebraMap K L).squareClassMap x.discr

The discriminant commutes with scalar extension of isometry classes: extending an isometry class to L pushes its discriminant forward along the induced map of square-class groups.

@[simp]

theorem TauCeti.RegularFormClass.signedDiscr_baseChange {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L] [Invertible 2] [Invertible 2] (x : RegularFormClass K) : (baseChange L x).signedDiscr = (algebraMap K L).squareClassMap x.signedDiscr

The signed discriminant commutes with scalar extension of isometry classes: extending an isometry class to L pushes its signed discriminant forward along the induced map of square-class groups.

@[simp]

theorem QuadraticForm.formClass_baseChange {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L] {V : Type w} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) : TauCeti.formClass (QuadraticForm.baseChange L Q) ⋯ = TauCeti.RegularFormClass.baseChange L (TauCeti.formClass Q hQ)

The class of a form extended to L is the scalar extension of its class.

theorem QuadraticForm.discr_formClass_baseChange_eq_zero {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L] {V : Type w} [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) {d : Kˣ} (hd : (TauCeti.formClass Q hQ).discr = TauCeti.squareClass d) {s : L} (hs : s * s = (algebraMap K L) ↑d) : (TauCeti.formClass (QuadraticForm.baseChange L Q) ⋯).discr = 0

If the discriminant of a regular form is the class of d, then the form has square discriminant after scalar extension to a field containing a square root of d.