# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: inf_Sup_right

#### Eric Wieser (Feb 24 2021 at 16:04):

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 (Feb 24 2021 at 16:07):

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 (Feb 24 2021 at 16:08):

Sorry, to be more precise `s`

should be the set of spans of members of a basis.

#### Adam Topaz (Feb 24 2021 at 16:09):

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

#### Eric Wieser (Feb 24 2021 at 16:09):

Oh, I guess i meant `complete_distrib_lattice`

?

#### Adam Topaz (Feb 24 2021 at 16:10):

`inf_Sup_eq`

#### Adam Topaz (Feb 24 2021 at 16:10):

#### Adam Topaz (Feb 24 2021 at 16:10):

#### Eric Wieser (Feb 24 2021 at 16:10):

Yep, just found it

#### Eric Wieser (Feb 24 2021 at 16:11):

The name doesn't match the pattern that `inf_sup_right`

led me to expect

#### Eric Wieser (Feb 24 2021 at 17:19):

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 (Feb 24 2021 at 17:23):

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

#### Aaron Anderson (Feb 24 2021 at 17:30):

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 (Feb 24 2021 at 17:33):

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 (Feb 24 2021 at 17:43):

I guess another question to ask would be "if its not true, should `independent`

be redefined such that it is?"

#### Damiano Testa (Feb 24 2021 at 17:45):

(deleted)

#### Aaron Anderson (Feb 24 2021 at 17:46):

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 (Feb 24 2021 at 17:48):

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 (Feb 24 2021 at 17:53):

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 (Feb 24 2021 at 18:01):

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 (Feb 24 2021 at 18:05):

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 (Feb 24 2021 at 18:05):

which is true

#### Kevin Buzzard (Feb 24 2021 at 19:50):

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 (Feb 24 2021 at 19:54):

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

#### Eric Wieser (Feb 25 2021 at 09:27):

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 (Feb 25 2021 at 09:40):

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

#### Peter Nelson (Feb 25 2021 at 13:12):

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.

Last updated: May 17 2021 at 15:13 UTC