## 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

docs#inf_Sup_eq

docs#Sup_inf_eq

#### 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
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
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?"

(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))

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