Zulip Chat Archive

Stream: Is there code for X?

Topic: inf_Sup_right


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Adam Topaz (Feb 24 2021 at 16:09):

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

view this post on Zulip Eric Wieser (Feb 24 2021 at 16:09):

Oh, I guess i meant complete_distrib_lattice?

view this post on Zulip Adam Topaz (Feb 24 2021 at 16:10):

inf_Sup_eq

view this post on Zulip Adam Topaz (Feb 24 2021 at 16:10):

docs#inf_Sup_eq

view this post on Zulip Adam Topaz (Feb 24 2021 at 16:10):

docs#Sup_inf_eq

view this post on Zulip Eric Wieser (Feb 24 2021 at 16:10):

Yep, just found it

view this post on Zulip Eric Wieser (Feb 24 2021 at 16:11):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Feb 24 2021 at 17:23):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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?"

view this post on Zulip Damiano Testa (Feb 24 2021 at 17:45):

(deleted)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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))

view this post on Zulip Aaron Anderson (Feb 24 2021 at 18:05):

which is true

view this post on Zulip 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)

view this post on Zulip Adam Topaz (Feb 24 2021 at 19:54):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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