linearIndependent_monoidHom — Mathlib

English

If v is LI and f is a linear map with kernel disjoint from span of v, then the image of v under f is LI.

Русский

Если v линейно независимо и ядро f дизjointно с span v, то образ v под f линейно независим.

LaTeX

$$$\\text{LinearIndepOn } R\\ id s \\rightarrow \\text{Disjoint}(\\operatorname{span}R s,\\, \\operatorname{ker}f) \\rightarrow \\text{LinearIndepOn } R\\ id (f''s)$$$

Lean4

/-- Dedekind's linear independence of characters -/
@[stacks 0CKL]
theorem linearIndependent_monoidHom (G : Type*) [MulOneClass G] (L : Type*) [CommRing L] [NoZeroDivisors L] :
    LinearIndependent L (M := G → L) (fun f => f : (G →* L) → G → L) :=
  by
  letI := Classical.decEq (G →* L)
  letI : MulAction L L := DistribMulAction.toMulAction
  apply linearIndependent_iff'.2
  intro s
  induction s using Finset.induction_on with
  | empty => simp
  | insert a s has ih =>
    intro g hg
    have h1 (i) (his : i ∈ s) : (g i • i : G → L) = g i • a :=
      by
      ext x
      rw [← sub_eq_zero]
      apply ih (fun j => g j * j x - g j * a x) _ i his
      ext y
      calc
        (∑ i ∈ s, (g i * i x - g i * a x) • i : G → L) y = (∑ i ∈ s, g i * i x * i y) - ∑ i ∈ s, g i * a x * i y := by
          simp [sub_mul]
        _ = (∑ i ∈ insert a s, g i * i x * i y) - ∑ i ∈ insert a s, g i * a x * i y := by simp [Finset.sum_insert has]
        _ = (∑ i ∈ insert a s, g i * (i x * i y)) - ∑ i ∈ insert a s, a x * (g i * i y) :=
          by
          congrm ∑ i ∈ insert a s, ?_ - ∑ i ∈ insert a s, ?_
          · rw [mul_assoc]
          · rw [mul_assoc, mul_left_comm]
        _ = (∑ i ∈ insert a s, g i • i : G → L) (x * y) - a x * (∑ i ∈ insert a s, (g i • (i : G → L))) y := by
          simp [Finset.mul_sum]
        _ = 0 := by rw [hg];
          simp
            -- On the other hand, since `a` is not already in `s`, for any character `i ∈ s`
              -- there is some element of the monoid on which it differs from `a`.

    have h2 (i) (his : i ∈ s) : ∃ y, i y ≠ a y := by
      by_contra! hia
      obtain rfl : i = a := MonoidHom.ext hia
      contradiction
        -- From these two facts we deduce that `g` actually vanishes on `s`,

    have h3 (i) (his : i ∈ s) : g i = 0 := by
      let ⟨y, hy⟩ := h2 i his
      have h : g i • i y = g i • a y := congr_fun (h1 i his) y
      rw [← sub_eq_zero, ← smul_sub, smul_eq_zero] at h
      exact
        h.resolve_right
          (sub_ne_zero_of_ne hy)
            -- And so, using the fact that the linear combination over `s` and over `insert a s` both
              -- vanish, we deduce that `g a = 0`.

    have h4 : g a = 0 :=
      calc
        g a = g a * 1 := (mul_one _).symm
        _ = (g a • a : G → L) 1 := by rw [← a.map_one]; rfl
        _ = (∑ i ∈ insert a s, g i • i : G → L) 1 :=
          by
          rw [Finset.sum_insert has, Finset.sum_eq_zero, add_zero]
          simp +contextual [h3]
        _ = 0 := by rw [hg];
          rfl
            -- Now we're done; the last two facts together imply that `g` vanishes on every element
              -- of `insert a s`.

    exact (Finset.forall_mem_insert ..).2 ⟨h4, h3⟩

Похожие утверждения