Commit 2023-01-24 00:38 68626536

feat(linear_algebra/dual): more about dual annihilator, some refactoring, and documentation (#17521)

• Extend documentation with descriptions of main definitions and results.
• Move linear_map.dual_map earlier in the file and redefine it to use module.transpose.
• fintype -> set.finite for module.dual_bases.
• Rename submodule.dual_annihilator_comap to submodule.dual_coannihilator.
• Add galois correspondence and coinsertion for submodule.dual_annihilator; replace proofs using standard GC lemmas.
• Add submodule.dual_pairing and submodule.dual_copairing for bilinear forms that are nondegenerate for subspaces.
• Add missing isomorphisms associated to these.
• Generalize f.dual_map.range = f.ker.dual_annihilator to vector spaces of arbitrary dimension.
• Add lemmas for facts such as (W ⊓ W').dual_annihilator = W.dual_annihilator ⊔ W'.dual_annihilator. Thanks to Junyan Xu for the generalization to dual_quot_equiv_dual_annihilator.