feat(linear_algebra/invariant_basis_number): basic API lemmas (#7882)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

src/algebra/module/linear_map.lean

@@ -584,6 +584,11 @@ symm_bijective.injective $ ext $ λ x, rfl
   { to_fun := f, inv_fun := e,
     ..(⟨e, h₁, h₂, f, h₃, h₄⟩ : M ≃ₗ[R] M₂).symm } := rfl
 
+@[simp] lemma coe_symm_mk [module R M] [module R M₂]
+  {to_fun inv_fun map_add map_smul left_inv right_inv} :
+  ⇑((⟨to_fun, map_add, map_smul, inv_fun, left_inv, right_inv⟩ : M ≃ₗ[R] M₂).symm) = inv_fun :=
+rfl
+
 protected lemma bijective : function.bijective e := e.to_equiv.bijective
 protected lemma injective : function.injective e := e.to_equiv.injective
 protected lemma surjective : function.surjective e := e.to_equiv.surjective

src/linear_algebra/basic.lean

@@ -82,36 +82,38 @@ begin
   { intro i, exact (h i).map_zero },
 end
 
-variable (R)
+variables (α : Type*) [fintype α]
+variables (R M) [add_comm_monoid M] [semiring R] [module R M]
 
 /-- Given `fintype α`, `linear_equiv_fun_on_fintype R` is the natural `R`-linear equivalence between
 `α →₀ β` and `α → β`. -/
-@[simps apply] noncomputable def linear_equiv_fun_on_fintype {α} [fintype α] [add_comm_monoid M]
-  [semiring R] [module R M] :
+@[simps apply] noncomputable def linear_equiv_fun_on_fintype :
   (α →₀ M) ≃ₗ[R] (α → M) :=
 { to_fun := coe_fn,
   map_add' := λ f g, by { ext, refl },
   map_smul' := λ c f, by { ext, refl },
   .. equiv_fun_on_fintype }
 
-@[simp] lemma linear_equiv_fun_on_fintype_single {α} [decidable_eq α] [fintype α]
-  [add_comm_monoid M] [semiring R] [module R M] (x : α) (m : M) :
-  (@linear_equiv_fun_on_fintype R M α _ _ _ _) (single x m) = pi.single x m :=
+@[simp] lemma linear_equiv_fun_on_fintype_single [decidable_eq α] (x : α) (m : M) :
+  (linear_equiv_fun_on_fintype R M α) (single x m) = pi.single x m :=
 begin
   ext a,
   change (equiv_fun_on_fintype (single x m)) a = _,
   convert _root_.congr_fun (equiv_fun_on_fintype_single x m) a,
 end
 
-@[simp] lemma linear_equiv_fun_on_fintype_symm_single {α} [decidable_eq α] [fintype α]
-  [add_comm_monoid M] [semiring R] [module R M] (x : α) (m : M) :
-  (@linear_equiv_fun_on_fintype R M α _ _ _ _).symm (pi.single x m) = single x m :=
+@[simp] lemma linear_equiv_fun_on_fintype_symm_single [decidable_eq α]
+  (x : α) (m : M) : (linear_equiv_fun_on_fintype R M α).symm (pi.single x m) = single x m :=
 begin
   ext a,
   change (equiv_fun_on_fintype.symm (pi.single x m)) a = _,
   convert congr_fun (equiv_fun_on_fintype_symm_single x m) a,
 end
 
+@[simp] lemma linear_equiv_fun_on_fintype_symm_coe (f : α →₀ M) :
+  (linear_equiv_fun_on_fintype R M α).symm f = f :=
+by { ext, simp [linear_equiv_fun_on_fintype], }
+
 end finsupp
 
 section

src/linear_algebra/basis.lean

@@ -644,8 +644,7 @@ calc card M = card (ι → R)    : card_congr b.equiv_fun.to_equiv
 a function `x : ι → R` to the linear combination `∑_i x i • v i`. -/
 @[simp] lemma basis.equiv_fun_symm_apply (x : ι → R) :
   b.equiv_fun.symm x = ∑ i, x i • b i :=
-by { simp [basis.equiv_fun, finsupp.total_apply, finsupp.sum_fintype],
-     refl }
+by simp [basis.equiv_fun, finsupp.total_apply, finsupp.sum_fintype]
 
 @[simp]
 lemma basis.equiv_fun_apply (u : M) : b.equiv_fun u = b.repr u := rfl
@@ -666,7 +665,7 @@ by { rw [b.equiv_fun_apply, b.repr_self_apply] }
 /-- Define a basis by mapping each vector `x : M` to its coordinates `e x : ι → R`,
 as long as `ι` is finite. -/
 def basis.of_equiv_fun (e : M ≃ₗ[R] (ι → R)) : basis ι R M :=
-basis.of_repr $ e.trans $ linear_equiv.symm $ finsupp.linear_equiv_fun_on_fintype R
+basis.of_repr $ e.trans $ linear_equiv.symm $ finsupp.linear_equiv_fun_on_fintype R R ι
 
 @[simp] lemma basis.of_equiv_fun_repr_apply (e : M ≃ₗ[R] (ι → R)) (x : M) (i : ι) :
   (basis.of_equiv_fun e).repr x i = e x i := rfl

src/linear_algebra/finite_dimensional.lean

@@ -697,7 +697,7 @@ end linear_equiv
 
 instance finite_dimensional_finsupp {ι : Type*} [fintype ι] [finite_dimensional K V] :
   finite_dimensional K (ι →₀ V) :=
-(finsupp.linear_equiv_fun_on_fintype K : (ι →₀ V) ≃ₗ[K] (ι → V)).symm.finite_dimensional
+(finsupp.linear_equiv_fun_on_fintype K V ι).symm.finite_dimensional
 
 namespace finite_dimensional
 

src/linear_algebra/finsupp.lean

@@ -928,7 +928,7 @@ lemma splitting_of_finsupp_surjective_injective (f : M →ₗ[R] (α →₀ R))
 def splitting_of_fun_on_fintype_surjective [fintype α] (f : M →ₗ[R] (α → R)) (s : surjective f) :
   (α → R) →ₗ[R] M :=
 (finsupp.lift _ _ _ (λ x : α, (s (finsupp.single x 1)).some)).comp
-  (@linear_equiv_fun_on_fintype R R α _ _ _ _).symm.to_linear_map
+  (linear_equiv_fun_on_fintype R R α).symm.to_linear_map
 
 lemma splitting_of_fun_on_fintype_surjective_splits
   [fintype α] (f : M →ₗ[R] (α → R)) (s : surjective f) :

src/linear_algebra/invariant_basis_number.lean

@@ -78,6 +78,24 @@ lemma le_of_fin_injective [strong_rank_condition R] {n m : ℕ} (f : (fin n →
   injective f → n ≤ m :=
 strong_rank_condition.le_of_fin_injective f
 
+lemma card_le_of_injective [strong_rank_condition R] {α β : Type*} [fintype α] [fintype β]
+  (f : (α → R) →ₗ[R] (β → R)) (i : injective f) : fintype.card α ≤ fintype.card β :=
+begin
+  let P := linear_map.fun_congr_left R R (fintype.equiv_fin α),
+  let Q := linear_map.fun_congr_left R R (fintype.equiv_fin β),
+  exact le_of_fin_injective R ((Q.symm.to_linear_map.comp f).comp P.to_linear_map)
+    (((linear_equiv.symm Q).injective.comp i).comp (linear_equiv.injective P)),
+end
+
+lemma card_le_of_injective' [strong_rank_condition R] {α β : Type*} [fintype α] [fintype β]
+  (f : (α →₀ R) →ₗ[R] (β →₀ R)) (i : injective f) : fintype.card α ≤ fintype.card β :=
+begin
+  let P := (finsupp.linear_equiv_fun_on_fintype R R β),
+  let Q := (finsupp.linear_equiv_fun_on_fintype R R α).symm,
+  exact card_le_of_injective R ((P.to_linear_map.comp f).comp Q.to_linear_map)
+    ((P.injective.comp i).comp Q.injective)
+end
+
 /-- We say that `R` satisfies the rank condition if `(fin n → R) →ₗ[R] (fin m → R)` surjective
     implies `m ≤ n`. -/
 class rank_condition : Prop :=
@@ -87,6 +105,24 @@ lemma le_of_fin_surjective [rank_condition R] {n m : ℕ} (f : (fin n → R) →
   surjective f → m ≤ n :=
 rank_condition.le_of_fin_surjective f
 
+lemma card_le_of_surjective [rank_condition R] {α β : Type*} [fintype α] [fintype β]
+  (f : (α → R) →ₗ[R] (β → R)) (i : surjective f) : fintype.card β ≤ fintype.card α :=
+begin
+  let P := linear_map.fun_congr_left R R (fintype.equiv_fin α),
+  let Q := linear_map.fun_congr_left R R (fintype.equiv_fin β),
+  exact le_of_fin_surjective R ((Q.symm.to_linear_map.comp f).comp P.to_linear_map)
+    (((linear_equiv.symm Q).surjective.comp i).comp (linear_equiv.surjective P)),
+end
+
+lemma card_le_of_surjective' [rank_condition R] {α β : Type*} [fintype α] [fintype β]
+  (f : (α →₀ R) →ₗ[R] (β →₀ R)) (i : surjective f) : fintype.card β ≤ fintype.card α :=
+begin
+  let P := (finsupp.linear_equiv_fun_on_fintype R R β),
+  let Q := (finsupp.linear_equiv_fun_on_fintype R R α).symm,
+  exact card_le_of_surjective R ((P.to_linear_map.comp f).comp Q.to_linear_map)
+    ((P.surjective.comp i).comp Q.surjective)
+end
+
 /--
 By the universal property for free modules, any surjective map `(fin n → R) →ₗ[R] (fin m → R)`
 has an injective splitting `(fin m → R) →ₗ[R] (fin n → R)`
@@ -117,6 +153,11 @@ variables (R : Type u) [ring R] [invariant_basis_number R]
 lemma eq_of_fin_equiv {n m : ℕ} : ((fin n → R) ≃ₗ[R] (fin m → R)) → n = m :=
 invariant_basis_number.eq_of_fin_equiv
 
+lemma card_eq_of_lequiv {α β : Type*} [fintype α] [fintype β]
+  (f : (α → R) ≃ₗ[R] (β → R)) : fintype.card α = fintype.card β :=
+eq_of_fin_equiv R (((linear_map.fun_congr_left R R (fintype.equiv_fin α)).trans f).trans
+  ((linear_map.fun_congr_left R R (fintype.equiv_fin β)).symm))
+
 lemma nontrivial_of_invariant_basis_number : nontrivial R :=
 begin
   by_contra h,