Dual submodules of lattices

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

Main declarations

• LinearMap.BilinForm.dualSubmoduleToDual_surjective: surjectivity of dualSubmoduleToDual for a free full lattice and nondegenerate bilinear form.
• LinearMap.BilinForm.dualSubmoduleEquivDual: the perfect linear equivalence B.dualSubmodule N ≃ₗ[R] Module.Dual R N.
• LinearMap.BilinForm.dualSubmoduleEquivDual_apply: evaluation of dualSubmoduleEquivDual is B.dualSubmoduleToDual N.
• LinearMap.BilinForm.dualSubmodule_dualSubmodule_flip: double duality for general full lattices using B.flip.
• LinearMap.BilinForm.dualSubmodule_flip_dualSubmodule: double duality for general full lattices with B.flip on the outside.

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] [Module.Free R ↥N] : Function.Surjective ⇑(B.dualSubmoduleToDual N)

Surjectivity of Mathlib's canonical pairing dualSubmoduleToDual for a free full lattice and a nondegenerate bilinear form.

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] [Module.Free R ↥N] : ↥(B.dualSubmodule N) ≃ₗ[R] Module.Dual R ↥N

The canonical pairing between the dual submodule of a free full lattice and the lattice itself is a linear equivalence over R whenever the ambient bilinear form is nondegenerate.

Equations

• B.dualSubmoduleEquivDual hB N = LinearEquiv.ofBijective (B.dualSubmoduleToDual N) ⋯

@[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] [Module.Free R ↥N] (x : ↥(B.dualSubmodule N)) : (B.dualSubmoduleEquivDual hB N) x = (B.dualSubmoduleToDual N) x

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

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.

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.