Centralizer of centralizer of centralizer

Stream: maths

[Kevin Buzzard]

I just noticed #13492 in #rss (the PR was made when I was asleep and I didn't get to it this morning before it was merged). Seems to me that "centralizer" is a Galois connection with itself (possibly with an ^op somewhere; smaller things have bigger centralizers) and that this PR could have used such functionality? For example the headline result just looks like it could be a special case of docs#GaloisConnection.u_l_u_eq_u . Or does the op mean that it would be too much of a kerfuffle to use this machinery?

[Yaël Dillies]

The "docs#GaloisConnection is too much of a kerfuffle for my use case" is countered by "Use docs#ClosureOperator" instead

[Johan Commelin]

But it isn't a closure operator, is it? You don't have C^2 = C. How does that golf C^3 = C?

[Johan Commelin]

I think Kevin's claim might work in theory. But I'm not sure whether the op will mess up the practice.

[Yaël Dillies]

Isn't C^2 a closure operator then?

[Johan Commelin]

It is. But how does that give you C^3 = C?

[Yaël Dillies]

I guess that only helps you with C^4 = C

[Johan Commelin]

I don't think C^4 = C is true in general. C^n doesn't stabilise. It alternates.

[Damiano Testa]

There is even the Double centralizer theorem.

[Kevin Buzzard]

It gives you C^4=C^2 :-)

[Kevin Buzzard]

Double centralizer says "sometimes, C^2=id". Like some Galois connections satisfy l(u x)=x.

[Yaël Dillies]

I don't think the double centralizer forms a Galois connection with itself?

[Yaël Dillies]

doubleCentralizer s ⊆ t ↔ s ⊆ doubleCentralizer t sounds like nonsense to me

[Kevin Buzzard]

No, in the same way that l composed with u doesn't form a Galois connection with itself usually. But C : subrings -> subrings^op might form a Galois connection with C^op : subrings^op -> subrings.

[Johan Commelin]

@Yaël Dillies if you restrict to s,t in the subspace of things that are centralizers, then your claim becomes true.

[Yaël Dillies]

s ⊆ doubleCentralizer t ↔ t ⊆ doubleCentralizer s? I guess that's actually true, yeah, since both sides mean "All elements of s commute with all elements of t"

[Johan Commelin]

That's Iff.rfl, right?

[Yaël Dillies]

Johan Commelin said:

if you restrict to s,t in the subspace of things that are centralizers, then your claim becomes true.

Yeah but that's too weak of a statement

[Yaël Dillies]

Sorry, edited

[Kevin Buzzard]

If my hunch about centraliser being a Galois connection with itself is true, then s subset doubleCentralizer t will mean something like Centralizer s superset Centralizer t (which isn't symmetric)

[Frédéric Dupuis]

It's a very easy proof to begin with, so "too much of a kerfuffle to use this machinery" sounds about right!

[Kevin Buzzard]

The argument for it is that you get access to all of the other lemmas too, but the op is worrying me.

I once developed a theory of contravariant functors explicitly and it was fun and nice, you could do things like "composite of a covariant and contravariant functor is contravariant" etc, there were no ops at all. So one could argue that another approach is to develop the theory of contravariant Galois connections (for example the original Galois connection, sending a subset of a Galois group to the subfield it fixes and a subset of the big field to the subgroup which fixes it pointwise) in an op-free manner and then there would be no excuse not to refactor :-) But I am not minded to do that unless there's a bigger application.

[Patrick Massot]

“docs#GaloisConnection is too much of a kerfuffle for my use case” seems very unlikely to ever hold. Galois connections have almost no kerfuffle overhead (by contrast to bringing category theory to a formalization for instance).

[Kevin Buzzard]

The overhead here is just ^op, because it's a coGalois connection.

[Anatole Dedecker]

I also think it would also make sense to have an API for Galois nnections (lol) because they have the extra feature of being entirely symmetric, which would be nice to have reflected in the API, and also because there are a bunch of examples. I also think we lack API about the fact that any Galois connection decomposes as closure operators both ways and an order isomorphism.

[Anatole Dedecker]

I mean we have all the mathematical results, but we need some glue to actual docs#OrderIso