feat: OrderIso between finite-codimensional subspaces and finite-dime…

…nsional subspaces in the dual (#9124)

+ Introduce the nondegenerate pairing (`(flip_)quotDualCoannihilatorToDual_injective`) between `M ⧸ W.dualCoannihilator` and `W` . If `M` is a vector space and `W` is a finite-dimensional subspace of its dual, this is a perfect pairing (`quotDualCoannihilatorToDual_bijective`), and `W` is equal to the annihilator of its coannihilator.

+ Use this pairing to show that `dualAnnihilator` and `dualCoannihilator` give an antitone order isomorphism `orderIsoFiniteCodimDim` between finite-codimensional subspaces in a vector space and finite-dimensional subspaces in its dual. This result can be e.g. found in Bourbaki's Algebra. For a finite-dimensional vector space, this gives an OrderIso between all subspaces and all subspaces of the dual.

+ Add some lemmas about the image and preimage of annihilators and coannihilators under `Dual.eval`.

+ Expand the docstring of `basis_finite_of_finite_spans` with comments on generalizations.

- [x] depends on: #8820 



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Mathlib/LinearAlgebra/Dimension.lean

@@ -362,7 +362,15 @@ theorem LinearIndependent.set_finite_of_isNoetherian [IsNoetherian R M] {s : Set
 -- One might hope that a finite spanning set implies that any linearly independent set is finite.
 -- While this is true over a division ring
 -- (simply because any linearly independent set can be extended to a basis),
--- I'm not certain what more general statements are possible.
+-- or over a ring satisfying the strong rank condition
+-- (which covers all commutative rings; see `LinearIndependent.finite_of_le_span_finite`).
+-- this is not true in general.
+-- For example, the left ideal generated by the variables in a noncommutative polynomial ring
+-- (`FreeAlgebra R ι`) in infinitely many variables (indexed by `ι`) is free
+-- with an infinite basis (consisting of the variables).
+-- As another example, for any commutative ring R, the ring of column-finite matrices
+-- `Module.End R (ℕ →₀ R)` is isomorphic to `ℕ → Module.End R (ℕ →₀ R)` as a module over itself,
+-- which also clearly contains an infinite linearly independent set.
 /--
 Over any nontrivial ring, the existence of a finite spanning set implies that any basis is finite.
 -/

Mathlib/LinearAlgebra/Dual.lean

@@ -62,6 +62,9 @@ The dual space of an $R$-module $M$ is the $R$-module of $R$-linear maps $M \to
     `LinearMap.range_dual_map_eq_dualAnnihilator_ker`.
   * `Submodule.dualQuotEquivDualAnnihilator` is the equivalence
     `Dual R (M ⧸ W) ≃ₗ[R] W.dualAnnihilator`
+  * `Submodule.quotDualCoannihilatorToDual` is the nondegenerate pairing
+    `M ⧸ W.dualCoannihilator →ₗ[R] Dual R W`.
+    It is an perfect pairing when `R` is a field and `W` is finite-dimensional.
 * Vector spaces:
   * `Subspace.dualAnnihilator_dualConnihilator_eq` says that the double dual annihilator,
     pulled back ground `Module.Dual.eval`, is the original submodule.
@@ -76,6 +79,10 @@ The dual space of an $R$-module $M$ is the $R$-module of $R$-linear maps $M \to
   * `Module.evalEquiv` is the equivalence `V ≃ₗ[K] Dual K (Dual K V)`
   * `Module.mapEvalEquiv` is the order isomorphism between subspaces of `V` and
     subspaces of `Dual K (Dual K V)`.
+  * `Subspace.orderIsoFiniteCodimDim` is the antitone order isomorphism between
+    finite-codimensional subspaces of `V` and finite-dimensional subspaces of `Dual K V`.
+  * `Subspace.orderIsoFiniteDimensional` is the antitone order isomorphism between
+    subspaces of a finite-dimensional vector space `V` and subspaces of its dual.
   * `Subspace.quotDualEquivAnnihilator W` is the equivalence
     `(Dual K V ⧸ W.dualLift.range) ≃ₗ[K] W.dualAnnihilator`, where `W.dualLift.range` is a copy
     of `Dual K W` inside `Dual K V`.
@@ -902,7 +909,15 @@ theorem mem_dualCoannihilator {Φ : Submodule R (Module.Dual R M)} (x : M) :
   simp_rw [dualCoannihilator, mem_comap, mem_dualAnnihilator, Module.Dual.eval_apply]
 #align submodule.mem_dual_coannihilator Submodule.mem_dualCoannihilator
 
-theorem dualAnnihilator_gc (R M : Type*) [CommSemiring R] [AddCommMonoid M] [Module R M] :
+theorem comap_dualAnnihilator (Φ : Submodule R (Module.Dual R M)) :
+    Φ.dualAnnihilator.comap (Module.Dual.eval R M) = Φ.dualCoannihilator := rfl
+
+theorem map_dualCoannihilator_le (Φ : Submodule R (Module.Dual R M)) :
+    Φ.dualCoannihilator.map (Module.Dual.eval R M) ≤ Φ.dualAnnihilator :=
+  map_le_iff_le_comap.mpr (comap_dualAnnihilator Φ).le
+
+variable (R M) in
+theorem dualAnnihilator_gc :
     GaloisConnection
       (OrderDual.toDual ∘ (dualAnnihilator : Submodule R M → Submodule R (Module.Dual R M)))
       (dualCoannihilator ∘ OrderDual.ofDual) := by
@@ -1042,6 +1057,14 @@ theorem forall_mem_dualAnnihilator_apply_eq_zero_iff (W : Subspace K V) (v : V)
   rw [← SetLike.ext_iff.mp dualAnnihilator_dualCoannihilator_eq v, mem_dualCoannihilator]
 #align subspace.forall_mem_dual_annihilator_apply_eq_zero_iff Subspace.forall_mem_dualAnnihilator_apply_eq_zero_iff
 
+theorem comap_dualAnnihilator_dualAnnihilator (W : Subspace K V) :
+    W.dualAnnihilator.dualAnnihilator.comap (Module.Dual.eval K V) = W := by
+  ext; rw [Iff.comm, ← forall_mem_dualAnnihilator_apply_eq_zero_iff]; simp
+
+theorem map_le_dualAnnihilator_dualAnnihilator (W : Subspace K V) :
+    W.map (Module.Dual.eval K V) ≤ W.dualAnnihilator.dualAnnihilator :=
+  map_le_iff_le_comap.mpr (comap_dualAnnihilator_dualAnnihilator W).ge
+
 /-- `Submodule.dualAnnihilator` and `Submodule.dualCoannihilator` form a Galois coinsertion. -/
 def dualAnnihilatorGci (K V : Type*) [Field K] [AddCommGroup V] [Module K V] :
     GaloisCoinsertion
@@ -1145,16 +1168,14 @@ section
 
 open FiniteDimensional
 
-variable {V₁ : Type*} [AddCommGroup V₁] [Module K V₁]
-
 instance instModuleDualFiniteDimensional [FiniteDimensional K V] :
     FiniteDimensional K (Module.Dual K V) := by
   infer_instance
 #align subspace.module.dual.finite_dimensional Subspace.instModuleDualFiniteDimensional
 
 @[simp]
 theorem dual_finrank_eq : finrank K (Module.Dual K V) = finrank K V := by
-  by_cases h : Module.Finite K V
+  by_cases h : FiniteDimensional K V
   · classical exact LinearEquiv.finrank_eq (Basis.ofVectorSpace K V).toDualEquiv.symm
   rw [finrank_eq_zero_of_basis_imp_false, finrank_eq_zero_of_basis_imp_false]
   · exact fun _ b ↦ h (Module.Finite.of_basis b)
@@ -1308,7 +1329,7 @@ theorem range_dualMap_mkQ_eq (W : Submodule R M) :
     exists W.dualCopairing ⟨φ, hφ⟩
 #align submodule.range_dual_map_mkq_eq Submodule.range_dualMap_mkQ_eq
 
-/-- Equivalence $(M/W)^* \approx \operatorname{ann}(W)$. That is, there is a one-to-one
+/-- Equivalence $(M/W)^* \cong \operatorname{ann}(W)$. That is, there is a one-to-one
 correspondence between the dual of `M ⧸ W` and those elements of the dual of `M` that
 vanish on `W`.
 
@@ -1339,6 +1360,37 @@ theorem dualQuotEquivDualAnnihilator_symm_apply_mk (W : Submodule R M) (φ : W.d
   rfl
 #align submodule.dual_quot_equiv_dual_annihilator_symm_apply_mk Submodule.dualQuotEquivDualAnnihilator_symm_apply_mk
 
+theorem finite_dualAnnihilator_iff {W : Submodule R M} [Free R (M ⧸ W)] :
+    Finite R W.dualAnnihilator ↔ Finite R (M ⧸ W) :=
+  (Finite.equiv_iff W.dualQuotEquivDualAnnihilator.symm).trans (finite_dual_iff R)
+
+open LinearMap in
+/-- The pairing between a submodule `W` of a dual module `Dual R M` and the quotient of
+`M` by the coannihilator of `W`, which is always nondegenerate. -/
+def quotDualCoannihilatorToDual (W : Submodule R (Dual R M)) :
+    M ⧸ W.dualCoannihilator →ₗ[R] Dual R W :=
+  liftQ _ (flip <| Submodule.subtype _) le_rfl
+
+@[simp]
+theorem quotDualCoannihilatorToDual_apply (W : Submodule R (Dual R M)) (m : M) (w : W) :
+    W.quotDualCoannihilatorToDual (Quotient.mk m) w = w.1 m := rfl
+
+theorem quotDualCoannihilatorToDual_injective (W : Submodule R (Dual R M)) :
+    Function.Injective W.quotDualCoannihilatorToDual :=
+  LinearMap.ker_eq_bot.mp (ker_liftQ_eq_bot _ _ _ le_rfl)
+
+theorem flip_quotDualCoannihilatorToDual_injective (W : Submodule R (Dual R M)) :
+    Function.Injective W.quotDualCoannihilatorToDual.flip :=
+  fun _ _ he ↦ Subtype.ext <| LinearMap.ext fun m ↦ FunLike.congr_fun he ⟦m⟧
+
+open LinearMap in
+theorem quotDualCoannihilatorToDual_nondegenerate (W : Submodule R (Dual R M)) :
+    W.quotDualCoannihilatorToDual.Nondegenerate := by
+  rw [Nondegenerate, separatingLeft_iff_ker_eq_bot, separatingRight_iff_flip_ker_eq_bot]
+  letI : AddCommGroup W := inferInstance
+  simp_rw [ker_eq_bot]
+  exact ⟨W.quotDualCoannihilatorToDual_injective, W.flip_quotDualCoannihilatorToDual_injective⟩
+
 end Submodule
 
 namespace LinearMap
@@ -1557,6 +1609,77 @@ theorem flip_bijective_iff₂ [FiniteDimensional K V₂] : Bijective B.flip ↔
 
 end LinearMap
 
+namespace Subspace
+
+variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
+
+theorem quotDualCoannihilatorToDual_bijective (W : Subspace K (Dual K V)) [FiniteDimensional K W] :
+    Function.Bijective W.quotDualCoannihilatorToDual :=
+  ⟨W.quotDualCoannihilatorToDual_injective, letI : AddCommGroup W := inferInstance
+    flip_injective_iff₂.mp W.flip_quotDualCoannihilatorToDual_injective⟩
+
+theorem flip_quotDualCoannihilatorToDual_bijective (W : Subspace K (Dual K V))
+    [FiniteDimensional K W] : Function.Bijective W.quotDualCoannihilatorToDual.flip :=
+  letI : AddCommGroup W := inferInstance
+  flip_bijective_iff₂.mpr W.quotDualCoannihilatorToDual_bijective
+
+theorem dualCoannihilator_dualAnnihilator_eq {W : Subspace K (Dual K V)} [FiniteDimensional K W] :
+    W.dualCoannihilator.dualAnnihilator = W :=
+  let e := (LinearEquiv.ofBijective _ W.flip_quotDualCoannihilatorToDual_bijective).trans
+    (Submodule.dualQuotEquivDualAnnihilator _)
+  letI : AddCommGroup W := inferInstance
+  haveI : FiniteDimensional K W.dualCoannihilator.dualAnnihilator := LinearEquiv.finiteDimensional e
+  (eq_of_le_of_finrank_eq W.le_dualCoannihilator_dualAnnihilator e.finrank_eq).symm
+
+theorem finiteDimensional_quot_dualCoannihilator_iff {W : Submodule K (Dual K V)} :
+    FiniteDimensional K (V ⧸ W.dualCoannihilator) ↔ FiniteDimensional K W :=
+  ⟨fun _ ↦ FiniteDimensional.of_injective _ W.flip_quotDualCoannihilatorToDual_injective,
+    fun _ ↦ have := Basis.dual_finite (R := K) (M := W)
+    FiniteDimensional.of_injective _ W.quotDualCoannihilatorToDual_injective⟩
+
+open OrderDual in
+/-- For any vector space, `dualAnnihilator` and `dualCoannihilator` gives an antitone order
+  isomorphism between the finite-codimensional subspaces in the vector space and the
+  finite-dimensional subspaces in its dual. -/
+def orderIsoFiniteCodimDim :
+    {W : Subspace K V // FiniteDimensional K (V ⧸ W)} ≃o
+    {W : Subspace K (Dual K V) // FiniteDimensional K W}ᵒᵈ where
+  toFun W := toDual ⟨W.1.dualAnnihilator, Submodule.finite_dualAnnihilator_iff.mpr W.2⟩
+  invFun W := ⟨(ofDual W).1.dualCoannihilator,
+    finiteDimensional_quot_dualCoannihilator_iff.mpr (ofDual W).2⟩
+  left_inv _ := Subtype.ext dualAnnihilator_dualCoannihilator_eq
+  right_inv W := have := (ofDual W).2; Subtype.ext dualCoannihilator_dualAnnihilator_eq
+  map_rel_iff' := dualAnnihilator_le_dualAnnihilator_iff
+
+open OrderDual in
+/-- For any finite-dimensional vector space, `dualAnnihilator` and `dualCoannihilator` give
+  an antitone order isomorphism between the subspaces in the vector space and the subspaces
+  in its dual. -/
+def orderIsoFiniteDimensional [FiniteDimensional K V] :
+    Subspace K V ≃o (Subspace K (Dual K V))ᵒᵈ where
+  toFun W := toDual W.dualAnnihilator
+  invFun W := (ofDual W).dualCoannihilator
+  left_inv _ := dualAnnihilator_dualCoannihilator_eq
+  right_inv _ := dualCoannihilator_dualAnnihilator_eq
+  map_rel_iff' := dualAnnihilator_le_dualAnnihilator_iff
+
+open Submodule in
+theorem dualAnnihilator_dualAnnihilator_eq_map (W : Subspace K V) [FiniteDimensional K W] :
+    W.dualAnnihilator.dualAnnihilator = W.map (Dual.eval K V) := by
+  let e1 := (Free.chooseBasis K W).toDualEquiv ≪≫ₗ W.quotAnnihilatorEquiv.symm
+  haveI := e1.finiteDimensional
+  let e2 := (Free.chooseBasis K _).toDualEquiv ≪≫ₗ W.dualAnnihilator.dualQuotEquivDualAnnihilator
+  haveI := LinearEquiv.finiteDimensional (V₂ := W.dualAnnihilator.dualAnnihilator) e2
+  rw [FiniteDimensional.eq_of_le_of_finrank_eq (map_le_dualAnnihilator_dualAnnihilator W)]
+  rw [← (equivMapOfInjective _ (eval_apply_injective K (V := V)) W).finrank_eq, e1.finrank_eq]
+  exact e2.finrank_eq
+
+theorem map_dualCoannihilator (W : Subspace K (Dual K V)) [FiniteDimensional K V] :
+    W.dualCoannihilator.map (Dual.eval K V) = W.dualAnnihilator := by
+  rw [← dualAnnihilator_dualAnnihilator_eq_map, dualCoannihilator_dualAnnihilator_eq]
+
+end Subspace
+
 end FiniteDimensional
 
 end VectorSpace

Mathlib/RingTheory/Finiteness.lean

@@ -642,6 +642,9 @@ theorem equiv [Finite R M] (e : M ≃ₗ[R] N) : Finite R N :=
   of_surjective (e : M →ₗ[R] N) e.surjective
 #align module.finite.equiv Module.Finite.equiv
 
+theorem equiv_iff (e : M ≃ₗ[R] N) : Finite R M ↔ Finite R N :=
+  ⟨fun _ ↦ equiv e, fun _ ↦ equiv e.symm⟩
+
 instance ulift [Finite R M] : Finite R (ULift M) := equiv ULift.moduleEquiv.symm
 
 section Algebra