lattice in which atoms are spanning and independent

Stream: Is there code for X?

[Johan Commelin]

A semisimple Lie algebra is roughly a Lie algebra whose lattice of ideals satisfies

  spanning : sSup {I : LieIdeal R L | IsAtom I} = ⊤
  independent : CompleteLattice.SetIndependent {I : LieIdeal R L | IsAtom I}

There is another axiom, namely

  non_abelian_of_isAtom : ∀ I : LieIdeal R L, IsAtom I → ¬ IsLieAbelian I

but that one isn't lattice-theoretic (afaik).

Do lattices that satisfy those first two axioms have a name? In mathlib?

[Yaël Dillies]

Yes they do have a name in the literature, although I don't remember it. It will be in work of Dilworth or Birkhoff.

[Kevin Buzzard]

What is the definition of a reductive Lie algebra in this language? Here the nonabelian condition is dropped, right?

[Johan Commelin]

You also need to tweak the independence. An abelian Lie algebra of rank > 2 does not satisfy that independence axiom.

[Bryan Gin-ge Chen]

This is just the result of random googling (in particular I have not read the proofs), but Corollary 2.5 of "Lie algebras with a finite number of ideals" by Pilar Benito and Jorge Roldán-López states the equivalence of a bunch of things, including:

• (a) the lattice of ideals of a Lie algebra L is a boolean lattice
• (e) L is either 0 or one of the following Lie algebras: $\mathbb{F} z$, a semisimple algebra $S$ or a direct sum as ideals of $\mathbb{F} z$ and $S$.

(They state that this particular equivalence is also proved in Benito's "The Lattice of Ideals of a Lie Algebra", where it looks like it's Theorem 2.4(iii).)

So maybe spanning and independent are enough to create an instance of BooleanAlgebra?

[Yaël Dillies]

I would think so as it basically amounts to saying that your lattice is atomic

[Kevin Buzzard]

I'm a bit confused by this. Does sl_2 x sl_2 not contain a bunch of diagonal sl_2's which mess up independence?

[Johan Commelin]

Nope, those aren't ideals. Because $[(e,e),(f,0)] = (h,0) \notin \Delta$. The diagonal is of course a subalgebra.

[Kevin Buzzard]

Aah and this argument doesn't apply in the abelian case because you always get (0,0). Weird!

[Johan Commelin]

Yeah, that's why you can only get a rank $\le 1$ abelian ideal. So we need the non-abelian axiom to exclude that.

[Johan Commelin]

But here's my next roadblock: suppose that $S, T$ are disjoint subsets of some complete lattice, and suppose that $S \cup T$ is SetIndependent. This means that for every $x \in S \cup T$ we have know that $x$ is disjoint from $\text{Sup} (S \cup T - \{x\})$.

Does it follow that $\text{Sup}(S)$ and $\text{Sup}(T)$ are disjoint?

I'm afraid it doesn't.

[Edward van de Meent]

i think you mean $\text{Sup}(S∪T−\{x\})$

[Edward van de Meent]

i think i may have a counterexample? let $A$ and $B$ be some infinite disjoint sets, and add an additional element $z$, and let $X=A \cup B \cup \{z\}$. Then consider the lattice on $\{R \in \mathcal{P}(X) | z \in R \rightarrow R.\text{Finite} \vee A \cup B \subseteq R\}$. Use the ordering given by subset relation. then choose $S = \{\{a\}| a \in A\}$ and $T = \{\{b\}|b \in B\}$. I believe this should be a complete lattice? At least i'm pretty certain that if it is, these $S$ and $T$ satisfy the requirements for being a counterexample?

[Edward van de Meent]

i'm not very familiar with lattices but i got nerdsniped :upside_down:

[Edward van de Meent]

oops nope

[Yaël Dillies]

Funnily enough, this discussion just showed up independently here: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Proof.20over.20indexed.3F.20sum.20and.20indexed.3F.20set.2E.2E.2E

[Yakov Pechersky]

My (poor) intuition suggests that if S and T are nice finite objects like finite Sets, Finsets, (finite families of Submodules in the linked thread), then Sup(S) and Sup(T) are disjoint: keep subtracting elements from S \union T to form your T. But I don't think this will be the case for an arbitrary complete lattice, where Sup(S) can be "outside" of S. Struggling to come up with a mental model of such.

[Mitchell Lee]

My friend found this counterexample:
441941529_844831864210464_922894223539858177_n.jpg

[Mitchell Lee]

Never mind, this isn't a lattice. But you can probably make it into a lattice by using the Dedekind completion.

[Antoine Chambert-Loir]

In the equivalence (a)-(e) of the Benito and Roldán-López, paper mentioned above, one shouldn't miss assertion
(d): The Jacobson radical of L is trivial and Z(L) has dimension at most 1.
which seems to be equivalent to the assertion (a) that the lattice of Lie ideals of L is boolean.

[Johan Commelin]

If I have a CompleteLattice, and I can show that it is a BooleanAlgebra. How do I make a CompleteBooleanAlgebra out of that?

[Ruben Van de Velde]

I think you ask @Yaël Dillies

[Yaël Dillies]

instance : CompleteBooleanAlgebra JohansType where
  __ := JohansType.instBooleanAlgebra
  __ := JohansType.instCompleteLattice
  iInf_sup_le_sup_sInf := sorry

?

[Yaël Dillies]

I don't think complete distributivity comes for free from the fact it's a boolean algebra, although https://en.wikipedia.org/wiki/Complete_Boolean_algebra disagrees

[Johan Commelin]

Ok, I don't need this urgently, and I don't have time to think about this atm... So then I'll just postpone this.

[Yaël Dillies]

Actually I believe docs#CompleteBooleanAlgebra is not what Wikipedia calls a "complete boolean algebra", precisely because we are enforcing complete distributivity and they are not. I'm thinking this because they mention that regular open sets in a topological space form a complete boolean algebra, and I don't think that this is completely distributive.

[Yaël Dillies]

We had a similar problem with CompleteDistribLattice, which we fixed by renaming it to docs#CompletelyDistribLattice and acquiring the weaker docs#CompleteDistribLattice