[Merged by Bors] - feat(linear_algebra/invariant_basis_number): strong_rank_condition_iff_succ

src/algebra/group/pi.lean

@@ -257,3 +257,16 @@ lemma pi.piecewise_div [Π i, has_div (f i)] (s : set I) [Π i, decidable (i ∈
 s.piecewise_op₂ _ _ _ _ (λ _, (/))
 
 end piecewise
+
+section extend
+
+variables {ι : Type u} {η : Type v} (R : Type w) (s : ι → η)
+
+/-- `function.extend s f 1` as a bundled hom. -/
+@[to_additive function.extend_by_zero.hom "`function.extend s f 0` as a bundled hom.", simps]
+noncomputable def function.extend_by_one.hom [mul_one_class R] : (ι → R) →* (η → R) :=
+{ to_fun := λ f, function.extend s f 1,
+  map_one' := function.extend_one s,
+  map_mul' := λ f g, by { simpa using function.extend_mul s f g 1 1 } }
+
+end extend

src/algebra/module/pi.lean

@@ -201,3 +201,12 @@ instance (α) {r : semiring α} {m : Π i, add_comm_monoid $ f i}
   (λ i, (smul_eq_zero.mp (congr_fun h i)).resolve_left hc))⟩
 
 end pi
+
+section extend
+
+@[to_additive]
+lemma function.extend_smul {R α β γ} [has_scalar R γ] (r : R) (f : α → β) (g : α → γ) (e : β → γ) :
+  function.extend f (r • g) (r • e) = r • function.extend f g e :=
+funext $ λ _, by convert (apply_dite ((•) r) _ _ _).symm
+
+end extend

src/data/pi.lean

@@ -114,6 +114,35 @@ function.update_injective _ i
 end
 end pi
 
+section extend
+
+namespace function
+
+variables {α β γ : Type*}
+
+@[to_additive]
+lemma extend_one [has_one γ] (f : α → β) :
+  function.extend f (1 : α → γ) (1 : β → γ) = 1 :=
+funext $ λ _, by apply if_t_t _ _
+
+@[to_additive]
+lemma extend_mul [has_mul γ] (f : α → β) (g₁ g₂ : α → γ) (e₁ e₂ : β → γ) :
+  function.extend f (g₁ * g₂) (e₁ * e₂) = function.extend f g₁ e₁ * function.extend f g₂ e₂ :=
+funext $ λ _, by convert (apply_dite2 (*) _ _ _ _ _).symm
+
+@[to_additive]
+lemma extend_inv [has_inv γ] (f : α → β) (g : α → γ) (e : β → γ) :
+  function.extend f (g⁻¹) (e⁻¹) = (function.extend f g e)⁻¹ :=
+funext $ λ _, by convert (apply_dite has_inv.inv _ _ _).symm
+
+@[to_additive]
+lemma extend_div [has_div γ] (f : α → β) (g₁ g₂ : α → γ) (e₁ e₂ : β → γ) :
+  function.extend f (g₁ / g₂) (e₁ / e₂) = function.extend f g₁ e₁ / function.extend f g₂ e₂ :=
+funext $ λ _, by convert (apply_dite2 (/) _ _ _ _ _).symm
+
+end function
+end extend
+
 lemma subsingleton.pi_single_eq {α : Type*} [decidable_eq I] [subsingleton I] [has_zero α]
   (i : I) (x : α) :
   pi.single i x = λ _, x :=

src/linear_algebra/invariant_basis_number.lean

@@ -71,13 +71,27 @@ variables (R : Type u) [ring R]
 
 /-- We say that `R` satisfies the strong rank condition if `(fin n → R) →ₗ[R] (fin m → R)` injective
     implies `n ≤ m`. -/
+@[mk_iff]
 class strong_rank_condition : Prop :=
 (le_of_fin_injective : ∀ {n m : ℕ} (f : (fin n → R) →ₗ[R] (fin m → R)), injective f → n ≤ m)
 
 lemma le_of_fin_injective [strong_rank_condition R] {n m : ℕ} (f : (fin n → R) →ₗ[R] (fin m → R)) :
   injective f → n ≤ m :=
 strong_rank_condition.le_of_fin_injective f
 
+/-- A ring satisfies the strong rank condition if and only if, for all `n : ℕ`, any linear map
+`(fin (n + 1) → R) →ₗ[R] (fin n → R)` is not injective. -/
+lemma strong_rank_condition_iff_succ : strong_rank_condition R ↔
+  ∀ (n : ℕ) (f : (fin (n + 1) → R) →ₗ[R] (fin n → R)), ¬function.injective f :=
+begin
+  refine ⟨λ h n, λ f hf, _, λ h, ⟨λ n m f hf, _⟩⟩,
+  { letI : strong_rank_condition R := h,
+    exact nat.not_succ_le_self n (le_of_fin_injective R f hf) },
+  { by_contra H,
+    exact h m (f.comp (function.extend_by_zero.linear_map R (fin.cast_le (not_le.1 H))))
+      (hf.comp (function.extend_injective (rel_embedding.injective _) 0)) }
+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

src/linear_algebra/pi.lean

@@ -331,3 +331,16 @@ def sum_arrow_lequiv_prod_arrow (α β R M : Type*) [semiring R] [add_comm_monoi
   ((sum_arrow_lequiv_prod_arrow α β R M).symm (f, g)) (sum.inr b) = g b := rfl
 
 end linear_equiv
+
+section extend
+
+variables (R) {η : Type x} [semiring R] (s : ι → η)
+
+/-- `function.extend s f 0` as a bundled linear map. -/
+@[simps]
+noncomputable def function.extend_by_zero.linear_map : (ι → R) →ₗ[R] (η → R) :=
+{ to_fun := λ f, function.extend s f 0,
+  map_smul' := λ r f, by { simpa using function.extend_smul r s f 0 },
+  ..function.extend_by_zero.hom R s }
+
+end extend

src/logic/function/basic.lean

@@ -485,6 +485,20 @@ begin
   exact congr_arg g (hf $ classical.some_spec (exists_apply_eq_apply f a))
 end
 
+@[simp] lemma extend_apply' (g : α → γ) (e' : β → γ) (b : β) (hb : ¬∃ a, f a = b) :
+  extend f g e' b = e' b :=
+by simp [function.extend_def, hb]
+
+lemma extend_injective (hf : injective f) (e' : β → γ) :
+  injective (λ g, extend f g e') :=
+begin
+  intros g₁ g₂ hg,
+  refine funext (λ x, _),
+  have H := congr_fun hg (f x),
+  simp only [hf, extend_apply] at H,
+  exact H
+end
+
 @[simp] lemma extend_comp (hf : injective f) (g : α → γ) (e' : β → γ) :
   extend f g e' ∘ f = g :=
 funext $ λ a, extend_apply hf g e' a