Proof over indexed? sum and indexed? set...

Stream: new members

[Arien Malec]

Sorry for the double ?? but I don't know how to set up the following.

Axler, in LADL, wants to prove:

Linear Algebra Done Right

"Suppose 𝑉_1, ..., 𝑉_𝑚 are subspaces of 𝑉. Then 𝑉_1 + ⋯ + 𝑉_𝑚 is a direct sum if and only if the only way to write 0 as a sum 𝑣_1+⋯+𝑣_𝑚, where each 𝑣_𝑘 ∈𝑉_𝑘, is by taking each 𝑣_𝑘 equal to 0`."

Translating to a Mathlib context, we want instead to prove that if for any V_i and V_j, Disjoint V_i V_j then v_1 + ... + v_m = 0 \iff \forall i, v_i = 0. (or something like that).

The proof over 2 elements is:

import Mathlib.Algebra.Module.Submodule.Lattice


variable {R : Type*} {M : Type*}
variable [Ring R] [AddCommGroup M] [Module R M]

example {y z : M} {p : Submodule R M} {p' : Submodule R M}
 (ymem: y ∈ p) (zmem: z ∈ p')  (h': Disjoint p p'):
  y + z = 0 ↔ y = 0 ∧ z = 0 := by
  constructor
  . intro h''
    rw [add_eq_zero_iff_neg_eq] at h''
    constructor
    . have := (Submodule.disjoint_def.mp h') _ (Submodule.neg_mem p ymem) (by rwa [h''])
      exact neg_eq_zero.mp this
    . rw [neg_eq_iff_eq_neg] at h''
      have := (Submodule.disjoint_def.mp h'.symm) _ (Submodule.neg_mem p' zmem) (by rwa [← h''])
      exact neg_eq_zero.mp this
  . rintro ⟨rfl, rfl⟩; simp only [add_zero]

And I assume we want an indexed foo (Σ i?) in the general proof, but I also want to index into the submodules?

What would the natural "shape" of the theorem look like here?

[Ruben Van de Velde]

Probably the first thing to take into account is that the explicit numeric indexing V_1 ··· V_m is probably going to be annoying in lean and you'd rather work with an arbitrary Finset of Vs

[Ruben Van de Velde]

Actually, not sure that fully made sense

[Arien Malec]

I think I can visualize how docs#Finset.sum works with that?

[Arien Malec]

I guess I can't....

[Ruben Van de Velde]

import Mathlib.Algebra.Module.Submodule.Lattice


variable {R : Type*} {M : Type*}
variable [Ring R] [AddCommGroup M] [Module R M]

example {y z : M} {p : Submodule R M} {p' : Submodule R M}
 (ymem: y ∈ p) (zmem: z ∈ p')  (h': Disjoint p p'):
  y + z = 0 ↔ y = 0 ∧ z = 0 := by
  constructor
  . intro h''
    rw [add_eq_zero_iff_neg_eq] at h''
    constructor
    . have := (Submodule.disjoint_def.mp h') _ (Submodule.neg_mem p ymem) (by rwa [h''])
      exact neg_eq_zero.mp this
    . rw [neg_eq_iff_eq_neg] at h''
      have := (Submodule.disjoint_def.mp h'.symm) _ (Submodule.neg_mem p' zmem) (by rwa [← h''])
      exact neg_eq_zero.mp this
  . rintro ⟨rfl, rfl⟩; simp only [add_zero]

open BigOperators
example  {ι : Type} [Fintype ι] {ys : ι → M} {Vs : ι → Submodule R M}
    (mem : ∀ i, ys i ∈ Vs i)  (h': Pairwise (Disjoint on Vs)) :
    ∑ i, ys i = 0 ↔ ∀ i, ys i = 0 := by
  sorry

[Arien Malec]

Perfect! Now for the fun bit :-)

[Arien Malec]

I can't seem to make induction work on Finset.sum -- is there a trick here (I get dependent elimination errors which usually indicated a track)? Or perhaps there's a different way to go at this -- my thought is to follow the shape of the proof above -- for a Finset of length 0/1, the proof is trivially true, and for any other length, induction + the above proof should get me there?

[Yakov Pechersky]

Which induction principle did you use? This usually calls for docs#Finset.cons_induction_on

[Arien Malec]

Tried docs#Finset.sum_induction

[Arien Malec]

But it turns out I was doing induction on an equality. Oops.

[Arien Malec]

So how do I reason over ∑ i, ys i = 0? The CS in me wants to say there's a trivial zero and one length case, and the general case has an induction hypothesis that resolves to the pair proof above, but I don't know what object in Mathlib allows that...

[Arien Malec]

I tried induction/cases over ∑ i, ys i but Lean says that's an M -- so how do I get at the sum?

[Yakov Pechersky]

When you say "reason over" the sum, what do you mean? I think you have the right case. You should induct like this:

import Mathlib

variable {R : Type*} {M : Type*}
variable [Ring R] [AddCommGroup M] [Module R M]


lemma foo {y z : M} {p : Submodule R M} {p' : Submodule R M}
 (ymem: y ∈ p) (zmem: z ∈ p')  (h': Disjoint p p'):
  y + z = 0 ↔ y = 0 ∧ z = 0 := by
  constructor
  . intro h''
    rw [add_eq_zero_iff_neg_eq] at h''
    constructor
    . have := (Submodule.disjoint_def.mp h') _ (Submodule.neg_mem p ymem) (by rwa [h''])
      exact neg_eq_zero.mp this
    . rw [neg_eq_iff_eq_neg] at h''
      have := (Submodule.disjoint_def.mp h'.symm) _ (Submodule.neg_mem p' zmem) (by rwa [← h''])
      exact neg_eq_zero.mp this
  . rintro ⟨rfl, rfl⟩; simp only [add_zero]


open BigOperators

lemma Submodule.sum_eq_iSup (s : Finset ι) (f : ι → Submodule R M) :
    ∑ i ∈ s, f i = ⨆ i ∈ s, f i := by
  induction s using Finset.cons_induction_on with
  | h₁ => simp
  | h₂ ha IH =>
    simp only [Finset.sum_cons, add_eq_sup, IH, Finset.mem_cons, iSup_or, iSup_sup_eq]
    congr
    simp

lemma Submodule.mem_sum_of_mem {s : Finset ι} {f : ι → Submodule R M} (x : M) (hi : ∃ i ∈ s, x ∈ f i) :
    x ∈ ∑ i ∈ s, f i := by
  rw [sum_eq_iSup, mem_iSup]
  intro N hN
  obtain ⟨i, hi, hx⟩ := hi
  exact hN i (mem_iSup_of_mem hi hx)

lemma Submodule.sum_mem_sum_of_forall_mem (s : Finset ι) {f : ι → Submodule R M} {g : ι → M} (h : ∀ i ∈ s, g i ∈ f i):
    ∑ i ∈ s, g i ∈ ∑ i ∈ s, f i := by
  rw [sum_eq_iSup, mem_iSup]
  intro N hN
  exact sum_mem fun i hi => hN i (mem_iSup_of_mem hi (h i hi))


lemma bar (s : Finset ι) {ys : ι → M} {Vs : ι → Submodule R M}
    (mem : ∀ i ∈ s, ys i ∈ Vs i) (h': Pairwise (Disjoint on Vs)) :
    ∑ i ∈ s, ys i = 0 ↔ ∀ i ∈ s, ys i = 0 := by
  induction s using Finset.cons_induction_on with
  | h₁ => simp
  | h₂ ha IH =>
    specialize IH (fun i hi => mem i (by simp [hi]))
    simp only [Finset.sum_cons, Finset.mem_cons, forall_eq_or_imp, ← IH]
    rename_i a s
    convert foo (R := R) _ _ _
    · infer_instance
    · exact (Vs a)
    · exact (∑ i ∈ s, Vs i) -- failed to synthesize instance AddCommMonoid (Submodule R M)
    · exact (mem a (by simp))
    · refine Submodule.sum_mem_sum_of_forall_mem (f := Vs) ?_ ?_
      intro i hi
      simp only [Finset.mem_cons, forall_eq_or_imp] at mem
      exact mem.right _ hi
    rw [Submodule.sum_eq_iSup]
    intro N hN hN'
    sorry

example  {ι : Type} [Fintype ι] {ys : ι → M} {Vs : ι → Submodule R M}
    (mem : ∀ i, ys i ∈ Vs i)  (h': Pairwise (Disjoint on Vs)) :
    ∑ i, ys i = 0 ↔ ∀ i, ys i = 0 := by
  rw [bar _ _ h']
  · simp
  · simpa using mem

[Yakov Pechersky]

I didn't do the Disjoint goal of the split sum. The pairwise disjoint hypothesis for that lemma can likely be weakened. @Yaël Dillies are submodules an Order.Frame? I was hoping to use docs#disjoint_iSup_iff

[Yaël Dillies]

No, they are not. In ℝ² consider the three submodules U = ⟨(0, 1)⟩, V = ⟨(1, 0)⟩, W = ⟨(1, 1)⟩ (subspaces generated by one vector). Then Disjoint U W, Disjoint V W but ¬ Disjoint (U ⊔ V) W.

[Yaël Dillies]

See https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/lattice.20in.20which.20atoms.20are.20spanning.20and.20independent for more relevant discussion

[Yakov Pechersky]

Then likely, pairwise disjoint on Vs isn't strong enough?

[Yaël Dillies]

Indeed. My counterexample also works as a counterexample to your statement

[Yaël Dillies]

You need to assume something like docs#CompleteLattice.SetIndependent

[Arien Malec]

is that the right answer to the question: all the members of a basis are?

[Arien Malec]

I'm doing this thing where Axler is going from his definition of Direct Sum, and I'm trying to go from the right Mathlib starting point...

[Arien Malec]

Also, I see that I'm trying to do induction on the sum, and I need to be doing induction on the Finset of course.

[Arien Malec]

Arien Malec said:

is that the right answer to the question: all the members of a basis are?

or rather, the span of all the elements of a basis are....

[Yakov Pechersky]

OK now with Yael's suggestion:

import Mathlib

variable {R : Type*} {M : Type*}
variable [Ring R] [AddCommGroup M] [Module R M]


lemma foo {y z : M} {p : Submodule R M} {p' : Submodule R M}
 (ymem: y ∈ p) (zmem: z ∈ p')  (h': Disjoint p p'):
  y + z = 0 ↔ y = 0 ∧ z = 0 := by
  constructor
  . intro h''
    rw [add_eq_zero_iff_neg_eq] at h''
    constructor
    . have := (Submodule.disjoint_def.mp h') _ (Submodule.neg_mem p ymem) (by rwa [h''])
      exact neg_eq_zero.mp this
    . rw [neg_eq_iff_eq_neg] at h''
      have := (Submodule.disjoint_def.mp h'.symm) _ (Submodule.neg_mem p' zmem) (by rwa [← h''])
      exact neg_eq_zero.mp this
  . rintro ⟨rfl, rfl⟩; simp only [add_zero]


open BigOperators

lemma Submodule.sum_eq_iSup (s : Finset ι) (f : ι → Submodule R M) :
    ∑ i ∈ s, f i = ⨆ i ∈ s, f i := by
  induction s using Finset.cons_induction_on with
  | h₁ => simp
  | h₂ ha IH =>
    simp only [Finset.sum_cons, add_eq_sup, IH, Finset.mem_cons, iSup_or, iSup_sup_eq]
    congr
    simp

lemma Submodule.mem_sum_of_mem {s : Finset ι} {f : ι → Submodule R M} (x : M) (hi : ∃ i ∈ s, x ∈ f i) :
    x ∈ ∑ i ∈ s, f i := by
  rw [sum_eq_iSup, mem_iSup]
  intro N hN
  obtain ⟨i, hi, hx⟩ := hi
  exact hN i (mem_iSup_of_mem hi hx)

lemma Submodule.sum_mem_sum_of_forall_mem (s : Finset ι) {f : ι → Submodule R M} {g : ι → M} (h : ∀ i ∈ s, g i ∈ f i):
    ∑ i ∈ s, g i ∈ ∑ i ∈ s, f i := by
  rw [sum_eq_iSup, mem_iSup]
  intro N hN
  exact sum_mem fun i hi => hN i (mem_iSup_of_mem hi (h i hi))


lemma bar (s : Finset ι) {ys : ι → M} {Vs : ι → Submodule R M}
    (mem : ∀ i ∈ s, ys i ∈ Vs i) (h': CompleteLattice.SetIndependent (Vs '' s)) :
    ∑ i ∈ s, ys i = 0 ↔ ∀ i ∈ s, ys i = 0 := by
  induction s using Finset.cons_induction_on with
  | h₁ => simp
  | h₂ ha IH =>
    rename_i a s
    simp only [Finset.coe_cons, Set.image_insert_eq] at h'
    specialize IH (fun i hi => mem i (by simp [hi])) ?_
    · -- TODO: factor out
      intro N hN
      specialize @h' N (by simp [hN])
      simp_rw [Set.insert_eq, Set.union_diff_distrib, sSup_union] at h'
      -- can't use disjoint_sup_iff, Submodule isn't a DistribLattice
      intro M hM hM'
      exact h' hM (le_sup_of_le_right hM')
    simp only [Finset.sum_cons, Finset.mem_cons, forall_eq_or_imp]
    rw [foo (R := R) (p := Vs a) (p' := ∑ i ∈ s, Vs i), IH]
    · exact (mem a (by simp))
    · refine Submodule.sum_mem_sum_of_forall_mem (f := Vs) ?_ ?_
      intro i hi
      simp only [Finset.mem_cons, forall_eq_or_imp] at mem
      exact mem.right _ hi
    ·
      have : ⨆ i ∈ s, Vs i = sSup (Vs '' s) := by
        rw [sSup_image]
        simp
      rw [Submodule.sum_eq_iSup, this]
      apply h'.disjoint_sSup (x := Vs a) (y := (Vs '' s))
      · simp
      · simp

lemma CompleteLattice.Independent.setIndependent_image {ι : Type*} {α : Type*} [CompleteLattice α] {t : ι → α}
    (h : CompleteLattice.Independent t) (s : Set ι) :
    CompleteLattice.SetIndependent (t '' s) := by
  apply h.setIndependent_range.mono
  simp

example  {ι : Type} [Fintype ι] {ys : ι → M} {Vs : ι → Submodule R M}
    (mem : ∀ i, ys i ∈ Vs i)  (h': CompleteLattice.Independent Vs) :
    ∑ i, ys i = 0 ↔ ∀ i, ys i = 0 := by
  rw [bar (Finset.univ : Finset ι) (ys := ys) (Vs := Vs) ?_ (h'.setIndependent_image _)]
  simp

[Yakov Pechersky]

can use some cleanup

[Yakov Pechersky]

Crucially, it's nicer to operate on the iSup (maybe even the sSup) than the \Sum

[Arien Malec]

A lot to dig into here -- thanks!

[Arien Malec]

I'm getting elaboration function for 'BigOperators.bigsum' has not been implemented -- does this mean update Mathlib or??

[Ruben Van de Velde]

What's bigsum?

[Yaël Dillies]

Arien Malec said:

I'm getting elaboration function for 'BigOperators.bigsum' has not been implemented -- does this mean update Mathlib or??

Yes

[Yaël Dillies]

... or alternatively use the deprecated \sum i in s, f i notation (instead of the new one \sum i \in s, f i), but I advise you against it

[Yaël Dillies]

Ruben Van de Velde said:

What's bigsum?

That's the name of the elaborator