inf_Sup_right

Stream: Is there code for X?

[Eric Wieser]

Is this true?

lemma inf_Sup_right {α : Type*} [complete_lattice α] (s : set α) {b : α} :
Sup s ⊓ b = ⨆ a ∈ s, a ⊓ b := sorry

Naively I'd expect it to follow from docs#inf_sup_right, but that perhaps presupposes a recursion principle on set. We have docs#supr_inf_le_inf_Sup which states this as an inequality, but I can't tell whether the stronger statement is false or just missing.

[Adam Topaz]

This is not true: If s is a basis of a vector space, and b is a 1-dimensional subspace which is not the span of any member of this basis, that would give a contradiction.

[Adam Topaz]

Sorry, to be more precise s should be the set of spans of members of a basis.

[Adam Topaz]

(the lattice here being the lattice of subspaces of the vector space)

[Eric Wieser]

Oh, I guess i meant complete_distrib_lattice?

[Adam Topaz]

inf_Sup_eq

[Adam Topaz]

docs#inf_Sup_eq

[Adam Topaz]

docs#Sup_inf_eq

[Eric Wieser]

Yep, just found it

[Eric Wieser]

The name doesn't match the pattern that inf_sup_right led me to expect

[Eric Wieser]

The actual motivation for my question was for whether this statement is true:

import order.complete_lattice

open complete_lattice (independent)

example {α : Type*} [complete_lattice α]
  {s : set α} (hs : independent s) {x y : set α} (hx : x ⊆ s) (hy : y ⊆ s) (hxy : disjoint x y) :
  disjoint (Sup x) (Sup y) :=
begin
  admit,
end

I think this one is, but I was only able to prove a weaker statement in #6405

[Eric Wieser]

cc @Aaron Anderson, since I think you added docs#complete_lattice.independent

[Aaron Anderson]

Eric Wieser said:

Is this true?

lemma inf_Sup_right {α : Type*} [complete_lattice α] (s : set α) {b : α} :
Sup s ⊓ b = ⨆ a ∈ s, a ⊓ b := sorry

Naively I'd expect it to follow from docs#inf_sup_right, but that perhaps presupposes a recursion principle on set. We have docs#supr_inf_le_inf_Sup which states this as an inequality, but I can't tell whether the stronger statement is false or just missing.

This is only true in a complete_distrib_lattice, or for directed s in an upper continuous lattice (we don't have a definition for upper continuous, but it's implied by compactly_generated)

[Aaron Anderson]

Eric Wieser said:

The actual motivation for my question was for whether this statement is true:

import order.complete_lattice

open complete_lattice (independent)

example {α : Type*} [complete_lattice α]
  {s : set α} (hs : independent s) {x y : set α} (hx : x ⊆ s) (hy : y ⊆ s) (hxy : disjoint x y) :
  disjoint (Sup x) (Sup y) :=
begin
  admit,
end

I think this one is, but I was only able to prove a weaker statement in #6405

I'm not sure what conditions are necessary for this... it feels like the proof I'm imagining requires inducting on some kind of Steinitz exchange property

[Eric Wieser]

I guess another question to ask would be "if its not true, should independent be redefined such that it is?"

[Damiano Testa]

(deleted)

[Aaron Anderson]

Eric Wieser said:

I guess another question to ask would be "if its not true, should independent be redefined such that it is?"

I can check the literature (by which I mean my one book on lattice theory, which I downloaded like a month and a half ago), but I'm pretty sure that's the default phrasing for all lattices.

[Aaron Anderson]

In order to get the exchange property I'm thinking of, I think what's required is a geometric lattice (as that would correspond to the lattice of closed sets on a matroid), and while we don't have that defined right now, [is_compactly_generated α] [is_modular_lattice α] would suffice.

[Aaron Anderson]

Aaron Anderson said:

Eric Wieser said:

I guess another question to ask would be "if its not true, should independent be redefined such that it is?"

I can check the literature (by which I mean my one book on lattice theory, which I downloaded like a month and a half ago), but I'm pretty sure that's the default phrasing for all lattices.

Yeah, Calugareanu's Lattice Concepts in Module Theory defines independent this way for complete lattices in general, and then proves facts about it assuming more conditions on the lattices.

[Aaron Anderson]

Outline of proof: complete_lattice.independent_iff_finite lets you reduce everything to finsets, and then you can move one element over at a time using disjoint.disjoint_sup_right_of_disjoint_sup_left

[Aaron Anderson]

This should let you show that disjoint (Sup x) (Sup y) where x and y are finsets is equivalent to disjoint (Sup \emptyset) (Sup (x \cup y))

[Aaron Anderson]

which is true

[Kevin Buzzard]

I have this vague idea that this sort of thing is the whole point of matroids (moving things one at a time , eg to prove that all bases of a fdvs have the same size)

[Adam Topaz]

@Kevin Buzzard that's right -- this is the so-called "exchange" axiom.

[Eric Wieser]

Does lean have matroids?

For full context, the statement I was vaguely hoping to prove was:

import linear_algebra.direct_sum_module
open_locale direct_sum
variables {R M ι : Type*} [decidable_eq ι] [semiring R] [add_comm_monoid M] [semimodule R M] (S : ι → submodule R M)

def direct_sum.collapse : (⨁ i, S i) →ₗ[R] ↥(⨆ i, S i) :=
direct_sum.to_module R ι _ $ λ i, submodule.of_le (le_supr S i)

/-- This makes `S` an internal direct sum. -/
lemma direct_sum.collapse_injective (hs : complete_lattice.independent $ set.range S) :
  function.bijective (direct_sum.collapse S) := sorry

[Kevin Buzzard]

I think @Peter Nelson is working on matroids but was having problems with finiteness type class issues

[Peter Nelson]

We have matroids, but unfortunately none of their connections with linear algebra or lattices yet. For what it’s worth, here’s the repository: https://github.com/e45lee/lean-matroids

Messy, WIP, etc.

@Kevin Buzzard, the type class issues have cropped up here and there, but aren’t getting in our way too much. Things are progressing well.

[Eric Wieser]

With the help of clues left by @Hanting Zhang, who may or may not have read this thread, I was able to show essentially the above in #9214, as independent_iff_dfinsupp_lsum_ker. However, the approach that Hanting took works only for add_comm_group M and not add_comm_monoid M as it involves constructions via subtraction. Is it even true for add_comm_monoid M?