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} [CommRing R] [Field S] [AddCommGroup M] [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M] (B : LinearMap.BilinForm S M) (N : Submodule R M) : Submodule R M

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

Equations

• B.dualSubmodule N = { carrier := {x : M | ∀ y ∈ N, (B x) y ∈ 1}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem LinearMap.BilinForm.mem_dualSubmodule {R : Type u_1} {S : Type u_3} {M : Type u_2} [CommRing R] [Field S] [AddCommGroup M] [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M] (B : LinearMap.BilinForm S M) {N : Submodule R M} {x : M} : x ∈ B.dualSubmodule N ↔ ∀ y ∈ N, (B x) y ∈ 1

theorem LinearMap.BilinForm.le_flip_dualSubmodule {R : Type u_1} {S : Type u_3} {M : Type u_2} [CommRing R] [Field S] [AddCommGroup M] [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M] (B : LinearMap.BilinForm S M) {N₁ : Submodule R M} {N₂ : Submodule R M} : 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} [CommRing R] [Field S] [AddCommGroup M] [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M] (B : LinearMap.BilinForm S M) {N : Submodule R M} (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 = Exists.choose ⋯

@[simp]

theorem LinearMap.BilinForm.dualSubmoduleParing_spec {R : Type u_1} {S : Type u_3} {M : Type u_2} [CommRing R] [Field S] [AddCommGroup M] [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M] (B : LinearMap.BilinForm S M) {N : Submodule R M} (x : ↥(B.dualSubmodule N)) (y : ↥N) : (algebraMap R S) (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} [CommRing R] [Field S] [AddCommGroup M] [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M] (B : LinearMap.BilinForm S M) [NoZeroSMulDivisors R S] (N : Submodule R M) (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} [CommRing R] [Field S] [AddCommGroup M] [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M] (B : LinearMap.BilinForm S M) [NoZeroSMulDivisors R S] (N : Submodule R M) : ↥(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' := ⋯ }

theorem LinearMap.BilinForm.dualSubmoduleToDual_injective {R : Type u_3} {S : Type u_2} {M : Type u_1} [CommRing R] [Field S] [AddCommGroup M] [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M] (B : LinearMap.BilinForm S M) (hB : B.Nondegenerate) [NoZeroSMulDivisors R S] (N : Submodule R M) (hN : Submodule.span S ↑N = ⊤) : Function.Injective ⇑(B.dualSubmoduleToDual N)

theorem LinearMap.BilinForm.dualSubmodule_span_of_basis {R : Type u_4} {S : Type u_3} {M : Type u_2} [CommRing R] [Field S] [AddCommGroup M] [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M] (B : LinearMap.BilinForm S M) {ι : Type u_1} [Finite ι] [DecidableEq ι] (hB : B.Nondegenerate) (b : Basis ι S M) : B.dualSubmodule (Submodule.span R (Set.range ⇑b)) = 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} [CommRing R] [Field S] [AddCommGroup M] [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M] (B : LinearMap.BilinForm S M) {ι : Type u_1} [Finite ι] (hB : B.Nondegenerate) (b : Basis ι S M) : B.dualSubmodule (B.flip.dualSubmodule (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)

theorem LinearMap.BilinForm.dualSubmodule_flip_dualSubmodule_of_basis {R : Type u_4} {S : Type u_3} {M : Type u_2} [CommRing R] [Field S] [AddCommGroup M] [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M] (B : LinearMap.BilinForm S M) {ι : Type u_1} [Finite ι] (hB : B.Nondegenerate) (b : Basis ι S M) : B.flip.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)

theorem LinearMap.BilinForm.dualSubmodule_dualSubmodule_of_basis {R : Type u_4} {S : Type u_3} {M : Type u_2} [CommRing R] [Field S] [AddCommGroup M] [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M] (B : LinearMap.BilinForm S M) {ι : Type u_1} [Finite ι] (hB : B.Nondegenerate) (hB' : B.IsSymm) (b : Basis ι S M) : B.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)