dimension theorem

Author: kckennylau

linear_algebra/dimension.lean

@@ -5,7 +5,7 @@ Author: Mario Carneiro
 
 Dimension of modules and vector spaces.
 -/
-import linear_algebra.basic set_theory.cardinal
+import linear_algebra.basic set_theory.ordinal
 noncomputable theory
 
 local attribute [instance] classical.prop_decidable
@@ -23,12 +23,53 @@ cardinal.min
   (λ b, cardinal.mk b.1)
 variables {α β}
 
-/-
+include α
+theorem basis_le_span (I J : set β) (h1 : is_basis I) (h2 : ∀x, x ∈ span J) : cardinal.mk I ≤ cardinal.mk J :=
+or.cases_on (le_or_lt cardinal.omega $ cardinal.mk J)
+(assume h4 : cardinal.omega ≤ cardinal.mk J,
+le_of_not_lt $ assume h3 : cardinal.mk I > cardinal.mk J,
+let h5 : J → set β := λ j, (h1.1.repr j).support.to_set in
+have h6 : ¬I ⊆ ⋃ j, h5 j,
+  from λ H, @not_lt_of_le _ _ (cardinal.mk I) (cardinal.mk (⋃ j, h5 j))
+    (⟨set.embedding_of_subset H⟩) $
+  calc  cardinal.mk (⋃ j, h5 j)
+      ≤ cardinal.mk J * cardinal.omega : cardinal.mk_union_le_mk_mul_omega $ λ j, finset.finite_to_set _
+  ... = max (cardinal.mk J) (cardinal.omega) : cardinal.mul_eq_max h4 (le_refl _)
+  ... = cardinal.mk J : max_eq_left h4
+  ... < cardinal.mk I : h3,
+let ⟨i₀, h7⟩ := not_forall.1 h6 in
+let ⟨h7, h8⟩ := not_imp.1 h7 in
+have h9 : _ := λ j : J, not_exists.1 (mt set.mem_Union.2 h8) j,
+have h9 : _ := λ j : J, by_contradiction $ mt (finsupp.mem_support_iff (h1.1.repr j) i₀).2 $ h9 j,
+let ⟨h10, h11, h12⟩ := h2 i₀ in
+have h13 : _ := (repr_eq_single h1.1 h7).symm.trans $
+  (congr_arg h1.1.repr h12).trans $
+  repr_finsupp_sum _ $ λ j _, h1.2 _,
+have h14 : ((finsupp.single i₀ (1:α) : lc α β) : β → α) i₀ = _,
+  from congr_fun (congr_arg finsupp.to_fun h13) i₀,
+begin
+  rw [finsupp.sum_apply, finsupp.single_eq_same, finsupp.sum] at h14,
+  rw [← finset.sum_subset (finset.empty_subset _), finset.sum_empty] at h14,
+  { exact zero_ne_one h14.symm },
+  intros v h15 h16,
+  have h17 := by_contradiction (mt (h11 v) ((finsupp.mem_support_iff _ _).1 h15)),
+  have h18 : (linear_independent.repr (h1.left) v) i₀ = 0 := h9 ⟨v, h17⟩,
+  rw [repr_smul h1.1 (h1.2 _), finsupp.smul_apply, h18, smul_eq_mul, mul_zero]
+end)
+(assume h4 : cardinal.mk J < cardinal.omega,
+let ⟨h5, h6⟩ := exists_finite_card_le_of_finite_of_linear_independent_of_span
+  (cardinal.lt_omega_iff_finite.1 h4) h1.1 (λ _ _, h2 _) in
+cardinal.mk_le_mk_of_finset_card_to_finset_le h6)
+
+theorem dimension_theorem {I J : set β} (h1 : is_basis I) (h2 : is_basis J) : cardinal.mk I = cardinal.mk J :=
+le_antisymm (basis_le_span _ _ h1 h2.2) (basis_le_span _ _ h2 h1.2)
+
 theorem mk_basis {b : set β} (h : is_basis b) : cardinal.mk b = dim α β :=
 begin
   cases (show ∃ b', dim α β = _, from cardinal.min_eq _ _) with b' e,
-  refine quotient.sound
+  refine dimension_theorem h _,
+  generalize : classical.some _ = b1,
+  exact b1.2,
 end
--/
 
 end vector_space

set_theory/cardinal.lean

@@ -651,4 +651,67 @@ lt_of_not_ge $ λ ⟨F⟩, begin
   hc i a (congr_fun h _),
 end
 
+theorem mk_le_mk_finset (α : Type u) : mk α ≤ mk (finset α) :=
+⟨⟨finset.singleton, λ _ _, finset.singleton_inj.1⟩⟩
+
+theorem mk_finset_le_mk_list (α : Type u) : mk (finset α) ≤ mk (list α) :=
+⟨⟨quotient.out ∘ finset.val, λ x y H, finset.val_inj.1 $
+calc x.1 = _ : (quotient.out_eq x.1).symm ... = _ : congr_arg _ H
+... = _ : quotient.out_eq y.1⟩⟩
+
+def vector_equiv_fin_fn (α : Type u) (n : ℕ) : vector α n ≃ (ulift.{u 0} (fin n) → α) :=
+{ to_fun := λ L i, vector.nth L i.down,
+  inv_fun := λ f, vector.of_fn (λ i, f (ulift.up i)),
+  left_inv := vector.of_fn_nth,
+  right_inv := λ f, funext (λ ⟨i⟩, vector.nth_of_fn _ i) }
+
+theorem vector_equiv_fin_fn_length (α : Type u) (n : ℕ) (f : ulift (fin n) → α) :
+  ((vector_equiv_fin_fn α n).symm f).1.length = n :=
+((vector_equiv_fin_fn α n).symm f).2
+
+theorem mk_list_eq_sum_pow (α : Type u) : mk (list α) = sum (λ n : ℕ, (mk α)^(n:cardinal.{u})) :=
+by conv {to_rhs, congr, funext, rw [← lift_mk_fin, lift_mk, power_def]};
+rw [sum_mk]; from
+(quotient.sound $ nonempty.intro $
+{ to_fun := λ L, ⟨L.length, vector_equiv_fin_fn α L.length ⟨L, rfl⟩⟩,
+  inv_fun := λ x, ((vector_equiv_fin_fn α x.1).symm x.2).to_list,
+  left_inv := λ L, by dsimp only; simp only [equiv.inverse_apply_apply]; refl,
+  right_inv := λ x, sigma.eq (vector_equiv_fin_fn_length _ _ _)
+    (begin dsimp only, generalize : rfl = H1,
+      generalize : vector_equiv_fin_fn_length α (x.fst) (x.snd) = H,
+      let N1 := ((vector_equiv_fin_fn α x.1).symm x.2).1.length,
+      change N1 = _ at H1,
+      generalize_hyp : ((vector_equiv_fin_fn α x.1).symm x.2).1.length = N3 at H H1 ⊢,
+      subst H,
+      simp only [vector.mk_to_list, equiv.apply_inverse_apply], end) })
+
+theorem mk_union_le_mk_mul_omega {α : Type u} {S : set α} {f : S → set α}
+  (hf : ∀ s, set.finite (f s)) : mk (⋃ s, f s) ≤ mk S * omega :=
+⟨⟨λ x, (classical.some (set.mem_Union.1 x.2),
+  (classical.choice (le_of_lt $ lt_omega_iff_finite.2 $ (hf $ classical.some (set.mem_Union.1 x.2)))).1
+    ⟨x.1, classical.some_spec (set.mem_Union.1 x.2)⟩),
+λ x y H, subtype.eq $ begin
+  cases prod.ext_iff.1 H with H1 H2, clear H,
+  dsimp only at H1 H2,
+  generalize_hyp : set.mem_Union.1 x.2 = H3 at H1 H2,
+  generalize_hyp : hf (classical.some H3) = H5 at H2,
+  generalize_hyp : classical.some_spec H3 = H7 at H2,
+  generalize_hyp : classical.some H3 = i at H1 H2 H5 H7,
+  subst H1,
+  exact subtype.mk.inj (function.embedding.inj _ H2)
+end⟩⟩
+
+theorem mk_le_mk_of_finset_card_to_finset_le {α : Type u} {S T : set α}
+  {HS : set.finite S} {HT : set.finite T}
+  (H : finset.card (set.finite.to_finset HS) ≤ finset.card (set.finite.to_finset HT)) :
+  mk S ≤ mk T :=
+begin
+  tactic.unfreeze_local_instances,
+  cases HS, cases HT,
+  rw [fintype_card, fintype_card, nat_cast_le],
+  rw [← fintype.card_coe, ← fintype.card_coe] at H,
+  convert H;
+  { ext z, rw [finset.mem_coe, set.finite.mem_to_finset] }
+end
+
 end cardinal

set_theory/ordinal.lean

@@ -2884,4 +2884,28 @@ lt_of_le_of_lt (add_le_add (le_max_left a b) (le_max_right a b)) $
   (λ h, lt_of_lt_of_le (add_lt_omega h h) hc)
   (λ h, by rw add_eq_self h; exact max_lt h1 h2)
 
+theorem pow_le {κ : cardinal.{u}} (H1 : omega ≤ κ) {n : ℕ} : κ^(n:cardinal.{u}) ≤ κ :=
+quotient.induction_on κ (λ α H1, nat.rec_on n
+  (le_of_lt $ lt_of_lt_of_le (by rw [nat.cast_zero, power_zero];
+    from one_lt_omega) H1)
+  (λ n ih, trans_rel_left _
+    (by rw [nat.cast_succ, power_add, power_one];
+      from mul_le_mul_right _ ih)
+    (mul_eq_self H1))) H1
+
+theorem mk_list_le_mk_aux {α : Type u} : sum (λ (n : ℕ), mk α) = sum (λ (n : ulift.{u} ℕ), mk α) :=
+by rw [sum_mk, sum_mk]; from
+(quotient.sound $ nonempty.intro $
+⟨λ x, ⟨ulift.up x.1, x.2⟩, λ x, ⟨ulift.down x.1, x.2⟩,
+λ ⟨x1, x2⟩, rfl, λ ⟨⟨x1⟩, x2⟩, rfl⟩)
+
+theorem mk_list_le_mk {α : Type u} (H1 : omega ≤ mk α) : mk (list α) ≤ mk α :=
+calc  mk (list α)
+    = sum (λ n : ℕ, mk α ^ (n : cardinal.{u})) : mk_list_eq_sum_pow α
+... ≤ sum (λ n : ℕ, mk α) : sum_le_sum _ _ $ λ n, pow_le H1
+... = sum (λ n : ulift.{u} ℕ, mk α) : mk_list_le_mk_aux
+... = omega * mk α : sum_const _ _
+... = max (omega) (mk α) : mul_eq_max (le_refl _) H1
+... = mk α : max_eq_right H1
+
 end cardinal