feat(linear_algebra): dimension theorem (#345)

* dimension theorem

* more theorems about dimension

* cardinal stuff

* fix error

* move A/S x S = A to quotient_module.lean

* remove pempty_equiv_empty

data/equiv/basic.lean

@@ -177,11 +177,20 @@ def equiv_pempty (h : α → false) : α ≃ pempty :=
 def false_equiv_pempty : false ≃ pempty :=
 equiv_pempty _root_.id
 
+def empty_equiv_pempty : empty ≃ pempty :=
+equiv_pempty $ empty.rec _
+
 def pempty_equiv_pempty : pempty.{v} ≃ pempty.{w} :=
-equiv_pempty (pempty.elim)
+equiv_pempty pempty.elim
 
 def empty_of_not_nonempty {α : Sort*} (h : ¬ nonempty α) : α ≃ empty :=
-⟨assume a, (h ⟨a⟩).elim, assume e, e.rec_on _, assume a, (h ⟨a⟩).elim, assume e, e.rec_on _⟩
+equiv_empty $ assume a, h ⟨a⟩
+
+def pempty_of_not_nonempty {α : Sort*} (h : ¬ nonempty α) : α ≃ pempty :=
+equiv_pempty $ assume a, h ⟨a⟩
+
+def true_equiv_punit : true ≃ punit :=
+⟨λ x, (), λ x, trivial, λ ⟨⟩, rfl, λ ⟨⟩, rfl⟩
 
 protected def ulift {α : Type u} : ulift α ≃ α :=
 ⟨ulift.down, ulift.up, ulift.up_down, λ a, rfl⟩
@@ -200,21 +209,21 @@ def punit_equiv_punit : punit.{v} ≃ punit.{w} :=
 ⟨λ _, punit.star, λ _, punit.star, λ u, by cases u; refl, λ u, by cases u; reflexivity⟩
 
 section
-@[simp] def arrow_unit_equiv_unit (α : Sort*) : (α → punit.{v}) ≃ punit.{w} :=
+@[simp] def arrow_punit_equiv_punit (α : Sort*) : (α → punit.{v}) ≃ punit.{w} :=
 ⟨λ f, punit.star, λ u f, punit.star, λ f, by funext x; cases f x; refl, λ u, by cases u; reflexivity⟩
 
-@[simp] def unit_arrow_equiv (α : Sort*) : (punit.{u} → α) ≃ α :=
+@[simp] def punit_arrow_equiv (α : Sort*) : (punit.{u} → α) ≃ α :=
 ⟨λ f, f punit.star, λ a u, a, λ f, by funext x; cases x; refl, λ u, rfl⟩
 
-@[simp] def empty_arrow_equiv_unit (α : Sort*) : (empty → α) ≃ punit.{u} :=
+@[simp] def empty_arrow_equiv_punit (α : Sort*) : (empty → α) ≃ punit.{u} :=
 ⟨λ f, punit.star, λ u e, e.rec _, λ f, funext $ λ x, x.rec _, λ u, by cases u; refl⟩
 
-@[simp] def pempty_arrow_equiv_unit (α : Sort*) : (pempty → α) ≃ punit.{u} :=
+@[simp] def pempty_arrow_equiv_punit (α : Sort*) : (pempty → α) ≃ punit.{u} :=
 ⟨λ f, punit.star, λ u e, e.rec _, λ f, funext $ λ x, x.rec _, λ u, by cases u; refl⟩
 
-@[simp] def false_arrow_equiv_unit (α : Sort*) : (false → α) ≃ punit.{u} :=
+@[simp] def false_arrow_equiv_punit (α : Sort*) : (false → α) ≃ punit.{u} :=
 calc (false → α) ≃ (empty → α) : arrow_congr false_equiv_empty (equiv.refl _)
-             ... ≃ punit       : empty_arrow_equiv_unit _
+             ... ≃ punit       : empty_arrow_equiv_punit _
 
 end
 
@@ -238,16 +247,16 @@ by cases e₁; cases e₂; refl
   prod_assoc α β γ p = ⟨p.1.1, ⟨p.1.2, p.2⟩⟩ := rfl
 
 section
-@[simp] def prod_unit (α : Sort*) : (α × punit.{u+1}) ≃ α :=
+@[simp] def prod_punit (α : Sort*) : (α × punit.{u+1}) ≃ α :=
 ⟨λ p, p.1, λ a, (a, punit.star), λ ⟨_, punit.star⟩, rfl, λ a, rfl⟩
 
-@[simp] theorem prod_unit_apply {α : Sort*} (a : α × punit.{u+1}) : prod_unit α a = a.1 := rfl
+@[simp] theorem prod_punit_apply {α : Sort*} (a : α × punit.{u+1}) : prod_punit α a = a.1 := rfl
 
-@[simp] def unit_prod (α : Sort*) : (punit.{u+1} × α) ≃ α :=
+@[simp] def punit_prod (α : Sort*) : (punit.{u+1} × α) ≃ α :=
 calc (punit × α) ≃ (α × punit) : prod_comm _ _
-  ... ≃ α          : prod_unit _
+  ... ≃ α          : prod_punit _
 
-@[simp] theorem unit_prod_apply {α : Sort*} (a : punit.{u+1} × α) : unit_prod α a = a.2 := rfl
+@[simp] theorem punit_prod_apply {α : Sort*} (a : punit.{u+1} × α) : punit_prod α a = a.2 := rfl
 
 @[simp] def prod_empty (α : Sort*) : (α × empty) ≃ empty :=
 equiv_empty (λ ⟨_, e⟩, e.rec _)
@@ -285,7 +294,7 @@ by cases e₁; cases e₂; refl
   sum_congr e₁ e₂ (inr b) = inr (e₂ b) :=
 by cases e₁; cases e₂; refl
 
-def bool_equiv_unit_sum_unit : bool ≃ (punit.{u+1} ⊕ punit.{v+1}) :=
+def bool_equiv_punit_sum_punit : bool ≃ (punit.{u+1} ⊕ punit.{v+1}) :=
 ⟨λ b, cond b (inr punit.star) (inl punit.star),
  λ s, sum.rec_on s (λ_, ff) (λ_, tt),
  λ b, by cases b; refl,
@@ -329,7 +338,7 @@ noncomputable def Prop_equiv_bool : Prop ≃ bool :=
 @[simp] def pempty_sum (α : Sort*) : (pempty ⊕ α) ≃ α :=
 (sum_comm _ _).trans $ sum_pempty _
 
-@[simp] def option_equiv_sum_unit (α : Sort*) : option α ≃ (α ⊕ punit.{u+1}) :=
+@[simp] def option_equiv_sum_punit (α : Sort*) : option α ≃ (α ⊕ punit.{u+1}) :=
 ⟨λ o, match o with none := inr punit.star | some a := inl a end,
  λ s, match s with inr _ := none | inl a := some a end,
  λ o, by cases o; refl,
@@ -423,22 +432,22 @@ calc (α × (β ⊕ γ)) ≃ ((β ⊕ γ) × α)       : prod_comm _ _
    prod_sum_distrib α β γ (a, sum.inr c) = sum.inr (a, c) := rfl
 
 def bool_prod_equiv_sum (α : Type u) : (bool × α) ≃ (α ⊕ α) :=
-calc (bool × α) ≃ ((unit ⊕ unit) × α)       : prod_congr bool_equiv_unit_sum_unit (equiv.refl _)
+calc (bool × α) ≃ ((unit ⊕ unit) × α)       : prod_congr bool_equiv_punit_sum_punit (equiv.refl _)
         ...     ≃ (α × (unit ⊕ unit))       : prod_comm _ _
         ...     ≃ ((α × unit) ⊕ (α × unit)) : prod_sum_distrib _ _ _
-        ...     ≃ (α ⊕ α)                   : sum_congr (prod_unit _) (prod_unit _)
+        ...     ≃ (α ⊕ α)                   : sum_congr (prod_punit _) (prod_punit _)
 end
 
 section
 open sum nat
-def nat_equiv_nat_sum_unit : ℕ ≃ (ℕ ⊕ punit.{u+1}) :=
+def nat_equiv_nat_sum_punit : ℕ ≃ (ℕ ⊕ punit.{u+1}) :=
 ⟨λ n, match n with zero := inr punit.star | succ a := inl a end,
  λ s, match s with inl n := succ n | inr punit.star := zero end,
  λ n, begin cases n, repeat { refl } end,
  λ s, begin cases s with a u, { refl }, {cases u, { refl }} end⟩
 
-@[simp] def nat_sum_unit_equiv_nat : (ℕ ⊕ punit.{u+1}) ≃ ℕ :=
-nat_equiv_nat_sum_unit.symm
+@[simp] def nat_sum_punit_equiv_nat : (ℕ ⊕ punit.{u+1}) ≃ ℕ :=
+nat_equiv_nat_sum_punit.symm
 
 def int_equiv_nat_sum_nat : ℤ ≃ (ℕ ⊕ ℕ) :=
 by refine ⟨_, _, _, _⟩; intro z; {cases z; [left, right]; assumption} <|> {cases z; refl}
@@ -475,6 +484,10 @@ def subtype_subtype_equiv_subtype {α : Type u} (p : α → Prop) (q : subtype p
   λ⟨a, ha⟩, ⟨⟨a, ha.cases_on $ assume h _, h⟩, by cases ha; exact ha_h⟩,
   assume ⟨⟨a, ha⟩, h⟩, rfl, assume ⟨a, h₁, h₂⟩, rfl⟩
 
+/-- aka coimage -/
+def equiv_sigma_subtype {α : Type u} {β : Type v} (f : α → β) : α ≃ Σ b, {x : α // f x = b} :=
+⟨λ x, ⟨f x, x, rfl⟩, λ x, x.2.1, λ x, rfl, λ ⟨b, x, H⟩, sigma.eq H $ eq.drec_on H $ subtype.eq rfl⟩
+
 end
 
 section

data/equiv/encodable.lean

@@ -127,7 +127,7 @@ instance sum : encodable (α ⊕ β) :=
 end sum
 
 instance bool : encodable bool :=
-of_equiv (unit ⊕ unit) equiv.bool_equiv_unit_sum_unit
+of_equiv (unit ⊕ unit) equiv.bool_equiv_punit_sum_punit
 
 @[simp] theorem encode_tt : encode tt = 1 := rfl
 @[simp] theorem encode_ff : encode ff = 0 := rfl

data/fintype.lean

@@ -181,6 +181,12 @@ instance : fintype unit := ⟨⟨()::0, by simp⟩, λ ⟨⟩, by simp⟩
 
 @[simp] theorem fintype.card_unit : fintype.card unit = 1 := rfl
 
+instance : fintype punit := ⟨⟨punit.star::0, by simp⟩, λ ⟨⟩, by simp⟩
+
+@[simp] theorem fintype.univ_punit : @univ punit _ = {punit.star} := rfl
+
+@[simp] theorem fintype.card_punit : fintype.card punit = 1 := rfl
+
 instance : fintype bool := ⟨⟨tt::ff::0, by simp⟩, λ x, by cases x; simp⟩
 
 @[simp] theorem fintype.univ_bool : @univ bool _ = {ff, tt} := rfl

linear_algebra/basic.lean

@@ -440,6 +440,7 @@ section is_basis
 lemma is_basis.map_repr (hs : is_basis s) : is_linear_map hs.1.repr :=
 ⟨assume b₁ b₂, repr_add hs.1 (hs.2 _) (hs.2 _), assume a b, repr_smul hs.1 (hs.2 _)⟩
 
+/-- Construct a linear map given the value at the basis. -/
 def is_basis.constr (hs : is_basis s) (f : β → γ) (b : β) : γ := (hs.1.repr b).sum (λb a, a • f b)
 
 lemma is_basis.map_constr (hs : is_basis s) {f : β → γ} : is_linear_map (hs.constr f) :=
@@ -594,6 +595,12 @@ iff.intro
   (assume h, h.of_image hf $ assume x hx y hy, hf_inj x (subset_span hx) y (subset_span hy))
   (assume h, h.image hf hf_inj)
 
+lemma is_basis.linear_equiv {s : set β} (hs : is_basis s)
+  {f : β ≃ₗ γ} : is_basis ((f.to_equiv : β → γ) '' s) :=
+⟨hs.1.image f.linear_fun $ λ b1 _ b2 _ H, f.to_equiv.bijective.1 H,
+λ x, by rw span_image_of_linear_map (show is_linear_map f.to_equiv, from f.linear_fun);
+  from ⟨f.to_equiv.symm x, hs.2 _, by rw equiv.apply_inverse_apply⟩⟩
+
 end module
 
 section vector_space

linear_algebra/dimension.lean

@@ -5,13 +5,17 @@ Author: Mario Carneiro
 
 Dimension of modules and vector spaces.
 -/
-import linear_algebra.basic set_theory.cardinal
+import linear_algebra.basic
+import linear_algebra.linear_map_module
+import linear_algebra.prod_module
+import linear_algebra.quotient_module
+import set_theory.ordinal
 noncomputable theory
 
 local attribute [instance] classical.prop_decidable
 
 universes u v w
-variables {α : Type u} {β : Type v} {γ : Type w}
+variables {α : Type u} {β γ : Type v}
 
 namespace vector_space
 variables [field α] [vector_space α β]
@@ -23,12 +27,89 @@ 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.sum (λ j, cardinal.mk (h5 j)) : cardinal.mk_Union_le_sum_mk
+  ... ≤ cardinal.sum (λ j : J, cardinal.omega.{v}) : cardinal.sum_le_sum _ _ $ λ j,
+    le_of_lt $ cardinal.lt_omega_iff_finite.2 $ finset.finite_to_set _
+  ... = cardinal.mk J * cardinal.omega : cardinal.sum_const _ _
+  ... = 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
+by rwa [← cardinal.nat_cast_le, cardinal.finset_card, cardinal.finset_card, finset.coe_to_finset, finset.coe_to_finset] at h6)
+
+/-- dimension theorem -/
+theorem mk_eq_mk_of_basis {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 mk_eq_mk_of_basis h _,
+  generalize : classical.some _ = b1,
+  exact b1.2,
 end
--/
+
+variables [vector_space α γ]
+
+theorem dim_eq_of_linear_equiv (f : β ≃ₗ γ) : dim α β = dim α γ :=
+let ⟨b, hb⟩ := exists_is_basis β in
+(mk_basis hb).symm.trans $ (cardinal.mk_eq_of_injective f.to_equiv.bijective.1).symm.trans $
+mk_basis $ hb.linear_equiv
+
+theorem dim_prod : dim α (β × γ) = dim α β + dim α γ :=
+let ⟨b, hb⟩ := exists_is_basis β in
+let ⟨c, hc⟩ := exists_is_basis γ in
+have H1 : _ := prod.is_basis_inl_union_inr hb hc,
+have H2 : _ := @mk_basis.{u v} _ (β × γ) _ _ _ H1,
+begin
+  rw [← mk_basis hb, ← mk_basis hc, ← H2, cardinal.mk_union_of_disjiont],
+  rw [cardinal.mk_eq_of_injective prod.injective_inl.{v v}], 
+  rw [cardinal.mk_eq_of_injective prod.injective_inr.{v v}],
+  intros z h,
+  rcases h with ⟨⟨x, h1, h2⟩, ⟨y, h3, h4⟩⟩,
+  subst h4,
+  cases prod.inl_eq_inr.1 h2 with h4 h5,
+  substs h4 h5,
+  exact zero_not_mem_of_linear_independent (@zero_ne_one α _) hb.1 h1
+end
+
+theorem dim_quotient {s : set β} [is_submodule s] : dim α (quotient_module.quotient β s) + dim α s = dim α β :=
+nonempty.rec_on (quotient_module.quotient_prod_linear_equiv s) $ λ f,
+dim_prod.symm.trans $ dim_eq_of_linear_equiv f
+
+/-- rank-nullity theorem -/
+theorem dim_im_add_dim_ker (f : linear_map β γ) : dim α f.im + dim α f.ker = dim α β :=
+by rw [← dim_eq_of_linear_equiv (linear_map.quot_ker_equiv_im f), dim_quotient]
 
 end vector_space

linear_algebra/quotient_module.lean

@@ -7,6 +7,8 @@ Quotient construction on modules
 -/
 
 import linear_algebra.basic
+import linear_algebra.prod_module
+import linear_algebra.subtype_module
 
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w}
@@ -130,4 +132,39 @@ assume a b, quotient.induction_on₂' a b $ assume a b (h : f a = f b), quotient
 lemma quotient.exists_rep {s : set β} [is_submodule s] : ∀ q : quotient β s, ∃ b : β, mk b = q :=
 @_root_.quotient.exists_rep _ (quotient_rel s)
 
+section vector_space
+variables {α' : Type u} {β' : Type v}
+variables [field α'] [vector_space α' β'] (s' : set β') [is_submodule s']
+omit α
+include α'
+
+instance quotient.vector_space : vector_space α' (quotient β' s') := {}
+
+theorem quotient_prod_linear_equiv :
+  nonempty ((quotient_module.quotient β' s' × s') ≃ₗ β') :=
+let ⟨g, H1, H2⟩ := exists_right_inverse_linear_map_of_surjective
+  (quotient_module.is_linear_map_quotient_mk s')
+  (quotient_module.quotient.exists_rep) in
+have H3 : ∀ b, quotient_module.mk (g b) = b := λ b, congr_fun H2 b,
+⟨{ to_fun := λ b, g b.1 + b.2.1,
+  inv_fun := λ b, (quotient_module.mk b, ⟨b - g (quotient_module.mk b),
+    (quotient_module.coe_eq_zero _ _).1 $
+    ((quotient_module.is_linear_map_quotient_mk _).sub _ _).trans $
+    by rw [H3, sub_self]⟩),
+  left_inv := λ ⟨q, b, h⟩,
+    have H4 : quotient_module.mk b = 0,
+      from (quotient_module.coe_eq_zero s' b).2 h,
+    have H5 : quotient_module.mk (g q + b) = q,
+      from ((quotient_module.is_linear_map_quotient_mk _).add _ _).trans $
+      by simp only [H3, H4, add_zero],
+    prod.ext H5 (subtype.eq $ by simp only [H5, add_sub_cancel']),
+  right_inv := λ b, add_sub_cancel'_right _ _,
+  linear_fun := ⟨λ ⟨q1, b1, h1⟩ ⟨q2, b2, h2⟩,
+      show g (q1 + q2) + (b1 + b2) = (g q1 + b1) + (g q2 + b2),
+      by rw [H1.add]; simp only [add_left_comm, add_assoc],
+    λ c ⟨q, b, h⟩, show g (c • q) + (c • b) = c • (g q + b),
+      by rw [H1.smul, smul_add]⟩ }⟩
+
+end vector_space
+
 end quotient_module