Bilinear forms and base change

This file relates bilinear forms transported along an IsBaseChange equivalence to Mathlib's canonical base change of bilinear forms, and records how nondegeneracy behaves under that base change.

Nondegeneracy is not preserved by an arbitrary base change: a form can acquire a kernel when its discriminant becomes a zero divisor. On a finite free module it is exactly the nonvanishing of that discriminant, so any structure map between integral domains reflects it, and an injective one also preserves it. Those are Ado.nondegenerate_of_nondegenerate_baseChange and Ado.nondegenerate_baseChange_iff, and the computations behind them, Ado.bilinForm_toMatrix_baseChange and Ado.bilinForm_det_toMatrix_baseChange, say that base change acts entrywise on the Gram matrix of a basis and maps its determinant accordingly.

Main declarations

• IsBaseChange.bilinForm_baseChange: if a bilinear form restricts along a map to a second form, evaluating it through the associated base-change equivalence agrees with the canonical base change of the second form.
• Ado.bilinForm_toMatrix_baseChange: the Gram matrix of a base-changed form, in the base-changed basis, is the entrywise image of the original Gram matrix.
• Ado.bilinForm_det_toMatrix_baseChange: the determinant of that Gram matrix is the image of the original determinant.
• Ado.nondegenerate_of_nondegenerate_baseChange: a bilinear form on a finite free module over an integral domain is nondegenerate as soon as its base change into a second integral domain is, with no hypothesis on the structure map.
• Ado.nondegenerate_baseChange_iff: along an injective structure map between integral domains the implication is an equivalence.
• LinearMap.BilinForm.IsometryEquiv.baseChange: an isometric equivalence of bilinear forms base-changes to an isometric equivalence of their base changes.

theorem IsBaseChange.bilinForm_baseChange {R : Type u_1} {A : Type u_2} {M : Type u_3} {N : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module A N] [Module R N] [IsScalarTower R A N] {f : M →ₗ[R] N} (h : IsBaseChange A f) (B' : LinearMap.BilinForm R M) (B : LinearMap.BilinForm A N) (hB : ∀ (x y : M), (B (f x)) (f y) = (algebraMap R A) ((B' x) y)) (x y : TensorProduct R A M) : (B (h.equiv x)) (h.equiv y) = ((LinearMap.BilinForm.baseChange A B') x) y

If B restricts along f to B', evaluating B on base-changed vectors agrees with the canonical base change of B'.

@[simp]

theorem Ado.bilinForm_toMatrix_baseChange {R : Type u_1} {A : Type u_2} {M : Type u_3} {ι : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [Module R M] [Fintype ι] [DecidableEq ι] (B : LinearMap.BilinForm R M) (b : Module.Basis ι R M) : (LinearMap.BilinForm.toMatrix (Module.Basis.baseChange A b)) (LinearMap.BilinForm.baseChange A B) = ((LinearMap.BilinForm.toMatrix b) B).map ⇑(algebraMap R A)

Base change acts entrywise on the Gram matrix of a bilinear form: the matrix of B.baseChange A in the base-changed basis is the image of the matrix of B under the structure map.

theorem Ado.bilinForm_det_toMatrix_baseChange {R : Type u_1} {A : Type u_2} {M : Type u_3} {ι : Type u_4} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Fintype ι] [DecidableEq ι] (B : LinearMap.BilinForm R M) (b : Module.Basis ι R M) : ((LinearMap.BilinForm.toMatrix (Module.Basis.baseChange A b)) (LinearMap.BilinForm.baseChange A B)).det = (algebraMap R A) ((LinearMap.BilinForm.toMatrix b) B).det

The Gram determinant of a base-changed bilinear form is the image of the original Gram determinant under the structure map.

theorem Ado.nondegenerate_of_nondegenerate_baseChange {R : Type u_1} (A : Type u_2) {M : Type u_3} {ι : Type u_4} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Finite ι] [IsDomain R] [IsDomain A] (B : LinearMap.BilinForm R M) (b : Module.Basis ι R M) (h : (LinearMap.BilinForm.baseChange A B).Nondegenerate) : B.Nondegenerate

Nondegeneracy descends along any base change of integral domains. On a finite free module, nondegeneracy of a bilinear form is nonvanishing of the determinant of its Gram matrix, and the structure map sends that determinant to the determinant of the base-changed Gram matrix, so a nondegenerate base change forces a nondegenerate form. No hypothesis on the structure map is needed.

theorem Ado.nondegenerate_baseChange_iff {R : Type u_1} {A : Type u_2} {M : Type u_3} {ι : Type u_4} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M] [Module R M] [Finite ι] [IsDomain A] [FaithfulSMul R A] (B : LinearMap.BilinForm R M) (b : Module.Basis ι R M) : (LinearMap.BilinForm.baseChange A B).Nondegenerate ↔ B.Nondegenerate

Nondegeneracy is preserved and reflected by an injective base change of integral domains. On a finite free module, nondegeneracy of a bilinear form is nonvanishing of the determinant of its Gram matrix, and an injective structure map neither creates nor destroys that.

def LinearMap.BilinForm.IsometryEquiv.baseChange {R : Type u_1} (A : Type u_2) {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] {B₁ : LinearMap.BilinForm R M₁} {B₂ : LinearMap.BilinForm R M₂} (f : B₁.IsometryEquiv B₂) : (BilinForm.baseChange A B₁).IsometryEquiv (BilinForm.baseChange A B₂)

Base change of an isometric equivalence of bilinear forms: the base change of the underlying linear equivalence is an isometric equivalence of the base-changed forms.

Equations

• LinearMap.BilinForm.IsometryEquiv.baseChange A f = { toLinearEquiv := LinearEquiv.baseChange R A M₁ M₂ f.toLinearEquiv, map_app' := ⋯ }

@[simp]

theorem LinearMap.BilinForm.IsometryEquiv.baseChange_tmul {R : Type u_1} {A : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] {B₁ : LinearMap.BilinForm R M₁} {B₂ : LinearMap.BilinForm R M₂} (f : B₁.IsometryEquiv B₂) (a : A) (m : M₁) : (baseChange A f) (a ⊗ₜ[R] m) = a ⊗ₜ[R] f m

On pure tensors, a base-changed isometric equivalence applies the original equivalence to the vector.