feat: Define dual submodule wrt bilinear form (#8997)

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Mathlib.lean

@@ -2331,6 +2331,7 @@ import Mathlib.LinearAlgebra.Basis.Bilinear
 import Mathlib.LinearAlgebra.Basis.Flag
 import Mathlib.LinearAlgebra.Basis.VectorSpace
 import Mathlib.LinearAlgebra.BilinearForm.Basic
+import Mathlib.LinearAlgebra.BilinearForm.DualLattice
 import Mathlib.LinearAlgebra.BilinearForm.Hom
 import Mathlib.LinearAlgebra.BilinearForm.Orthogonal
 import Mathlib.LinearAlgebra.BilinearForm.Properties

Mathlib/LinearAlgebra/BilinearForm/Basic.lean

@@ -61,6 +61,8 @@ structure BilinForm (R : Type*) (M : Type*) [Semiring R] [AddCommMonoid M] [Modu
 
 variable {R : Type*} {M : Type*} [Semiring R] [AddCommMonoid M] [Module R M]
 
+variable {S : Type*} [CommSemiring S] [Algebra S R] [Module S M] [IsScalarTower S R M]
+
 variable {R₁ : Type*} {M₁ : Type*} [Ring R₁] [AddCommGroup M₁] [Module R₁ M₁]
 
 variable {R₂ : Type*} {M₂ : Type*} [CommSemiring R₂] [AddCommMonoid M₂] [Module R₂ M₂]
@@ -137,6 +139,14 @@ theorem sub_right (x y z : M₁) : B₁ x (y - z) = B₁ x y - B₁ x z := by
   rw [sub_eq_add_neg, sub_eq_add_neg, add_right, neg_right]
 #align bilin_form.sub_right BilinForm.sub_right
 
+@[simp]
+lemma smul_left_of_tower (r : S) (x y : M) : B (r • x) y = r • B x y := by
+  rw [← IsScalarTower.algebraMap_smul R r, smul_left, Algebra.smul_def]
+
+@[simp]
+lemma smul_right_of_tower (r : S) (x y : M) : B x (r • y) = r • B x y := by
+  rw [← IsScalarTower.algebraMap_smul R r, smul_right, Algebra.smul_def]
+
 variable {D : BilinForm R M} {D₁ : BilinForm R₁ M₁}
 
 -- TODO: instantiate `FunLike`

Mathlib/LinearAlgebra/BilinearForm/DualLattice.lean

@@ -0,0 +1,130 @@
+/-
+Copyright (c) 2018 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import Mathlib.LinearAlgebra.BilinearForm.Properties
+
+/-!
+
+# 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.
+-/
+
+variable {R S M} [CommRing R] [Field S] [AddCommGroup M]
+variable [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M]
+
+namespace BilinForm
+
+variable (B : BilinForm S M)
+
+/-- The dual submodule of a submodule with respect to a bilinear form. -/
+def dualSubmodule (N : Submodule R M) : Submodule R M where
+  carrier := { x | ∀ y ∈ N, B x y ∈ (1 : Submodule R S) }
+  add_mem' {a b} ha hb y hy := by simpa using add_mem (ha y hy) (hb y hy)
+  zero_mem' y _ := by rw [B.zero_left]; exact zero_mem _
+  smul_mem' r a ha y hy := by
+    convert (1 : Submodule R S).smul_mem r (ha y hy)
+    rw [← IsScalarTower.algebraMap_smul S r a, bilin_smul_left, Algebra.smul_def]
+
+lemma mem_dualSubmodule {N : Submodule R M} {x} :
+    x ∈ B.dualSubmodule N ↔ ∀ y ∈ N, B x y ∈ (1 : Submodule R S) := Iff.rfl
+
+lemma le_flip_dualSubmodule {N₁ N₂ : Submodule R M} :
+    N₁ ≤ B.flip.dualSubmodule N₂ ↔ N₂ ≤ B.dualSubmodule N₁ := by
+  show (∀ (x : M), x ∈ N₁ → _) ↔ ∀ (x : M), x ∈ N₂ → _
+  simp only [mem_dualSubmodule, Submodule.mem_one, flip_apply]
+  exact forall₂_swap
+
+/-- The natural paring of `B.dualSubmodule N` and `N`.
+This is bundled as a bilinear map in `BilinForm.dualSubmoduleToDual`. -/
+noncomputable
+def dualSubmoduleParing {N : Submodule R M} (x : B.dualSubmodule N) (y : N) : R :=
+  (x.prop y y.prop).choose
+
+@[simp]
+lemma dualSubmoduleParing_spec {N : Submodule R M} (x : B.dualSubmodule N) (y : N) :
+    algebraMap R S (B.dualSubmoduleParing x y) = B x y :=
+  (x.prop y y.prop).choose_spec
+
+/-- The natural paring of `B.dualSubmodule N` and `N`. -/
+-- TODO: Show that this is perfect when `N` is a lattice and `B` is nondegenerate.
+@[simps]
+noncomputable
+def dualSubmoduleToDual [NoZeroSMulDivisors R S] (N : Submodule R M) :
+    B.dualSubmodule N →ₗ[R] Module.Dual R N :=
+  { toFun := fun x ↦
+    { toFun := B.dualSubmoduleParing x
+      map_add' := fun x y ↦ NoZeroSMulDivisors.algebraMap_injective R S (by simp)
+      map_smul' := fun r m ↦ NoZeroSMulDivisors.algebraMap_injective R S
+        (by simp [← Algebra.smul_def]) }
+    map_add' := fun x y ↦ LinearMap.ext fun z ↦ NoZeroSMulDivisors.algebraMap_injective R S
+      (by simp)
+    map_smul' := fun r x ↦ LinearMap.ext fun y ↦ NoZeroSMulDivisors.algebraMap_injective R S
+      (by simp [← Algebra.smul_def]) }
+
+lemma dualSubmoduleToDual_injective (hB : B.Nondegenerate) [NoZeroSMulDivisors R S]
+    (N : Submodule R M) (hN : Submodule.span S (N : Set M) = ⊤) :
+    Function.Injective (B.dualSubmoduleToDual N) := by
+  intro x y e
+  ext
+  apply LinearMap.ker_eq_bot.mp hB.ker_eq_bot
+  apply LinearMap.ext_on hN
+  intro z hz
+  simpa using congr_arg (algebraMap R S) (LinearMap.congr_fun e ⟨z, hz⟩)
+
+lemma dualSubmodule_span_of_basis {ι} [Fintype ι] [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) := by
+  apply le_antisymm
+  · intro x hx
+    rw [← (B.dualBasis hB b).sum_repr x]
+    apply sum_mem
+    rintro i -
+    obtain ⟨r, hr⟩ := hx (b i) (Submodule.subset_span ⟨_, rfl⟩)
+    simp only [dualBasis_repr_apply, ← hr, Algebra.linearMap_apply, algebraMap_smul]
+    apply Submodule.smul_mem
+    exact Submodule.subset_span ⟨_, rfl⟩
+  · rw [Submodule.span_le]
+    rintro _ ⟨i, rfl⟩ y hy
+    obtain ⟨f, rfl⟩ := (mem_span_range_iff_exists_fun _).mp hy
+    simp only [sum_right, bilin_smul_right]
+    apply sum_mem
+    rintro j -
+    rw [← IsScalarTower.algebraMap_smul S (f j), B.bilin_smul_right, apply_dualBasis_left,
+      mul_ite, mul_one, mul_zero, ← (algebraMap R S).map_zero, ← apply_ite]
+    exact ⟨_, rfl⟩
+
+lemma dualSubmodule_dualSubmodule_flip_of_basis {ι} [Fintype ι]
+    (hB : B.Nondegenerate) (b : Basis ι S M) :
+    B.dualSubmodule (B.flip.dualSubmodule (Submodule.span R (Set.range b))) =
+      Submodule.span R (Set.range b) := by
+  classical
+  letI := FiniteDimensional.of_fintype_basis b
+  rw [dualSubmodule_span_of_basis _ hB.flip, dualSubmodule_span_of_basis B hB,
+    dualBasis_dualBasis_flip B hB]
+
+lemma dualSubmodule_flip_dualSubmodule_of_basis {ι} [Fintype ι]
+    (hB : B.Nondegenerate) (b : Basis ι S M) :
+    B.flip.dualSubmodule (B.dualSubmodule (Submodule.span R (Set.range b))) =
+      Submodule.span R (Set.range b) := by
+  classical
+  letI := FiniteDimensional.of_fintype_basis b
+  rw [dualSubmodule_span_of_basis B hB, dualSubmodule_span_of_basis _ hB.flip,
+    dualBasis_flip_dualBasis B hB]
+
+lemma dualSubmodule_dualSubmodule_of_basis
+    {ι} [Fintype ι] (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) := by
+  classical
+  letI := FiniteDimensional.of_fintype_basis b
+  rw [dualSubmodule_span_of_basis B hB, dualSubmodule_span_of_basis B hB,
+    dualBasis_dualBasis B hB hB']

Mathlib/LinearAlgebra/BilinearForm/Properties.lean

@@ -461,6 +461,17 @@ theorem toDual_def {B : BilinForm K V} (b : B.Nondegenerate) {m n : V} : B.toDua
   rfl
 #align bilin_form.to_dual_def BilinForm.toDual_def
 
+lemma Nondegenerate.flip {B : BilinForm K V} (hB : B.Nondegenerate) :
+    B.flip.Nondegenerate := by
+  intro x hx
+  apply (Module.evalEquiv K V).injective
+  ext f
+  obtain ⟨y, rfl⟩ := (B.toDual hB).surjective f
+  simpa using hx y
+
+lemma nonDegenerateFlip_iff {B : BilinForm K V} :
+    B.flip.Nondegenerate ↔ B.Nondegenerate := ⟨Nondegenerate.flip, Nondegenerate.flip⟩
+
 section DualBasis
 
 variable {ι : Type*} [DecidableEq ι] [Fintype ι]
@@ -470,6 +481,7 @@ variable {ι : Type*} [DecidableEq ι] [Fintype ι]
 where `B` is a nondegenerate (symmetric) bilinear form and `b` is a finite basis. -/
 noncomputable def dualBasis (B : BilinForm K V) (hB : B.Nondegenerate) (b : Basis ι K V) :
     Basis ι K V :=
+  haveI := FiniteDimensional.of_fintype_basis b
   b.dualBasis.map (B.toDual hB).symm
 #align bilin_form.dual_basis BilinForm.dualBasis
 
@@ -482,6 +494,7 @@ theorem dualBasis_repr_apply (B : BilinForm K V) (hB : B.Nondegenerate) (b : Bas
 
 theorem apply_dualBasis_left (B : BilinForm K V) (hB : B.Nondegenerate) (b : Basis ι K V) (i j) :
     B (B.dualBasis hB b i) (b j) = if j = i then 1 else 0 := by
+  have := FiniteDimensional.of_fintype_basis b
   rw [dualBasis, Basis.map_apply, Basis.coe_dualBasis, ← toDual_def hB,
     LinearEquiv.apply_symm_apply, Basis.coord_apply, Basis.repr_self, Finsupp.single_apply]
 #align bilin_form.apply_dual_basis_left BilinForm.apply_dualBasis_left
@@ -491,6 +504,29 @@ theorem apply_dualBasis_right (B : BilinForm K V) (hB : B.Nondegenerate) (sym :
   rw [sym, apply_dualBasis_left]
 #align bilin_form.apply_dual_basis_right BilinForm.apply_dualBasis_right
 
+@[simp]
+lemma dualBasis_dualBasis_flip (B : BilinForm K V) (hB : B.Nondegenerate) {ι}
+    [Fintype ι] [DecidableEq ι] (b : Basis ι K V) :
+    B.dualBasis hB (B.flip.dualBasis hB.flip b) = b := by
+  ext i
+  refine LinearMap.ker_eq_bot.mp hB.ker_eq_bot ((B.flip.dualBasis hB.flip b).ext (fun j ↦ ?_))
+  rw [toLin_apply, apply_dualBasis_left, toLin_apply, ← B.flip_apply (R₂ := K),
+    apply_dualBasis_left]
+  simp_rw [@eq_comm _ i j]
+
+@[simp]
+lemma dualBasis_flip_dualBasis (B : BilinForm K V) (hB : B.Nondegenerate) {ι}
+    [Fintype ι] [DecidableEq ι] [FiniteDimensional K V] (b : Basis ι K V) :
+    B.flip.dualBasis hB.flip (B.dualBasis hB b) = b :=
+  dualBasis_dualBasis_flip _ hB.flip b
+
+@[simp]
+lemma dualBasis_dualBasis (B : BilinForm K V) (hB : B.Nondegenerate) (hB' : B.IsSymm) {ι}
+    [Fintype ι] [DecidableEq ι] [FiniteDimensional K V] (b : Basis ι K V) :
+    B.dualBasis hB (B.dualBasis hB b) = b := by
+  convert dualBasis_dualBasis_flip _ hB.flip b
+  rwa [eq_comm, ← isSymm_iff_flip]
+
 end DualBasis
 
 section LinearAdjoints