linearIndependent_of_top_le_span_of_card_eq_finrank

English

If the span of a family that indexes V covers the top, and the cardinality matches finrank, then the family is linearly independent.

Русский

Если порождение семейства индексов покрывает все пространство и размер совпадает с финразмерностью, то семейство линейно независимо.

LaTeX

$$$(\text{spans } \top) \land (|ι| = \operatorname{finrank}_K(V)) \Rightarrow (\text{linearIndependent } f)$$$

Lean4

theorem linearIndependent_of_top_le_span_of_card_eq_finrank {ι : Type*} [Fintype ι] {b : ι → V}
    (spans : ⊤ ≤ span K (Set.range b)) (card_eq : Fintype.card ι = finrank K V) : LinearIndependent K b :=
  linearIndependent_iff'.mpr fun s g dependent i i_mem_s => by
    classical
    by_contra gx_ne_zero
    refine
      not_le_of_gt (span_lt_top_of_card_lt_finrank (show (b '' (Set.univ \ { i })).toFinset.card < finrank K V from ?_))
        ?_
    ·
      calc
        (b '' (Set.univ \ { i })).toFinset.card = ((Set.univ \ { i }).toFinset.image b).card := by
          rw [Set.toFinset_card, Fintype.card_ofFinset]
        _ ≤ (Set.univ \ { i }).toFinset.card := Finset.card_image_le
        _ = (Finset.univ.erase i).card := (congr_arg Finset.card (Finset.ext (by simp [and_comm])))
        _ < Finset.univ.card := (Finset.card_erase_lt_of_mem (Finset.mem_univ i))
        _ = finrank K V := card_eq
    refine spans.trans (span_le.mpr ?_)
    rintro _
      ⟨j, rfl, rfl⟩
          -- The case that `j ≠ i` is easy because `b j ∈ b '' (univ \ {i})`.

    by_cases j_eq : j = i
    swap
    · refine subset_span ⟨j, (Set.mem_diff _).mpr ⟨Set.mem_univ _, ?_⟩, rfl⟩
      exact mt Set.mem_singleton_iff.mp j_eq
    rw [j_eq, SetLike.mem_coe, show b i = -((g i)⁻¹ • (s.erase i).sum fun j => g j • b j) from _]
    · refine neg_mem (smul_mem _ _ (sum_mem fun k hk => ?_))
      obtain ⟨k_ne_i, _⟩ := Finset.mem_erase.mp hk
      refine smul_mem _ _ (subset_span ⟨k, ?_, rfl⟩)
      simp_all only [Set.mem_univ, Set.mem_diff, Set.mem_singleton_iff, and_self, not_false_eq_true]
        -- To show `b i` is a weighted sum of the other `b j`s, we'll rewrite this sum
            -- to have the form of the assumption `dependent`.

    apply eq_neg_of_add_eq_zero_left
    calc
      (b i + (g i)⁻¹ • (s.erase i).sum fun j => g j • b j) =
          (g i)⁻¹ • (g i • b i + (s.erase i).sum fun j => g j • b j) :=
        by rw [smul_add, ← mul_smul, inv_mul_cancel₀ gx_ne_zero, one_smul]
      _ = (g i)⁻¹ • (0 : V) := (congr_arg _ ?_)
      _ = 0 :=
        smul_zero
          _
            -- And then it's just a bit of manipulation with finite sums.

    rwa [← Finset.insert_erase i_mem_s, Finset.sum_insert (Finset.notMem_erase _ _)] at dependent

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