A set of basis vectors is LI (over a semiring)

Stream: Is there code for X?

[Richard Copley]

Think this is any use?

$$\begin{CD} b(s) @>{(↑)}>> M \\ @A≃AeA @AAbA \\ s @>{(↑)}>> ι \end{CD}$$

import Mathlib.LinearAlgebra.Basis

/-- If `b` is a basis for a `Module` over a semiring and `s` is a set of indices then the image
`b '' s` (a set of basis vectors) is linearly independent. Compare `LinearIndependent.image`,
which holds in a module over a ring. -/
theorem Basis.linearIndependent_image {R M ι : Type*} [Semiring R] [AddCommMonoid M] [Module R M]
    (b : Basis ι R M) (s : Set ι) : LinearIndependent R fun x : b '' s => (x : M) := by
  nontriviality R
  let e : s ≃ b '' s := Equiv.Set.image b s b.injective
  rewrite [show (↑) = b ∘ (↑) ∘ e.symm from funext fun ⟨x, w, hws, hwx⟩ => by
    rewrite [Function.comp_apply, Function.comp_apply]
    simp_rw [← hwx]
    rw [Equiv.Set.image_symm_apply]]
  exact b.linearIndependent.comp _ (Subtype.val_injective.comp e.symm.injective)

[Andrew Yang]

I think LinearIndependent.image_of_comp (and thus LinearIndependent.image) generalizes to semirings just fine?

theorem LinearIndependent.image_of_comp {ι ι'} (s : Set ι) (f : ι → ι') (g : ι' → M)
    (hs : LinearIndependent R fun x : s => g (f x)) :
    LinearIndependent R fun x : f '' s => g x := by
  rw [linearIndependent_iff] at hs ⊢
  intros l hl
  obtain ⟨i : f '' s → s, hi⟩ := surjective_onto_image.hasRightInverse
  have hi' : ∀ x, f (i x) = x := fun x ↦ congr_arg Subtype.val (hi x)
  ext j
  have := FunLike.congr_fun (hs (l.mapDomain i)
    (by simpa only [Finsupp.total_mapDomain, Function.comp, hi'])) (i j)
  rwa [Finsupp.mapDomain_apply hi.injective] at this

[Richard Copley]

Great, much better! It's in a section with a comment /-! ### Properties which require `Ring R` -/, so I didn't even consider that.

[Richard Copley]

No reason not to PR that, I think? @Andrew Yang, would you care to do the honours, so that the credit goes where it is due?

[Junyan Xu]

Unfortunately the current behavior of behavior of docs#LinearIndependent is pathologic for semirings. See:
Junyan Xu said:

If we really want rank to work with Semirings we should replace LinearIndependent by an injection from Finsupp. As it stands, Nat as a Nat-module has rank aleph0 ({1,2,3,...} is linearly independent!).

So I'm not sure it's useful to generalize linear independence lemmas to semirings; if we change the definition the proofs would need small fixes.

[Eric Rodriguez]

As far as I can tell this notion of linear algebra over semirings hasn't really been investigated - it'd be a fun experiment to try it out!