sequential independence

Stream: Is there code for X?

[Johan Commelin]

Let $U,V,W$ be subspaces of some ambient vector space. Suppose that $V$ and $W$ are disjoint: $V \cap W = 0$. And suppose that $U \cap (V + W) = 0$. Then we can deduce that $V$ is disjoint from $U + W$.

More generally: suppose that $V_i$ is a family of subspaces, where $i$ ranges over Fin n (or maybe some well-ordered indexing set). Then we can deduce that the family $V_i$ is docs#CompleteLattice.Independent by checking that $\bigoplus_{i < k} V_i$ and $V_k$ are disjoint, for all $k$.

Is there a more general type of lattice in which this sort of "sequential independence" implies docs#CompleteLattice.Independent?

[Yaël Dillies]

Does it not just hold in any complete lattice docs#Order.Frame? See docs#disjoint_iSup_iff

[Yaël Dillies]

Ah but vector spaces do not form a frame. Intuitively, I want to say that the correct generality is modular lattices.

[Johan Commelin]

@loogle IsModularLattice ?X, CompleteLattice.Independent ?V

[Johan Commelin]

@loogle IsModularLattice ?X, CompleteLattice.Independent ?V

[loogle]

:shrug: nothing found

[Adam Topaz]

I think this holds more generally than modular lattices (assuming your def of modular is similar to what I have in mind).

[Adam Topaz]

Isn’t this something like an exchange axiom?

[Adam Topaz]

Oh actually I think you’re right that this is stronger and modularity is probably the right level of generality

[Yaël Dillies]

Yes, this feels like it would be equivalent to modularity under some mild nontriviality conditions

[Yaël Dillies]

Do we agree that we want a condition such that a and b sup c are independent iff a sup c and b are independent?

[Yaël Dillies]

For vector spaces this is true because a inf (b sup c) nonempty iff (a sup -c) inf b nonempty (literally expand everything out) iff (a sup c) inf b nonempty

[Johan Commelin]

Assuming b and c are disjoint, right?

[Johan Commelin]

Hmm, I don't really know my way around modular lattices...
@Yaël Dillies do you know what "mild nontriviality conditions" should be added?

import Mathlib.Order.ModularLattice

variable {α : Type*} [CompleteLattice α] [IsModularLattice α]

lemma disjoint_helper (a b c : α) (h₁ : Disjoint b c) (h₂ : Disjoint a (b ⊔ c)) :
    Disjoint b (a ⊔ c) := by
  sorry

[Yaël Dillies]

I think your lemma is true as stated

[Yaël Dillies]

I'm into the last stretch of revision, so I sadly won't be able to help for the next three weeks

[Johan Commelin]

Ok, at least it's good to know that you think the statement is true. That gives me some confidence.

[Yaël Dillies]

The point of modular lattices is to use the interval isomorphisms, so your proof should go through that

[Johan Commelin]

I looked at those, but didn't see a path to the proof yet

[Andrew Yang]

import Mathlib.Order.ModularLattice

variable {α : Type*} [CompleteLattice α] [IsModularLattice α]

lemma disjoint_helper (a b c : α) (h₁ : Disjoint b c) (h₂ : Disjoint a (b ⊔ c)) :
    Disjoint b (a ⊔ c) := by
  rw [disjoint_iff_inf_le, inf_comm, sup_comm]
  trans ((c ⊔ a) ⊓ (b ⊔ c)) ⊓ b
  · simp [inf_assoc]
  rw [sup_inf_assoc_of_le _ le_sup_right, h₂.eq_bot, sup_bot_eq, h₁.symm.eq_bot]

[Kevin Buzzard]

docs#Disjoint.disjoint_sup_right_of_disjoint_sup_left

[Johan Commelin]

Awesome!

[Kevin Buzzard]

lemma disjoint_helper (a b c : α) (h₁ : Disjoint b c) (h₂ : Disjoint a (b ⊔ c)) :
    Disjoint b (a ⊔ c) := by
  rw [sup_comm]
  exact Disjoint.disjoint_sup_right_of_disjoint_sup_left h₁ h₂.symm

[Kevin Buzzard]

The trick is to look slightly beyond the interval isomorphisms in the same file ;-)

[Kevin Buzzard]

And kudos to @Oliver Nash who put exactly (modulo sup_comm) Johan's lemma into mathlib 8 months ago.