union_support_maximal_linearIndependent_eq_range_basis

English

For a maximal linearly independent family v in a basis b, the union of the supports of b.repr(v_k) equals the whole index set ι.

Русский

Для максимальной линейно независимой системы v относительно базиса b объединение поддержек b.repr(v_k) охватывает весь набор индексов ι.

LaTeX

$$$\\bigcup_k ((b.repr (v_k)).\\mathrm{support} :\\text{Set } ι) = \\text{Set.univ}$$$

Lean4

/-- Over any ring `R`, if `b` is a basis for a module `M`,
and `s` is a maximal linearly independent set,
then the union of the supports of `x ∈ s` (when written out in the basis `b`) is all of `b`.
-/
theorem union_support_maximal_linearIndependent_eq_range_basis {ι : Type w} (b : Basis ι R M) {κ : Type w'} (v : κ → M)
    (ind : LinearIndependent R v) (m : ind.Maximal) : ⋃ k, ((b.repr (v k)).support : Set ι) = Set.univ := by
  -- If that's not the case,

  by_contra h
  simp only [← Ne.eq_def, ne_univ_iff_exists_notMem, mem_iUnion, not_exists_not, Finsupp.mem_support_iff,
    Finset.mem_coe] at h
  obtain ⟨i, w⟩ := h
  have repr_eq_zero (l) : b.repr (linearCombination R v l) i = 0 := by
    simp [linearCombination_apply, Finsupp.sum, w]
      -- Using this, we'll construct a linearly independent family strictly larger than `v`,
        -- by also using this `b i`.

  let v' (o : Option κ) : M := o.elim (b i) v
  have r : range v ⊆ range v' := by rintro - ⟨k, rfl⟩; exact ⟨some k, rfl⟩
  have r' : b i ∉ range v := fun ⟨k, p⟩ ↦ by simpa [w] using congr(b.repr $p i)
  have r'' : range v ≠ range v' :=
    (r' <| · ▸ ⟨none, rfl⟩)
      -- The key step in the proof is checking that this strictly larger family is linearly independent.

  have i' : LinearIndepOn R id (range v') :=
    by
    apply LinearIndependent.linearIndepOn_id
    rw [linearIndependent_iffₛ]
    intro l l' z
    simp_rw [linearCombination_option, v', Option.elim] at z
    change _ + linearCombination R v l.some = _ + linearCombination R v l'.some at z
    ext
      (_ | a)
          -- We'll first show the coefficient of `b i` is zero,
              -- by expressing the `v k` in the basis `b`, and using that the `v k` have no `b i` term.

    ·
      simpa [repr_eq_zero] using
        congr(b.repr $z i)
          -- All the other coefficients are also equal, because `v` is linear independent,
              -- by comparing the coefficients in the basis `b`.

    have l₁ : l.some = l'.some :=
      ind <|
        b.repr.injective <|
          ext fun j ↦ by
            obtain rfl | ne := eq_or_ne i j
            · simp_rw [repr_eq_zero]
            classical simpa [single_apply, ne] using congr(b.repr $z j)
    exact DFunLike.congr_fun l₁ a
  exact r'' (m (range v') i' r)

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