# Dual submodule with respect to a bilinear form. #

## Main definitions and results #

• BilinForm.dualSubmodule: The dual submodule with respect to a bilinear form.
• BilinForm.dualSubmodule_span_of_basis: The dual of a lattice is spanned by the dual basis.

## TODO #

Properly develop the material in the context of lattices.

def LinearMap.BilinForm.dualSubmodule {R : Type u_1} {S : Type u_2} {M : Type u_3} [] [] [] [Algebra R S] [Module R M] [Module S M] [] (B : ) (N : ) :

The dual submodule of a submodule with respect to a bilinear form.

Equations
• B.dualSubmodule N = { carrier := {x : M | yN, (B x) y 1}, add_mem' := , zero_mem' := , smul_mem' := }
Instances For
theorem LinearMap.BilinForm.mem_dualSubmodule {R : Type u_1} {S : Type u_3} {M : Type u_2} [] [] [] [Algebra R S] [Module R M] [Module S M] [] (B : ) {N : } {x : M} :
x B.dualSubmodule N yN, (B x) y 1
theorem LinearMap.BilinForm.le_flip_dualSubmodule {R : Type u_1} {S : Type u_3} {M : Type u_2} [] [] [] [Algebra R S] [Module R M] [Module S M] [] (B : ) {N₁ : } {N₂ : } :
N₁ B.flip.dualSubmodule N₂ N₂ B.dualSubmodule N₁
noncomputable def LinearMap.BilinForm.dualSubmoduleParing {R : Type u_1} {S : Type u_2} {M : Type u_3} [] [] [] [Algebra R S] [Module R M] [Module S M] [] (B : ) {N : } (x : (B.dualSubmodule N)) (y : N) :
R

The natural paring of B.dualSubmodule N and N. This is bundled as a bilinear map in BilinForm.dualSubmoduleToDual.

Equations
• B.dualSubmoduleParing x y =
Instances For
@[simp]
theorem LinearMap.BilinForm.dualSubmoduleParing_spec {R : Type u_1} {S : Type u_3} {M : Type u_2} [] [] [] [Algebra R S] [Module R M] [Module S M] [] (B : ) {N : } (x : (B.dualSubmodule N)) (y : N) :
() (B.dualSubmoduleParing x y) = (B x) y
@[simp]
theorem LinearMap.BilinForm.dualSubmoduleToDual_apply_apply {R : Type u_1} {S : Type u_2} {M : Type u_3} [] [] [] [Algebra R S] [Module R M] [Module S M] [] (B : ) [] (N : ) (x : (B.dualSubmodule N)) (y : N) :
((B.dualSubmoduleToDual N) x) y = B.dualSubmoduleParing x y
noncomputable def LinearMap.BilinForm.dualSubmoduleToDual {R : Type u_1} {S : Type u_2} {M : Type u_3} [] [] [] [Algebra R S] [Module R M] [Module S M] [] (B : ) [] (N : ) :
(B.dualSubmodule N) →ₗ[R] Module.Dual R N

The natural paring of B.dualSubmodule N and N.

Equations
• B.dualSubmoduleToDual N = { toFun := fun (x : (B.dualSubmodule N)) => { toFun := B.dualSubmoduleParing x, map_add' := , map_smul' := }, map_add' := , map_smul' := }
Instances For
theorem LinearMap.BilinForm.dualSubmoduleToDual_injective {R : Type u_3} {S : Type u_2} {M : Type u_1} [] [] [] [Algebra R S] [Module R M] [Module S M] [] (B : ) (hB : B.Nondegenerate) [] (N : ) (hN : = ) :
Function.Injective (B.dualSubmoduleToDual N)
theorem LinearMap.BilinForm.dualSubmodule_span_of_basis {R : Type u_4} {S : Type u_3} {M : Type u_2} [] [] [] [Algebra R S] [Module R M] [Module S M] [] (B : ) {ι : Type u_1} [] [] (hB : B.Nondegenerate) (b : Basis ι S M) :
B.dualSubmodule (Submodule.span R ()) = Submodule.span R (Set.range (B.dualBasis hB b))
theorem LinearMap.BilinForm.dualSubmodule_dualSubmodule_flip_of_basis {R : Type u_4} {S : Type u_3} {M : Type u_2} [] [] [] [Algebra R S] [Module R M] [Module S M] [] (B : ) {ι : Type u_1} [] (hB : B.Nondegenerate) (b : Basis ι S M) :
B.dualSubmodule (B.flip.dualSubmodule (Submodule.span R ())) = Submodule.span R ()
theorem LinearMap.BilinForm.dualSubmodule_flip_dualSubmodule_of_basis {R : Type u_4} {S : Type u_3} {M : Type u_2} [] [] [] [Algebra R S] [Module R M] [Module S M] [] (B : ) {ι : Type u_1} [] (hB : B.Nondegenerate) (b : Basis ι S M) :
B.flip.dualSubmodule (B.dualSubmodule (Submodule.span R ())) = Submodule.span R ()
theorem LinearMap.BilinForm.dualSubmodule_dualSubmodule_of_basis {R : Type u_4} {S : Type u_3} {M : Type u_2} [] [] [] [Algebra R S] [Module R M] [Module S M] [] (B : ) {ι : Type u_1} [] (hB : B.Nondegenerate) (hB' : B.IsSymm) (b : Basis ι S M) :
B.dualSubmodule (B.dualSubmodule (Submodule.span R ())) = Submodule.span R ()