feat(linear_algebra/dim): findim equivalence (#1217)

* feat(linear_algebra/dim): findim equivalence

* feat(linear_algebra/dim): two versions of dim_fun

* feat(linear_algebra/dim): clean up

Author: abentkamp

src/linear_algebra/dimension.lean

@@ -9,10 +9,10 @@ import linear_algebra.basis
 import set_theory.ordinal
 noncomputable theory
 
-universes u v v' w w'
+universes u u' u'' v v' w w'
 
 variables {α : Type u} {β γ δ ε : Type v}
-variables {ι : Type w} {ι' : Type w'} {η : Type u} {φ : η → Type u}
+variables {ι : Type w} {ι' : Type w'} {η : Type u''} {φ : η → Type u'}
 -- TODO: relax these universe constraints
 
 section vector_space
@@ -313,12 +313,20 @@ begin
   simp [λ i, (hb i).mk_range_eq_dim.symm, cardinal.sum_mk]
 end
 
-lemma dim_fun {β : Type u} [add_comm_group β] [vector_space α β] :
+lemma dim_fun {β η : Type u} [fintype η] [add_comm_group β] [vector_space α β] :
   vector_space.dim α (η → β) = fintype.card η * vector_space.dim α β :=
 by rw [dim_pi, cardinal.sum_const, cardinal.fintype_card]
 
+lemma dim_fun_eq_lift_mul :
+  vector_space.dim α (η → β) = (fintype.card η : cardinal.{max u'' v}) *
+    cardinal.lift.{v u''} (vector_space.dim α β) :=
+by rw [dim_pi, cardinal.sum_const_eq_lift_mul, cardinal.fintype_card, cardinal.lift_nat_cast]
+
 lemma dim_fun' : vector_space.dim α (η → α) = fintype.card η :=
-by rw [dim_fun, dim_of_field α, mul_one]
+by rw [dim_fun_eq_lift_mul, dim_of_field α, cardinal.lift_one, mul_one, cardinal.nat_cast_inj]
+
+lemma dim_fin_fun (n : ℕ) : dim α (fin n → α) = n :=
+by simp [dim_fun']
 
 end fintype
 

src/linear_algebra/finsupp_vector_space.lean

@@ -80,36 +80,63 @@ end dim
 end finsupp
 
 section vector_space
-universes u v
-variables {α : Type u} {β γ : Type v}
+/- We use `universe variables` instead of `universes` here because universes introduced by the
+   `universes` keyword do not get replaced by metavariables once a lemma has been proven. So if you
+   prove a lemma using universe `u`, you can only apply it to universe `u` in other lemmas of the
+   same section. -/
+universe variables u v w
+variables {α : Type u} {β γ : Type v} {β' : Type v} {γ' : Type w}
 variables [discrete_field α]
 variables [add_comm_group β] [vector_space α β]
 variables [add_comm_group γ] [vector_space α γ]
+variables [add_comm_group β'] [vector_space α β']
+variables [add_comm_group γ'] [vector_space α γ']
 
 open vector_space
 
 set_option class.instance_max_depth 70
 
-lemma equiv_of_dim_eq_dim [decidable_eq β] [decidable_eq γ] (h : dim α β = dim α γ) :
-  nonempty (β ≃ₗ[α] γ) :=
+lemma equiv_of_dim_eq_lift_dim
+  (h : cardinal.lift.{v w} (dim α β') = cardinal.lift.{w v} (dim α γ')) :
+  nonempty (β' ≃ₗ[α] γ') :=
 begin
-  rcases exists_is_basis α β with ⟨b, hb⟩,
-  rcases exists_is_basis α γ with ⟨c, hc⟩,
-  rw [← cardinal.lift_inj, ← hb.mk_eq_dim, ← hc.mk_eq_dim, cardinal.lift_inj] at h,
+  haveI := classical.dec_eq β',
+  haveI := classical.dec_eq γ',
+  rcases exists_is_basis α β' with ⟨b, hb⟩,
+  rcases exists_is_basis α γ' with ⟨c, hc⟩,
+  rw [←cardinal.lift_inj.1 hb.mk_eq_dim, ←cardinal.lift_inj.1 hc.mk_eq_dim] at h,
   rcases quotient.exact h with ⟨e⟩,
+  let e := (equiv.ulift.symm.trans e).trans equiv.ulift,
   exact ⟨((module_equiv_finsupp hb).trans
       (finsupp.dom_lcongr e)).trans
       (module_equiv_finsupp hc).symm⟩,
 end
 
-lemma eq_bot_iff_dim_eq_zero [decidable_eq β] (p : submodule α β) (h : dim α p = 0) : p = ⊥ :=
+def equiv_of_dim_eq_dim (h : dim α β = dim α γ) : β ≃ₗ[α] γ :=
+begin
+  classical,
+  exact classical.choice (equiv_of_dim_eq_lift_dim (cardinal.lift_inj.2 h))
+end
+
+lemma fin_dim_vectorspace_equiv (n : ℕ)
+  (hn : (dim α β) = n) : β ≃ₗ[α] (fin n → α) :=
+begin
+  have : cardinal.lift.{v u} (n : cardinal.{v}) = cardinal.lift.{u v} (n : cardinal.{u}),
+    by simp,
+  have hn := cardinal.lift_inj.{v u}.2 hn,
+  rw this at hn,
+  rw ←@dim_fin_fun α _ n at hn,
+  exact classical.choice (equiv_of_dim_eq_lift_dim hn),
+end
+
+lemma eq_bot_iff_dim_eq_zero (p : submodule α β) (h : dim α p = 0) : p = ⊥ :=
 begin
   have : dim α p = dim α (⊥ : submodule α β) := by rwa [dim_bot],
-  rcases equiv_of_dim_eq_dim this with ⟨e⟩,
+  let e := equiv_of_dim_eq_dim this,
   exact e.eq_bot_of_equiv _
 end
 
-lemma injective_of_surjective [decidable_eq β] [decidable_eq γ] (f : β →ₗ[α] γ)
+lemma injective_of_surjective (f : β →ₗ[α] γ)
   (hβ : dim α β < cardinal.omega) (heq : dim α γ = dim α β) (hf : f.range = ⊤) : f.ker = ⊥ :=
 have hk : dim α f.ker < cardinal.omega := lt_of_le_of_lt (dim_submodule_le _) hβ,
 begin

src/set_theory/cardinal.lean

@@ -505,6 +505,20 @@ calc lift.{u (max v w)} a = lift.{v (max u w)} b
     = lift.{(max u v) w} (lift.{v u} b) : by simp
   ... ↔ lift.{u v} a = lift.{v u} b : lift_inj
 
+theorem mk_prod {α : Type u} {β : Type v} :
+  mk (α × β) = lift.{u v} (mk α) * lift.{v u} (mk β) :=
+quotient.sound ⟨equiv.prod_congr (equiv.ulift).symm (equiv.ulift).symm⟩
+
+theorem sum_const_eq_lift_mul (ι : Type u) (a : cardinal.{v}) :
+  sum (λ _:ι, a) = lift.{u v} (mk ι) * lift.{v u} a :=
+begin
+  apply quotient.induction_on a,
+  intro α,
+  simp only [cardinal.mk_def, cardinal.sum_mk, cardinal.lift_id],
+  convert mk_prod using 1,
+  exact quotient.sound ⟨equiv.sigma_equiv_prod ι α⟩,
+end
+
 /-- `ω` is the smallest infinite cardinal, also known as ℵ₀. -/
 def omega : cardinal.{u} := lift (mk ℕ)