feat(linear_algebra/dimension): linear equiv iff eq dim (#5559)

See related zulip discussion
https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Classification.20of.20finite-dimensional.20vector.20spaces/near/221357275


Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

Author: 3 people

src/linear_algebra/basis.lean

@@ -235,7 +235,7 @@ def module_equiv_finsupp (hv : is_basis R v) : M ≃ₗ[R] ι →₀ R :=
 
 /-- Isomorphism between the two modules, given two modules `M` and `M'` with respective bases
 `v` and `v'` and a bijection between the indexing sets of the two bases. -/
-def equiv_of_is_basis {v : ι → M} {v' : ι' → M'} (hv : is_basis R v) (hv' : is_basis R v')
+def linear_equiv_of_is_basis {v : ι → M} {v' : ι' → M'} (hv : is_basis R v) (hv' : is_basis R v')
   (e : ι ≃ ι') : M ≃ₗ[R] M' :=
 { inv_fun := hv'.constr (v ∘ e.symm),
   left_inv := have (hv'.constr (v ∘ e.symm)).comp (hv.constr (v' ∘ e)) = linear_map.id,
@@ -248,7 +248,7 @@ def equiv_of_is_basis {v : ι → M} {v' : ι' → M'} (hv : is_basis R v) (hv'
 
 /-- Isomorphism between the two modules, given two modules `M` and `M'` with respective bases
 `v` and `v'` and a bijection between the two bases. -/
-def equiv_of_is_basis' {v : ι → M} {v' : ι' → M'} (f : M → M') (g : M' → M)
+def linear_equiv_of_is_basis' {v : ι → M} {v' : ι' → M'} (f : M → M') (g : M' → M)
   (hv : is_basis R v) (hv' : is_basis R v')
   (hf : ∀i, f (v i) ∈ range v') (hg : ∀i, g (v' i) ∈ range v)
   (hgf : ∀i, g (f (v i)) = v i) (hfg : ∀i, f (g (v' i)) = v' i) :
@@ -266,33 +266,33 @@ def equiv_of_is_basis' {v : ι → M} {v' : ι' → M'} (f : M → M') (g : M' 
     λ y, congr_arg (λ h:M' →ₗ[R] M', h y) this,
   ..hv.constr (f ∘ v) }
 
-@[simp] lemma equiv_of_is_basis_comp {ι'' : Type*} {v : ι → M} {v' : ι' → M'} {v'' : ι'' → M''}
-  (hv : is_basis R v) (hv' : is_basis R v') (hv'' : is_basis R v'')
+@[simp] lemma linear_equiv_of_is_basis_comp {ι'' : Type*} {v : ι → M} {v' : ι' → M'}
+  {v'' : ι'' → M''} (hv : is_basis R v) (hv' : is_basis R v') (hv'' : is_basis R v'')
   (e : ι ≃ ι') (f : ι' ≃ ι'' ) :
-  (equiv_of_is_basis hv hv' e).trans (equiv_of_is_basis hv' hv'' f) =
-  equiv_of_is_basis hv hv'' (e.trans f) :=
+  (linear_equiv_of_is_basis hv hv' e).trans (linear_equiv_of_is_basis hv' hv'' f) =
+  linear_equiv_of_is_basis hv hv'' (e.trans f) :=
 begin
   apply linear_equiv.injective_to_linear_map,
   apply hv.ext,
   intros i,
-  simp [equiv_of_is_basis]
+  simp [linear_equiv_of_is_basis]
 end
 
-@[simp] lemma equiv_of_is_basis_refl :
-  equiv_of_is_basis hv hv (equiv.refl ι) = linear_equiv.refl R M :=
+@[simp] lemma linear_equiv_of_is_basis_refl :
+  linear_equiv_of_is_basis hv hv (equiv.refl ι) = linear_equiv.refl R M :=
 begin
   apply linear_equiv.injective_to_linear_map,
   apply hv.ext,
   intros i,
-  simp [equiv_of_is_basis]
+  simp [linear_equiv_of_is_basis]
 end
 
-lemma equiv_of_is_basis_trans_symm (e : ι ≃ ι') {v' : ι' → M'} (hv' : is_basis R v') :
-  (equiv_of_is_basis hv hv' e).trans (equiv_of_is_basis hv' hv e.symm) = linear_equiv.refl R M :=
+lemma linear_equiv_of_is_basis_trans_symm (e : ι ≃ ι') {v' : ι' → M'} (hv' : is_basis R v') :
+  (linear_equiv_of_is_basis hv hv' e).trans (linear_equiv_of_is_basis hv' hv e.symm) = linear_equiv.refl R M :=
 by simp
 
-lemma equiv_of_is_basis_symm_trans (e : ι ≃ ι') {v' : ι' → M'} (hv' : is_basis R v') :
-  (equiv_of_is_basis hv' hv e.symm).trans (equiv_of_is_basis hv hv' e) = linear_equiv.refl R M' :=
+lemma linear_equiv_of_is_basis_symm_trans (e : ι ≃ ι') {v' : ι' → M'} (hv' : is_basis R v') :
+  (linear_equiv_of_is_basis hv' hv e.symm).trans (linear_equiv_of_is_basis hv hv' e) = linear_equiv.refl R M' :=
 by simp
 
 lemma is_basis_inl_union_inr {v : ι → M} {v' : ι' → M'}

src/linear_algebra/dimension.lean

@@ -145,13 +145,61 @@ hb.mk_eq_dim'' ▸ cardinal.card_le_of (λ s, @finset.card_map _ _ ⟨_, subtype
 
 variables [add_comm_group V'] [vector_space K V']
 
+/-- Two linearly equivalent vector spaces have the same dimension, a version with different
+universes. -/
+theorem linear_equiv.lift_dim_eq (f : V ≃ₗ[K] V') :
+  cardinal.lift.{v v'} (dim K V) = cardinal.lift.{v' v} (dim K V') :=
+let ⟨b, hb⟩ := exists_is_basis K V in
+calc cardinal.lift.{v v'} (dim K V) = cardinal.lift.{v v'} (cardinal.mk b) :
+  congr_arg _ hb.mk_eq_dim''.symm
+... = cardinal.lift.{v' v} (dim K V') : (f.is_basis hb).mk_eq_dim
+
 /-- Two linearly equivalent vector spaces have the same dimension. -/
 theorem linear_equiv.dim_eq (f : V ≃ₗ[K] V₁) :
   dim K V = dim K V₁ :=
-by letI := classical.dec_eq V;
-letI := classical.dec_eq V₁; exact
-let ⟨b, hb⟩ := exists_is_basis K V in
-cardinal.lift_inj.1 $ hb.mk_eq_dim.symm.trans (f.is_basis hb).mk_eq_dim
+cardinal.lift_inj.1 f.lift_dim_eq
+
+/-- Two vector spaces are isomorphic if they have the same dimension. -/
+theorem nonempty_linear_equiv_of_lift_dim_eq
+  (cond : cardinal.lift.{v v'} (dim K V) = cardinal.lift.{v' v} (dim K V')) :
+  nonempty (V ≃ₗ[K] V') :=
+begin
+  obtain ⟨B, h⟩ := exists_is_basis K V,
+  obtain ⟨B', h'⟩ := exists_is_basis K V',
+  have : cardinal.lift.{v v'} (cardinal.mk B) = cardinal.lift.{v' v} (cardinal.mk B'),
+    by rw [h.mk_eq_dim'', cond, h'.mk_eq_dim''],
+  exact (cardinal.lift_mk_eq.{v v' 0}.1 this).map (linear_equiv_of_is_basis h h')
+end
+
+/-- Two vector spaces are isomorphic if they have the same dimension. -/
+theorem nonempty_linear_equiv_of_dim_eq (cond : dim K V = dim K V₁) :
+  nonempty (V ≃ₗ[K] V₁) :=
+nonempty_linear_equiv_of_lift_dim_eq $ congr_arg _ cond
+
+section
+
+variables (V V' V₁)
+
+/-- Two vector spaces are isomorphic if they have the same dimension. -/
+def linear_equiv.of_lift_dim_eq
+  (cond : cardinal.lift.{v v'} (dim K V) = cardinal.lift.{v' v} (dim K V')) :
+  V ≃ₗ[K] V' :=
+classical.choice (nonempty_linear_equiv_of_lift_dim_eq cond)
+
+/-- Two vector spaces are isomorphic if they have the same dimension. -/
+def linear_equiv.of_dim_eq (cond : dim K V = dim K V₁) : V ≃ₗ[K] V₁ :=
+classical.choice (nonempty_linear_equiv_of_dim_eq cond)
+
+end
+
+/-- Two vector spaces are isomorphic if and only if they have the same dimension. -/
+theorem linear_equiv.nonempty_equiv_iff_lift_dim_eq :
+  nonempty (V ≃ₗ[K] V') ↔ cardinal.lift.{v v'} (dim K V) = cardinal.lift.{v' v} (dim K V') :=
+⟨λ ⟨h⟩, linear_equiv.lift_dim_eq h, λ h, nonempty_linear_equiv_of_lift_dim_eq h⟩
+
+/-- Two vector spaces are isomorphic if and only if they have the same dimension. -/
+theorem linear_equiv.nonempty_equiv_iff_dim_eq : nonempty (V ≃ₗ[K] V₁) ↔ dim K V = dim K V₁ :=
+⟨λ ⟨h⟩, linear_equiv.dim_eq h, λ h, nonempty_linear_equiv_of_dim_eq h⟩
 
 @[simp] lemma dim_bot : dim K (⊥ : submodule K V) = 0 :=
 by letI := classical.dec_eq V;

src/linear_algebra/finite_dimensional.lean

@@ -644,18 +644,40 @@ theorem findim_eq (f : V ≃ₗ[K] V₂) [finite_dimensional K V] :
   findim K V = findim K V₂ :=
 begin
   haveI : finite_dimensional K V₂ := f.finite_dimensional,
-  rcases exists_is_basis_finite K V with ⟨s, s_basis, s_finite⟩,
-  letI : fintype s := s_finite.fintype,
-  have A : findim K V = fintype.card s := findim_eq_card_basis s_basis,
-  have : is_basis K (λx:s, f (subtype.val x)) := f.is_basis s_basis,
-  have B : findim K V₂ = fintype.card s := findim_eq_card_basis this,
-  rw [A, B]
+  simpa [← findim_eq_dim] using f.lift_dim_eq
 end
 
 end linear_equiv
 
 namespace finite_dimensional
 
+/--
+Two finite-dimensional vector spaces are isomorphic if they have the same (finite) dimension.
+-/
+theorem nonempty_linear_equiv_of_findim_eq [finite_dimensional K V] [finite_dimensional K V₂]
+  (cond : findim K V = findim K V₂) : nonempty (V ≃ₗ[K] V₂) :=
+nonempty_linear_equiv_of_lift_dim_eq $ by simp only [← findim_eq_dim, cond, lift_nat_cast]
+
+/--
+Two finite-dimensional vector spaces are isomorphic if and only if they have the same (finite) dimension.
+-/
+theorem nonempty_linear_equiv_iff_findim_eq [finite_dimensional K V] [finite_dimensional K V₂] :
+   nonempty (V ≃ₗ[K] V₂) ↔ findim K V = findim K V₂ :=
+⟨λ ⟨h⟩, h.findim_eq, λ h, nonempty_linear_equiv_of_findim_eq h⟩
+
+section
+
+variables (V V₂)
+
+/--
+Two finite-dimensional vector spaces are isomorphic if they have the same (finite) dimension.
+-/
+noncomputable def linear_equiv.of_findim_eq [finite_dimensional K V] [finite_dimensional K V₂]
+  (cond : findim K V = findim K V₂) : V ≃ₗ[K] V₂ :=
+classical.choice $ nonempty_linear_equiv_of_findim_eq cond
+
+end
+
 lemma eq_of_le_of_findim_le {S₁ S₂ : submodule K V} [finite_dimensional K S₂] (hle : S₁ ≤ S₂)
   (hd : findim K S₂ ≤ findim K S₁) : S₁ = S₂ :=
 begin

src/linear_algebra/matrix.lean

@@ -451,7 +451,7 @@ lemma is_basis.iff_det {v : ι → M} : is_basis R v ↔ is_unit (he.det v) :=
 begin
   split,
   { intro hv,
-    suffices : is_unit (linear_map.to_matrix he he (equiv_of_is_basis he hv $ equiv.refl ι)).det,
+    suffices : is_unit (linear_map.to_matrix he he (linear_equiv_of_is_basis he hv $ equiv.refl ι)).det,
     { rw [is_basis.det_apply, is_basis.to_matrix_eq_to_matrix_constr],
       exact this },
     apply linear_equiv.is_unit_det },