Scalar extension of an integral bilinear form

This file specializes IsBaseChange.bilinForm to integral lattices and their rational and complex scalar extensions. The two extensions agree on purely rational vectors of the complexification.

Two properties make the complex extension usable in Hodge theory. It is real: conjugating both arguments conjugates the value, because lattice-induced conjugation fixes the integral vectors. And it is nondegenerate as soon as the integral form is: nondegeneracy is preserved first by localization from ℤ to ℚ and then by scalar extension from ℚ to ℂ.

Main declarations

• TauCeti.Hodge.bilinForm_latticeConj: the complex extension commutes with lattice-induced conjugation.
• TauCeti.Hodge.nondegenerate_bilinForm_complex: the complex extension inherits nondegeneracy from the integral form.
• TauCeti.Hodge.bilinForm_rationalToComplexLinearEquiv_one_tmul: the complexified form computes the rationalified one on purely rational vectors.

theorem TauCeti.Hodge.integralMapToComplex_bilinForm {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (hℂ : IsBaseChange ℂ ιℂ) (Q : LinearMap.BilinForm ℤ V) : integralMapToComplex hℂ (dualLatticeMap hℂ) Q = hℂ.bilinForm Q

Complexifying the linear map from a bilinear form to the dual gives the linear map of the complexified form.

theorem TauCeti.Hodge.bilinForm_apply_latticeConj {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (hℂ : IsBaseChange ℂ ιℂ) (Q : LinearMap.BilinForm ℤ V) (x : V) (y : Vℂ) : ((hℂ.bilinForm Q) (ιℂ x)) ((latticeConj hℂ) y) = (starRingEnd ℂ) (((hℂ.bilinForm Q) (ιℂ x)) y)

Conjugating the second argument of a complexified integral form against an integral first argument conjugates its value.

@[simp]

theorem TauCeti.Hodge.bilinForm_latticeConj {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (hℂ : IsBaseChange ℂ ιℂ) (Q : LinearMap.BilinForm ℤ V) (x y : Vℂ) : ((hℂ.bilinForm Q) ((latticeConj hℂ) x)) ((latticeConj hℂ) y) = (starRingEnd ℂ) (((hℂ.bilinForm Q) x) y)

Conjugating both arguments of a complexified integral form conjugates its value: the form takes real values on the lattice.

theorem TauCeti.Hodge.nondegenerate_bilinForm_complex {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} (hℂ : IsBaseChange ℂ ιℂ) {Q : LinearMap.BilinForm ℤ V} (hQ : Q.Nondegenerate) : (hℂ.bilinForm Q).Nondegenerate

Complexification preserves nondegeneracy of an integral bilinear form.

Comparing the rational and the complex extension

theorem TauCeti.Hodge.bilinForm_rationalToComplexLinearEquiv_one_tmul {V : Type u} {Vℂ : Type v} [AddCommGroup V] [AddCommGroup Vℂ] [Module ℂ Vℂ] {ιℂ : V →ₗ[ℤ] Vℂ} {Vℚ : Type u_1} [AddCommGroup Vℚ] [Module ℚ Vℚ] {ιℚ : V →ₗ[ℤ] Vℚ} (hℚ : IsBaseChange ℚ ιℚ) (hℂ : IsBaseChange ℂ ιℂ) (Q : LinearMap.BilinForm ℤ V) (x y : Vℚ) : ((hℂ.bilinForm Q) ((rationalToComplexLinearEquiv hℚ hℂ) (1 ⊗ₜ[ℚ] x))) ((rationalToComplexLinearEquiv hℚ hℂ) (1 ⊗ₜ[ℚ] y)) = ↑(((hℚ.bilinForm Q) x) y)

The two scalar extensions of an integral form agree: on purely rational vectors of the complexification, the complexified form takes the values of the rationalified form.