chore(LinearAlgebra): golfs around linearIndependent_single (#24209)

also generalize to semirings

Author: alreadydone

Mathlib/LinearAlgebra/Finsupp/VectorSpace.lean

@@ -22,68 +22,70 @@ open Set LinearMap Submodule
 
 universe u v w
 
+namespace DFinsupp
+
+variable {ι : Type*} {R : Type*} {M : ι → Type*}
+variable [Semiring R] [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)]
+
+/-- The direct sum of free modules is free.
+
+Note that while this is stated for `DFinsupp` not `DirectSum`, the types are defeq. -/
+noncomputable def basis {η : ι → Type*} (b : ∀ i, Basis (η i) R (M i)) :
+    Basis (Σ i, η i) R (Π₀ i, M i) :=
+  .ofRepr
+    ((mapRange.linearEquiv fun i => (b i).repr).trans (sigmaFinsuppLequivDFinsupp R).symm)
+
+variable (R M) in
+instance _root_.Module.Free.dfinsupp [∀ i : ι, Module.Free R (M i)] : Module.Free R (Π₀ i, M i) :=
+  .of_basis <| DFinsupp.basis fun i => Module.Free.chooseBasis R (M i)
+
+variable [DecidableEq ι] {φ : ι → Type*} (f : ∀ i, φ i → M i)
+
+open Finsupp (linearCombination)
+
+theorem linearIndependent_single (hf : ∀ i, LinearIndependent R (f i)) :
+    LinearIndependent R fun ix : Σ i, φ i ↦ single ix.1 (f ix.1 ix.2) := by
+  classical
+  have : linearCombination R (fun ix : Σ i, φ i ↦ single ix.1 (f ix.1 ix.2)) =
+    DFinsupp.mapRange.linearMap (fun i ↦ linearCombination R (f i)) ∘ₗ
+    (sigmaFinsuppLequivDFinsupp R).toLinearMap := by ext; simp
+  rw [LinearIndependent, this]
+  exact ((DFinsupp.mapRange_injective _ fun _ ↦ map_zero _).mpr hf).comp (Equiv.injective _)
+
+lemma linearIndependent_single_iff :
+    LinearIndependent R (fun ix : Σ i, φ i ↦ single ix.1 (f ix.1 ix.2)) ↔
+      ∀ i, LinearIndependent R (f i) :=
+  ⟨fun h i ↦ (h.comp _ sigma_mk_injective).of_comp (lsingle i), linearIndependent_single _⟩
+
+end DFinsupp
+
 namespace Finsupp
 
 section Semiring
 
 variable {R : Type*} {M : Type*} {ι : Type*}
 variable [Semiring R] [AddCommMonoid M] [Module R M]
 
-theorem linearIndependent_single {φ : ι → Type*} (f : ∀ ι, φ ι → M)
+theorem linearIndependent_single {φ : ι → Type*} (f : ∀ i, φ i → M)
     (hf : ∀ i, LinearIndependent R (f i)) :
     LinearIndependent R fun ix : Σ i, φ i ↦ single ix.1 (f ix.1 ix.2) := by
   classical
-  have : linearCombination R (fun ix : Σ i, φ i ↦ single ix.1 (f ix.1 ix.2)) =
-    (finsuppLequivDFinsupp R).symm.toLinearMap ∘ₗ
-    DFinsupp.mapRange.linearMap (fun i ↦ linearCombination R (f i)) ∘ₗ
-    (sigmaFinsuppLequivDFinsupp R).toLinearMap := by ext; simp
-  rw [LinearIndependent, this]
-  exact (finsuppLequivDFinsupp R).symm.injective.comp <|
-    ((DFinsupp.mapRange_injective _ fun _ ↦ map_zero _).mpr hf).comp (Equiv.injective _)
+  convert (DFinsupp.linearIndependent_single _ hf).map_injOn
+    _ (finsuppLequivDFinsupp R).symm.injective.injOn
+  simp
 
-lemma linearIndependent_single_iff {φ : ι → Type*} {f : ∀ ι, φ ι → M} :
+lemma linearIndependent_single_iff {φ : ι → Type*} {f : ∀ i, φ i → M} :
     LinearIndependent R (fun ix : Σ i, φ i ↦ single ix.1 (f ix.1 ix.2)) ↔
-      ∀ i, LinearIndependent R (f i) := by
-  refine ⟨fun h i => ?_, linearIndependent_single _⟩
-  replace h := h.comp _ (sigma_mk_injective  (i := i))
-  exact .of_comp (Finsupp.lsingle i) h
+      ∀ i, LinearIndependent R (f i) :=
+  ⟨fun h i ↦ (h.comp _ sigma_mk_injective).of_comp (lsingle i), linearIndependent_single _⟩
 
 open LinearMap Submodule
 
 open scoped Classical in
 /-- The basis on `ι →₀ M` with basis vectors `fun ⟨i, x⟩ ↦ single i (b i x)`. -/
-protected def basis {φ : ι → Type*} (b : ∀ i, Basis (φ i) R M) : Basis (Σi, φ i) R (ι →₀ M) :=
-  Basis.ofRepr
-    { toFun := fun g =>
-        { toFun := fun ix => (b ix.1).repr (g ix.1) ix.2
-          support := g.support.sigma fun i => ((b i).repr (g i)).support
-          mem_support_toFun := fun ix => by
-            simp only [Finset.mem_sigma, mem_support_iff, and_iff_right_iff_imp, Ne]
-            intro b hg
-            simp [hg] at b }
-      invFun := fun g =>
-        { toFun := fun i => (b i).repr.symm (g.comapDomain _ sigma_mk_injective.injOn)
-          support := g.support.image Sigma.fst
-          mem_support_toFun := fun i => by
-            rw [Ne, ← (b i).repr.injective.eq_iff, (b i).repr.apply_symm_apply,
-                DFunLike.ext_iff]
-            simp only [exists_prop, LinearEquiv.map_zero, comapDomain_apply, zero_apply,
-              exists_and_right, mem_support_iff, exists_eq_right, Sigma.exists, Finset.mem_image,
-              not_forall] }
-      left_inv := fun g => by
-        ext i
-        rw [← (b i).repr.injective.eq_iff]
-        ext x
-        simp only [coe_mk, LinearEquiv.apply_symm_apply, comapDomain_apply]
-      right_inv := fun g => by
-        ext ⟨i, x⟩
-        simp only [coe_mk, LinearEquiv.apply_symm_apply, comapDomain_apply]
-      map_add' := fun g h => by
-        ext ⟨i, x⟩
-        simp only [coe_mk, add_apply, LinearEquiv.map_add]
-      map_smul' := fun c h => by
-        ext ⟨i, x⟩
-        simp only [coe_mk, smul_apply, LinearEquiv.map_smul, RingHom.id_apply] }
+protected def basis {φ : ι → Type*} (b : ∀ i, Basis (φ i) R M) : Basis (Σ i, φ i) R (ι →₀ M) :=
+  .ofRepr <| (finsuppLequivDFinsupp R).trans <|
+    (DFinsupp.mapRange.linearEquiv fun i ↦ (b i).repr).trans (sigmaFinsuppLequivDFinsupp R).symm
 
 @[simp]
 theorem basis_repr {φ : ι → Type*} (b : ∀ i, Basis (φ i) R M) (g : ι →₀ M) (ix) :
@@ -95,7 +97,6 @@ theorem coe_basis {φ : ι → Type*} (b : ∀ i, Basis (φ i) R M) :
     ⇑(Finsupp.basis b) = fun ix : Σi, φ i => single ix.1 (b ix.1 ix.2) :=
   funext fun ⟨i, x⟩ =>
     Basis.apply_eq_iff.mpr <| by
-      classical
       ext ⟨j, y⟩
       by_cases h : i = j
       · cases h
@@ -136,24 +137,6 @@ end Ring
 
 end Finsupp
 
-namespace DFinsupp
-variable {ι : Type*} {R : Type*} {M : ι → Type*}
-variable [Semiring R] [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)]
-
-/-- The direct sum of free modules is free.
-
-Note that while this is stated for `DFinsupp` not `DirectSum`, the types are defeq. -/
-noncomputable def basis {η : ι → Type*} (b : ∀ i, Basis (η i) R (M i)) :
-    Basis (Σi, η i) R (Π₀ i, M i) :=
-  .ofRepr
-    ((mapRange.linearEquiv fun i => (b i).repr).trans (sigmaFinsuppLequivDFinsupp R).symm)
-
-variable (R M) in
-instance _root_.Module.Free.dfinsupp [∀ i : ι, Module.Free R (M i)] : Module.Free R (Π₀ i, M i) :=
-  .of_basis <| DFinsupp.basis fun i => Module.Free.chooseBasis R (M i)
-
-end DFinsupp
-
 lemma Module.Free.trans {R S M : Type*} [CommSemiring R] [Semiring S] [Algebra R S]
     [AddCommMonoid M] [Module R M] [Module S M] [IsScalarTower R S M] [Module.Free S M]
     [Module.Free R S] : Module.Free R M :=

Mathlib/LinearAlgebra/StdBasis.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
 import Mathlib.Algebra.Algebra.Pi
-import Mathlib.LinearAlgebra.Finsupp.SumProd
+import Mathlib.LinearAlgebra.Finsupp.VectorSpace
 import Mathlib.LinearAlgebra.FreeModule.Basic
 import Mathlib.LinearAlgebra.LinearIndependent.Lemmas
 
@@ -31,7 +31,6 @@ this is a basis over `Fin 3 → R`.
 
 -/
 
-
 open Function Set Submodule
 
 namespace Pi
@@ -46,38 +45,16 @@ section Module
 
 variable {η : Type*} {ιs : η → Type*} {Ms : η → Type*}
 
-theorem linearIndependent_single [Ring R] [∀ i, AddCommGroup (Ms i)] [∀ i, Module R (Ms i)]
+theorem linearIndependent_single [Semiring R] [∀ i, AddCommMonoid (Ms i)] [∀ i, Module R (Ms i)]
     [DecidableEq η] (v : ∀ j, ιs j → Ms j) (hs : ∀ i, LinearIndependent R (v i)) :
-    LinearIndependent R fun ji : Σj, ιs j ↦ Pi.single ji.1 (v ji.1 ji.2) := by
-  have hs' : ∀ j : η, LinearIndependent R fun i : ιs j => LinearMap.single R Ms j (v j i) := by
-    intro j
-    exact (hs j).map' _ (LinearMap.ker_single _ _ _)
-  apply linearIndependent_iUnion_finite hs'
-  intro j J _ hiJ
-  have h₀ :
-    ∀ j, span R (range fun i : ιs j => LinearMap.single R Ms j (v j i)) ≤
-      LinearMap.range (LinearMap.single R Ms j) := by
-    intro j
-    rw [span_le, LinearMap.range_coe]
-    apply range_comp_subset_range
-  have h₁ :
-    span R (range fun i : ιs j => LinearMap.single R Ms j (v j i)) ≤
-      ⨆ i ∈ ({j} : Set _), LinearMap.range (LinearMap.single R Ms i) := by
-    rw [@iSup_singleton _ _ _ fun i => LinearMap.range (LinearMap.single R (Ms) i)]
-    apply h₀
-  have h₂ :
-    ⨆ j ∈ J, span R (range fun i : ιs j => LinearMap.single R Ms j (v j i)) ≤
-      ⨆ j ∈ J, LinearMap.range (LinearMap.single R (fun j : η => Ms j) j) :=
-    iSup₂_mono fun i _ => h₀ i
-  have h₃ : Disjoint (fun i : η => i ∈ ({j} : Set _)) J := by
-    convert Set.disjoint_singleton_left.2 hiJ using 0
-  exact (disjoint_single_single _ _ _ _ h₃).mono h₁ h₂
-
-theorem linearIndependent_single_one (ι R : Type*) [Ring R] [DecidableEq ι] :
+    LinearIndependent R fun ji : Σ j, ιs j ↦ Pi.single ji.1 (v ji.1 ji.2) := by
+  convert (DFinsupp.linearIndependent_single _ hs).map_injOn _ DFinsupp.injective_pi_lapply.injOn
+
+theorem linearIndependent_single_one (ι R : Type*) [Semiring R] [DecidableEq ι] :
     LinearIndependent R (fun i : ι ↦ Pi.single i (1 : R)) := by
   rw [← linearIndependent_equiv (Equiv.sigmaPUnit ι)]
   exact Pi.linearIndependent_single (fun (_ : ι) (_ : Unit) ↦ (1 : R))
-    <| by simp +contextual [Fintype.linearIndependent_iff]
+    <| by simp +contextual [Fintype.linearIndependent_iffₛ]
 
 lemma linearIndependent_single_of_ne_zero {ι R M : Type*} [Ring R] [AddCommGroup M] [Module R M]
     [NoZeroSMulDivisors R M] [DecidableEq ι] {v : ι → M} (hv : ∀ i, v i ≠ 0) :
@@ -105,7 +82,7 @@ given by `s j` on each component.
 For the standard basis over `R` on the finite-dimensional space `η → R` see `Pi.basisFun`.
 -/
 protected noncomputable def basis (s : ∀ j, Basis (ιs j) R (Ms j)) :
-    Basis (Σj, ιs j) R (∀ j, Ms j) :=
+    Basis (Σ j, ιs j) R (∀ j, Ms j) :=
   Basis.ofRepr
     ((LinearEquiv.piCongrRight fun j => (s j).repr) ≪≫ₗ
       (Finsupp.sigmaFinsuppLEquivPiFinsupp R).symm)