Documentation

TauCeti.LinearAlgebra.BilinearForm.Dual.Lattice

Dual submodules of lattices #

This file develops the duality theory for full lattices in vector spaces equipped with a nondegenerate bilinear form over a fraction field.

Main declarations #

source
theorem LinearMap.BilinForm.dualSubmodule_anti {R : Type u_1} {K : Type u_2} {V : Type u_3} [CommRing R] [Field K] [Algebra R K] [AddCommGroup V] [Module R V] [Module K V] [IsScalarTower R K V] (B : LinearMap.BilinForm K V) :
Antitone B.dualSubmodule

Taking dual submodules with respect to a bilinear form reverses inclusions.

source
theorem LinearMap.BilinForm.det_toMatrix_smul_mem_span {R : Type u_1} {K : Type u_2} {V : Type u_3} [CommRing R] [Field K] [Algebra R K] [AddCommGroup V] [Module R V] [Module K V] [IsScalarTower R K V] (B : LinearMap.BilinForm K V) {ι : Type u_4} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K V) (hb : ∀ (i j : ι), (B (b i)) (b j) ∈ 1) {x : V} (hx : x ∈ B.dualSubmodule (Submodule.span R (Set.range ⇑b))) :
((toMatrix b) B).det • x ∈ Submodule.span R (Set.range ⇑b)

Cramer's rule for dual lattices. Let b be a basis of V over the field K such that every Gram matrix entry B (b i) (b j) lies in R. Then the Gram determinant r = det (B (b i) (b j)) multiplies the dual of the R-span of b into that span: r • x lies in the R-span of b whenever every B x (b j) lies in R. When B is nondegenerate, r ≠ 0 (LinearMap.BilinForm.nondegenerate_iff_det_ne_zero), so the dual lattice lies in r⁻¹ • span R (Set.range b).

The adjugate argument is adapted from Mathlib's Algebra.discr_mul_isIntegral_mem_adjoin, which treats the trace form of a separable field extension and a power basis; here it is stated for an arbitrary bilinear form and basis.

source
theorem LinearMap.BilinForm.dualSubmoduleToDual_surjective {R : Type u_1} {K : Type u_2} {V : Type u_3} [CommRing R] [IsDomain R] [Field K] [Algebra R K] [IsFractionRing R K] [Module.IsTorsionFree R K] [AddCommGroup V] [Module R V] [Module K V] [IsScalarTower R K V] (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) (N : Submodule R V) [Submodule.IsLattice K N] :
Function.Surjective ⇑(B.dualSubmoduleToDual N)

For a nondegenerate bilinear form B over the fraction field and a full lattice N, Mathlib's canonical pairing B.dualSubmoduleToDual N from the dual lattice to the dual of N is surjective. No lattice basis is needed.

source
noncomputable def LinearMap.BilinForm.dualSubmoduleEquivDual {R : Type u_1} {K : Type u_2} {V : Type u_3} [CommRing R] [IsDomain R] [Field K] [Algebra R K] [IsFractionRing R K] [Module.IsTorsionFree R K] [AddCommGroup V] [Module R V] [Module K V] [IsScalarTower R K V] (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) (N : Submodule R V) [hN : Submodule.IsLattice K N] :
↥(B.dualSubmodule N) ≃ₗ[R] Module.Dual R ↥N

The dual submodule of a full lattice is canonically isomorphic to its R-linear dual whenever the ambient bilinear form is nondegenerate.

Instances For
    source
    @[simp]
    theorem LinearMap.BilinForm.dualSubmoduleEquivDual_apply {R : Type u_1} {K : Type u_2} {V : Type u_3} [CommRing R] [IsDomain R] [Field K] [Algebra R K] [IsFractionRing R K] [Module.IsTorsionFree R K] [AddCommGroup V] [Module R V] [Module K V] [IsScalarTower R K V] (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) (N : Submodule R V) [Submodule.IsLattice K N] (x : ↥(B.dualSubmodule N)) :
    (B.dualSubmoduleEquivDual hB N) x = (B.dualSubmoduleToDual N) x

    The underlying linear map of dualSubmoduleEquivDual is B.dualSubmoduleToDual N.

    source
    theorem LinearMap.BilinForm.dualSubmodule_dualSubmodule_flip {R : Type u_1} {K : Type u_2} {V : Type u_3} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [AddCommGroup V] [Module R V] [Module K V] [IsScalarTower R K V] (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) (N : Submodule R V) [Submodule.IsLattice K N] [Module.Free R ↥N] :
    B.dualSubmodule (B.flip.dualSubmodule N) = N

    Dualizing by B.flip and then by B recovers the original free full lattice.

    source
    theorem LinearMap.BilinForm.dualSubmodule_flip_dualSubmodule {R : Type u_1} {K : Type u_2} {V : Type u_3} [CommRing R] [Field K] [Algebra R K] [IsFractionRing R K] [AddCommGroup V] [Module R V] [Module K V] [IsScalarTower R K V] (B : LinearMap.BilinForm K V) (hB : B.Nondegenerate) (N : Submodule R V) [Submodule.IsLattice K N] [Module.Free R ↥N] :
    B.flip.dualSubmodule (B.dualSubmodule N) = N

    Dualizing by B and then by B.flip recovers the original free full lattice.

    source
    theorem LinearMap.BilinForm.fg_of_le_dualSubmodule {A : Type u_4} {K : Type u_5} {M : Type u_6} [CommRing A] [Field K] [AddCommGroup M] [Algebra A K] [Module A M] [Module K M] [IsScalarTower A K M] [FiniteDimensional K M] [IsNoetherianRing A] {B : LinearMap.BilinForm K M} (hB : B.Nondegenerate) {N : Submodule A M} (hspan : Submodule.span K ↑N = ⊤) (hN : N ≤ B.dualSubmodule N) :
    N.FG

    Over a Noetherian ring A, a submodule N which spans a finite-dimensional K-vector space M and lies in its own dual for a nondegenerate bilinear form B is finitely generated: it lies in the A-span of the dual basis of a basis of M chosen inside N.