linearIndependent_sum — Mathlib

English

If v is LI on Sum ι ι' → M, then LI on its parts; equivalence with a disjoint span condition.

Русский

Если v линейно независимо на сумме индексов, то также LI на частях; эквивалентно условию о непересечении их спанов.

LaTeX

$$$\\text{LinearIndependent } R v \\leftrightarrow \\text{LinearIndependent } R (v\\circ \\mathrm{Sum.inl}) \\land \\text{LinearIndependent } R (v\\circ \\mathrm{Sum.inr}) \\land \\text{Disjoint}(\\operatorname{span}R(\\{v\\circ\\mathrm{inl}\\}), \\operatorname{span}R(\\{v\\circ\\mathrm{inr}\\}))$$$

Lean4

theorem linearIndependent_sum {v : ι ⊕ ι' → M} :
    LinearIndependent R v ↔
      LinearIndependent R (v ∘ Sum.inl) ∧
        LinearIndependent R (v ∘ Sum.inr) ∧
          Disjoint (Submodule.span R (range (v ∘ Sum.inl))) (Submodule.span R (range (v ∘ Sum.inr))) :=
  by
  classical
  rw [range_comp v, range_comp v]
  refine ⟨?_, ?_⟩
  · intro h
    refine ⟨h.comp _ Sum.inl_injective, h.comp _ Sum.inr_injective, ?_⟩
    exact h.disjoint_span_image <| isCompl_range_inl_range_inr.disjoint
  rintro ⟨hl, hr, hlr⟩
  rw [linearIndependent_iff'] at *
  intro s g hg i hi
  have :
    ((∑ i ∈ s.preimage Sum.inl Sum.inl_injective.injOn, (fun x => g x • v x) (Sum.inl i)) +
        ∑ i ∈ s.preimage Sum.inr Sum.inr_injective.injOn, (fun x => g x • v x) (Sum.inr i)) =
      0 :=
    by
    -- Porting note: `g` must be specified.

    rw [Finset.sum_preimage' (g := fun x => g x • v x), Finset.sum_preimage' (g := fun x => g x • v x), ←
      Finset.sum_union, ← Finset.filter_or]
    · simpa only [← mem_union, range_inl_union_range_inr, mem_univ, Finset.filter_true]
    · exact Finset.disjoint_filter.2 fun x _ hx => disjoint_left.1 isCompl_range_inl_range_inr.disjoint hx
  rw [← eq_neg_iff_add_eq_zero] at this
  rw [disjoint_def'] at hlr
  have A := by
    refine hlr _ (sum_mem fun i _ => ?_) _ (neg_mem <| sum_mem fun i _ => ?_) this
    · exact smul_mem _ _ (subset_span ⟨Sum.inl i, mem_range_self _, rfl⟩)
    · exact smul_mem _ _ (subset_span ⟨Sum.inr i, mem_range_self _, rfl⟩)
  rcases i with i | i
  · exact hl _ _ A i (Finset.mem_preimage.2 hi)
  · rw [this, neg_eq_zero] at A
    exact hr _ _ A i (Finset.mem_preimage.2 hi)

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