[Merged by Bors] - feat: Define dual submodule wrt bilinear form

[erdOne]

---

[riccardobrasca]

Thanks!

bors d+

[riccardobrasca]

FiniteDimensional S M is automatic since you have a finite basis.

[erdOne]

But dualBasis needs [FiniteDimensional S M]. Or maybe we should remove that from dualBasis.

[riccardobrasca]

You can write

let _ : FiniteDimensional S M := ...

before the : and it should be happy (not 100% sure the syntax is exactly that, but it is similar, and I forgot if we want let or letI here).

[riccardobrasca]

lemma dualSubmodule_span_of_basis {ι} [Fintype ι] [DecidableEq ι] (hB : B.Nondegenerate)
    (b : Basis ι S M) :
    letI _ : FiniteDimensional S M := FiniteDimensional.of_fintype_basis b
    B.dualSubmodule (Submodule.span R (Set.range b)) =
      Submodule.span R (Set.range <| B.dualBasis hB b) := by
  let _ : FiniteDimensional S M := FiniteDimensional.of_fintype_basis b
  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⟩

[erdOne]

I added that over at dualBasis.

[mathlib-bors]

✌️ erdOne can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[erdOne]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Check all files imported