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 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 : BilinForm S M) (N : Submodule R M) : Submodule R M

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

Equations

• BilinForm.dualSubmodule B N = { toAddSubmonoid := { toAddSubsemigroup := { carrier := {x : M | ∀ y ∈ N, B.bilin x y ∈ 1}, add_mem' := ⋯ }, zero_mem' := ⋯ }, smul_mem' := ⋯ }

theorem 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 : BilinForm S M) {N : Submodule R M} {x : M} : x ∈ BilinForm.dualSubmodule B N ↔ ∀ y ∈ N, B.bilin x y ∈ 1

theorem 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 : BilinForm S M) {N₁ : Submodule R M} {N₂ : Submodule R M} : N₁ ≤ BilinForm.dualSubmodule (BilinForm.flip B) N₂ ↔ N₂ ≤ BilinForm.dualSubmodule B N₁

noncomputable def 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 : BilinForm S M) {N : Submodule R M} (x : ↥(BilinForm.dualSubmodule B N)) (y : ↥N) : R

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

Equations

• BilinForm.dualSubmoduleParing B x y = Exists.choose ⋯

@[simp]

theorem 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 : BilinForm S M) {N : Submodule R M} (x : ↥(BilinForm.dualSubmodule B N)) (y : ↥N) : (algebraMap R S) (BilinForm.dualSubmoduleParing B x y) = B.bilin ↑x ↑y

@[simp]

theorem 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 : BilinForm S M) [NoZeroSMulDivisors R S] (N : Submodule R M) (x : ↥(BilinForm.dualSubmodule B N)) (y : ↥N) : ((BilinForm.dualSubmoduleToDual B N) x) y = BilinForm.dualSubmoduleParing B x y

noncomputable def 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 : BilinForm S M) [NoZeroSMulDivisors R S] (N : Submodule R M) : ↥(BilinForm.dualSubmodule B N) →ₗ[R] Module.Dual R ↥N

The natural paring of B.dualSubmodule N and N.

Equations

• One or more equations did not get rendered due to their size.

theorem 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 : BilinForm S M) (hB : BilinForm.Nondegenerate B) [NoZeroSMulDivisors R S] (N : Submodule R M) (hN : Submodule.span S ↑N = ⊤) : Function.Injective ⇑(BilinForm.dualSubmoduleToDual B N)

theorem 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 : BilinForm S M) {ι : Type u_1} [Finite ι] [DecidableEq ι] (hB : BilinForm.Nondegenerate B) (b : Basis ι S M) : BilinForm.dualSubmodule B (Submodule.span R (Set.range ⇑b)) = Submodule.span R (Set.range ⇑(BilinForm.dualBasis B hB b))

theorem 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 : BilinForm S M) {ι : Type u_1} [Finite ι] (hB : BilinForm.Nondegenerate B) (b : Basis ι S M) : BilinForm.dualSubmodule B (BilinForm.dualSubmodule (BilinForm.flip B) (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)

theorem 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 : BilinForm S M) {ι : Type u_1} [Finite ι] (hB : BilinForm.Nondegenerate B) (b : Basis ι S M) : BilinForm.dualSubmodule (BilinForm.flip B) (BilinForm.dualSubmodule B (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)

theorem 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 : BilinForm S M) {ι : Type u_1} [Finite ι] (hB : BilinForm.Nondegenerate B) (hB' : BilinForm.IsSymm B) (b : Basis ι S M) : BilinForm.dualSubmodule B (BilinForm.dualSubmodule B (Submodule.span R (Set.range ⇑b))) = Submodule.span R (Set.range ⇑b)