Jordan Hölder theorem

Stream: maths

[Chris Hughes]

I've proved a general version of the Jordan Hölder theorem for a class jordan_hoelder_class which I defined and this should mean that it should be possible to prove that subgroup G or submodule M is a Jordan Hölder class. The main definitions are as follows

class jordan_hoelder_class (X : Type u) [lattice X] :=
(is_maximal : X → X → Prop)
(lt_of_is_maximal : ∀ {x y}, is_maximal x y → x < y)
(sup_eq_of_is_maximal : ∀ {x y z}, is_maximal x z → is_maximal y z →
  x ≠ y → x ⊔ y = z)
(is_maximal_inf_left : ∀ {x y z}, is_maximal x z → is_maximal y z → x ≠ y →
  is_maximal (x ⊓ y) x)
(isom : (X × X) → (X × X) → Prop)
--(isom_refl : ∀ x, isom x x)
(isom_symm : ∀ {x y}, isom x y → isom y x)
(isom_trans : ∀ {x y z}, isom x y → isom y z → isom x z)
(second_iso : ∀ x y, isom (x, x ⊔ y) (x ⊓ y, y))```

```lean
structure composition_series (X : Type u) [lattice X] [jordan_hoelder_class X] : Type u :=
(length : ℕ)
(series : fin (length + 1) → X)
(step' : ∀ i : fin length, is_maximal (series i.cast_succ) (series i.succ))

I'm looking for comments on this stuff. There needs to be an API for composition series which includes mapping over morphisms (so we maybe need to define morphisms of and I'm not sure whether to attempt to write this all in the generality of Jordan Hölder class or not). I'm not sure if there are any applications other than groups and modules, obviously if there are more, then we might want a more general API. I may have to change the definition of second_iso to stipulate that x is maximal inside x ⊔ y.

[Alex J. Best]

I definitely think generality is useful here, at least I've seen applications that make use of Jordan Holder for p-divisible groups and the like. My understanding was that the "right" generality is that the theorem holds in any abelian category, how does your Jordan-Holder class compare to that? (Edit: I guess it really should be more general! groups aren't an abelian category after all)

[Alex J. Best]

I'm guessing you already saw https://en.wikipedia.org/wiki/Composition_series#Generalization, I've never heard of those things before but if its the right generality to reduce duplicate proofs maybe groups with a set of operators is the way to go?

[Yakov Pechersky]

Is there a reason to prefer the dependent fin for a series as opposed to a list.chain'?

[Yakov Pechersky]

You could have local notation within the structure like "<m" so that it's more clear that is_maximal has the maximal term on the right.

[Chris Hughes]

Yakov Pechersky said:

Is there a reason to prefer the dependent fin for a series as opposed to a list.chain'?

fin makes it a lot easier to state equivalence of composition series. I just need a fin s₁.length ≃ fin s₂.length to define equivalence, but isomorphisms of lists is harder to deal with.

[Jakob von Raumer]

Here's my Isabelle formalisation of Jordan-Hölder. I compared the isomorphism classes of the quotients as multisets

[Chris Hughes]

Jakob von Raumer said:

Here's my Isabelle formalisation of Jordan-Hölder. I compared the isomorphism classes of the quotients as multisets

That might have been a better idea for me in hindsight.

[Chris Hughes]

One issue is that we don't have a great way of taking the list of adjacent pairs given a list, but I could easily have defined a composition series to be a list of pairs.

[Yakov Pechersky]

zip l l.tail

[Yakov Pechersky]

Which I use to great extent in docs#list.form_perm

[Patrick Massot]

Alex J. Best said:

I'm guessing you already saw https://en.wikipedia.org/wiki/Composition_series#Generalization, I've never heard of those things before but if its the right generality to reduce duplicate proofs maybe groups with a set of operators is the way to go?

I really think anyone interested in math formalization should have a look at Bourbaki. Some of the greatest mathematicians of their time faced a lot of those questions, and they sorted it out. Groups with operators are defined on Page 31 of Algebra I. Jordan-Hölder starts on Page 41.

[Patrick Massot]

I just fixed that Wikipedia page.

[Yaël Dillies]

Context is #17226. I'm looking at docs#jordan_holder_lattice.is_maximal. Is there any other notion of maximality than docs#covby?

[Yaël Dillies]

By that I mean: Will we ever define an instance of docs#jordan_holder_lattice that won't set is_maximal := (⋖)?

[Andrew Yang]

The docstring in the file mentions

In the example of subgroups of a group, is_maximal H K means that H is a maximal normal subgroup of K.

[Yaël Dillies]

Somehow this is still covby, simply in another lattice :thinking:

[Yaël Dillies]

Okay, better question: Will is_maximal always be the pullback of covby over some sublattice of α?

[Yaël Dillies]

I'm trying to see whether there's something automatic about checking the jordan_holder_lattice axioms.

[Yaël Dillies]

(as an aside, that really should be called jordan_hoelder_lattice!)

[Damiano Testa]

(jordan_hölder_lattice would be even better.)

[Yaël Dillies]

(French keyboard users would be overadvantaged :wine:)

[Junyan Xu]

mathlib convention is to not include any accent in declaration names, e.g. docs#stone_cech, docs#witt_vector.teichmuller, docs#picard_lindelof ...

[Damiano Testa]

The fact that this is the convention, does not mean that having accents would be worst! :stuck_out_tongue_wink:

[Junyan Xu]

Lean 4 also use capital letters extensively in declaration names. Maybe we should capitalize appropriately and add accents to the Lean3-Lean4 mathport dictionary?

[Junyan Xu]

We also need proper VSCode (and other text editor) support to type the accents. It seems to follow LaTeX convention now, but you can't actually type ö using \"o according to the list.

[Yaël Dillies]

The thing is that german umlauts have prescribed digramm transcriptions:

• ä → ae
• ö → oe
• ü → ue

[Damiano Testa]

If we really go there, an option could be to allow jordan_hölder_lattice and jordan_holder_lattice to be the same declaration, similar to how -> and → already mean the same.

[David Wärn]

In Swedish web addresses and such, people just write aao instead of åäö (never aa ae oe). It does lose information but it feels like a smaller change than turning one letter into two

[Julian Külshammer]

As Swedes won't get tired to explain the Swedish åäö are separate vowels while the German äöü are umlaut, so it makes sense that there are different rules to transcribe them if they are not available :-)

[David Wärn]

Indeed I could have this discussion all day :-) Let me just say that I agree with the conclusion: we have two different languages with two different conventions and they both make sense. Most occurrences of äö in mathlib are surely German, but there's also docs#picard_lindelof and file#analysis/complex/phragmen_lindelof, where I approve of the status quo

[Johan Commelin]

https://en.wikipedia.org/wiki/Umlaut_(diacritic)#History The German ö ↦ oe phenomenon has a good historical explanation: it reverts a process that took place several centuries ago.

[Junyan Xu]

In the example of subgroups of a group, is_maximal H K means that H is a maximal normal subgroup of K.

Let me note that if you take the lattice of normal subgroups and consider the covby relation, then the composition_series you get is called a chief series. Normal subgroups and submodules are both examples of Ω-subgroups, and it's apparently possible to unify both cases.

(Update: Wikipedia says the butterfly lemma (not in mathlib?) holds for the lattice of Ω-subgroups for any choice of Ω. Maybe that's how you may unify the proofs.)

[Daan van Gent]

But is it a good idea to set up a theory for Omega groups (or I guess monoids acting on groups sounds slightly more modern)? Certainly you won't want to define a module as a commutative Omega group with extra properties.

[Andrew Yang]

I think the current approach is already general enough.
We might want to separate the is_maximal and iso part of the typeclass so that composition series of modules is definitionally equal to compositon series on modular lattices.

[Chris Hughes]

Yaël Dillies said:

Somehow this is still covby, simply in another lattice :thinking:

It isn't really, because the relation of being a normal subgroup is not transitive

[Daan van Gent]

Then we just need a generalization of lattices where le need not be transitive :yum:

[Daan van Gent]

it makes me wonder though how often transitivity is used in all those proofs

[Chris Hughes]

Actually, maybe just taking the transitive closure of the normal subgroup relation works.

[Daan van Gent]

Since we take is_maximal to be covby I guess we don't care about those extra relations.

[Daan van Gent]

Side note: Is it a problem that our underlying set subgroup G gets two partial orders (the usual inclusion and the closure of normal_in)?

[Junyan Xu]

But is it a good idea to set up a theory for Omega groups (or I guess monoids acting on groups sounds slightly more modern)? Certainly you won't want to define a module as a commutative Omega group with extra properties.

docs#mul_distrib_mul_action is the proper typeclass, and docs#module extends its additive version docs#distrib_mul_action. So if to_additive can handle this, then you can write the code for Ω-groups and it automatically applies to modules. We'd also need the multiplicative version of docs#submodule, and relax [module] to [distrib_mul_action], but this has led to timeout. Maybe after transition to Lean 4?

[Junyan Xu]

Actually, maybe just taking the transitive closure of the normal subgroup relation works.

This isn't a lattice though. If H is a maximal subgroup in the whole group G that is not normal, then H and G have no supremum :( G isn't a top element, even though the trivial group is always a bottom element.

[Junyan Xu]

If we only consider those subgroups reachable from the whole group G via (the transitive closure of) the normal-subgroup relation, i.e. the subnormal subgroups, it's true that a subnormal subgroup H of G is a subnormal subgroup of any subgroup containing it, so the transitive closure of the normal-subgroup relation is just the subgroup relation on subnormal subgroups, and the intersection of two subnormal subgroups is still subnormal so infima exist. However, the subgroup generated by two subnormal subgroups may not be subnormal, so it's not clear whether the supremum exists. https://math.stackexchange.com/a/1319663/12932

[Junyan Xu]

Side note: Is it a problem that our underlying set subgroup G gets two partial orders (the usual inclusion and the closure of normal_in)?

I think we don't need to do this; I think in the general situation, the is_maximal H K relation on the lattice of Ω-subgroup is always "H is a maximal Ω-stable normal subgroup in K" (Ω-stable subgroup means the same thing as Ω-subgroup and is a notion independent of K). When G is commutative (e.g. it's a module) or when Ω is the inner automorphisms (so H is normal in G and hence in K), the normality requirement is vacuous and we recover the covby relation.