chore(linear_algebra/dimension): more same-universe versions of is_basis.mk_eq_dim (#4591)

While all the `lift` magic is good for general theory, it is not that convenient for the case when everything is in `Type`.

* add `mk_eq_mk_of_basis'`: same-universe version of `mk_eq_mk_of_basis`;
* generalize `is_basis.mk_eq_dim''` to any index type in the same universe as `V`, not necessarily `s : set V`;
* reorder lemmas to optimize the total length of the proofs;
* drop one `finite_dimensional` assumption in `findim_of_infinite_dimensional`.

Author: urkud

src/field_theory/tower.lean

@@ -74,12 +74,18 @@ by { rw [submodule.restrict_scalars'_top, eq_top_iff, ← hb, submodule.span_le]
 
 /-- Tower law: if `A` is a `K`-algebra and `K` is a field extension of `F` then
 `dim_F(A) = dim_F(K) * dim_K(A)`. -/
-theorem findim_mul_findim [finite_dimensional F K] [finite_dimensional K A] :
+theorem findim_mul_findim [finite_dimensional F K] :
   findim F K * findim K A = findim F A :=
-let ⟨b, hb⟩ := exists_is_basis_finset F K in
-let ⟨c, hc⟩ := exists_is_basis_finset K A in
-by rw [findim_eq_card_basis hb, findim_eq_card_basis hc,
-    findim_eq_card_basis (hb.smul hc), fintype.card_prod]
+begin
+  by_cases hA : finite_dimensional K A,
+  { resetI,
+    rcases exists_is_basis_finset F K with ⟨b, hb⟩,
+    rcases exists_is_basis_finset K A with ⟨c, hc⟩,
+    rw [findim_eq_card_basis hb, findim_eq_card_basis hc,
+      findim_eq_card_basis (hb.smul hc), fintype.card_prod] },
+  { rw [findim_of_infinite_dimensional hA, mul_zero, findim_of_infinite_dimensional],
+    exact mt (@right F K A _ _ _ _ _ _ _) hA }
+end
 
 instance linear_map (F : Type u) (V : Type v) (W : Type w)
   [field F] [add_comm_group V] [vector_space F V] [add_comm_group W] [vector_space F W]

src/linear_algebra/dimension.lean

@@ -109,17 +109,24 @@ begin
       apply (cardinal.mk_range_eq_of_injective hv.injective).symm, }, }
 end
 
-theorem is_basis.mk_range_eq_dim {v : ι → V} (h : is_basis K v) :
-  cardinal.mk (range v) = dim K V :=
+theorem mk_eq_mk_of_basis' {ι' : Type w} {v : ι → V} {v' : ι' → V} (hv : is_basis K v)
+  (hv' : is_basis K v') :
+  cardinal.mk ι = cardinal.mk ι' :=
+cardinal.lift_inj.1 $ mk_eq_mk_of_basis hv hv'
+
+theorem is_basis.mk_eq_dim'' {ι : Type v} {v : ι → V} (h : is_basis K v) :
+  cardinal.mk ι = dim K V :=
 begin
-  have := show ∃ v', dim K V = _, from cardinal.min_eq _ _,
-  rcases this with ⟨v', e⟩,
+  obtain ⟨v', e : dim K V = _⟩ := cardinal.min_eq _ _,
   rw e,
-  apply cardinal.lift_inj.1,
-  rw cardinal.mk_range_eq_of_injective h.injective,
-  convert @mk_eq_mk_of_basis _ _ _ _ _ _ _ _ _ h v'.property
+  rw ← cardinal.mk_range_eq _ h.injective,
+  exact mk_eq_mk_of_basis' h.range v'.2
 end
 
+theorem is_basis.mk_range_eq_dim {v : ι → V} (h : is_basis K v) :
+  cardinal.mk (range v) = dim K V :=
+h.range.mk_eq_dim''
+
 theorem is_basis.mk_eq_dim {v : ι → V} (h : is_basis K v) :
   cardinal.lift.{w v} (cardinal.mk ι) = cardinal.lift.{v w} (dim K V) :=
 by rw [←h.mk_range_eq_dim, cardinal.mk_range_eq_of_injective h.injective]
@@ -128,10 +135,6 @@ theorem {m} is_basis.mk_eq_dim' {v : ι → V} (h : is_basis K v) :
   cardinal.lift.{w (max v m)} (cardinal.mk ι) = cardinal.lift.{v (max w m)} (dim K V) :=
 by simpa using h.mk_eq_dim
 
-theorem is_basis.mk_eq_dim'' {b : set V} (hb : is_basis K (λ x : b, (x : V))) :
-  cardinal.mk b = dim K V :=
-(dim K V).lift_id ▸ hb.mk_eq_dim ▸ (cardinal.mk b).lift_id.symm
-
 theorem dim_le {n : ℕ}
   (H : ∀ s : finset V, linear_independent K (λ i : (↑s : set V), (i : V)) → s.card ≤ n) :
   dim K V ≤ n :=

src/linear_algebra/finite_dimensional.lean

@@ -195,14 +195,17 @@ begin
   exact (classical.some_spec (lt_omega.1 (dim_lt_omega K V))).symm
 end
 
+lemma findim_of_infinite_dimensional {K V : Type*} [field K] [add_comm_group V] [vector_space K V]
+  (h : ¬finite_dimensional K V) : findim K V = 0 :=
+dif_neg $ mt finite_dimensional_iff_dim_lt_omega.2 h
+
 /-- If a vector space has a finite basis, then its dimension (seen as a cardinal) is equal to the
 cardinality of the basis. -/
 lemma dim_eq_card_basis {ι : Type w} [fintype ι] {b : ι → V} (h : is_basis K b) :
   dim K V = fintype.card ι :=
 by rw [←h.mk_range_eq_dim, cardinal.fintype_card,
        set.card_range_of_injective h.injective]
 
-
 /-- If a vector space has a finite basis, then its dimension is equal to the cardinality of the
 basis. -/
 lemma findim_eq_card_basis {ι : Type w} [fintype ι] {b : ι → V} (h : is_basis K b) :