feat(group_theory/iwasawa.lean): add a proof of the Iwasawa criterion for simplicity by AntoineChambert-Loir · Pull Request #10253 · leanprover-community/mathlib3

AntoineChambert-Loir · 2021-11-09T23:43:02Z

Add the Iwasawa criterion for simplicity.
This criterion can be used in the proof of simplicity of some classical
groups such as the alternating group or the projective special linear group
(these applications are TODO).

jcommelin · 2021-11-10T04:27:24Z

src/group_theory/iwasawa.lean

+
+**Lemma.** If the action is 2-transitive, then it is primitive.
+
+**Theorem (Iwasawa criterion).** Let G be a group with a primitive action on a set X.


Thanks for this module docstring at the top of the file!
Could you please cross-link to the Lean code below, by adding the name of Lean theorems/defs (in backticks) to this list of thms/defs? The generated html documentation will automatically turn those into hyperlinks and people who open this file will quickly know the Lean name of the main result.

src/group_theory/iwasawa.lean

jcommelin · 2021-11-10T20:32:35Z

src/group_theory/iwasawa.lean

+
+/-- An subgroup is maximal if it is maximal in the collection of proper subgroups. -/
+class subgroup.is_maximal (K : subgroup G) : Prop := 
+  (out : is_coatom K)  


Suggested change

(out : is_coatom K)

(out : is_coatom K)

jcommelin · 2021-11-10T20:34:41Z

src/group_theory/iwasawa.lean

+theorem is_maximal_iff {K: subgroup G} : K.is_maximal ↔
+  K ≠ ⊤ ∧ ∀ (H: subgroup G) g, K ≤ H → g ∉ K → g ∈ H → H = ⊤ :=
+begin
+  split, 


Please put { } around the subproofs that work on the two goals.
I see that you are structuring your proof with newlines, which also indicates the subproofs, but the mathlib style is to use { }-blocks around subproofs.

jcommelin · 2021-11-10T20:39:00Z

src/group_theory/iwasawa.lean

+  begin 
+    simp, intro z, rw z at hgK, exact hgK hgH,
+  end,


Two remarks:

You can save two lines, by just writing { some, tactic, proof }, instead of the begin .. end block.

Please replace simp by the output of squeeze_simp. (In VScode, you can even click on the output in the goal view, and it will automatically replace it.) The reason we don't want a bare simp halfway a proof is the following: if someone adds new simp-lemmas to file X, and in a later PR file X is added as import to one of the dependencies of this Iwasawa file, all of a sudden, this simp might do more/different stuff from what it is doing now. And then this proof breaks. But the person who is adding this import maybe doesn't understand the maths in this file. So now they have a PR with a broken proof in random part of the library that they don't know how to fix.
Long story short: squeeze_simp helps a lot with long-term maintenance of proofs. See also https://leanprover-community.github.io/glossary.html#non-terminal-simp

Thanks! The main reason for my begin … end blocks is that I wrote theorem …… := …,
and the {… } syntax didn't work until I changed the := to ,.

Regarding 2, this is an issue I had imagined you could have, when people rewrite/extend tactics.
Most often, squeeze_simp suggests a simp only [do_stuff]
and I see that rw do_stuff suffices.
Is it enough to leave the simp only or is it better to change it to rw?

Usually simp only is fine. rw is slightly faster, but is a bit less powerful than simp only. I wouldn't worry too much for now. simp only is stable and pretty fast.

jcommelin · 2021-11-10T20:41:27Z

src/group_theory/iwasawa.lean

+end
+
+/-- f(f⁻¹(t)) = f.range ∩ t  -/
+lemma map_comap_of {α β : Type*} (f: α → β) (t: set β):


I think the more predictable name would be to use image_preimage_eq. Also, these lemmas should move to some basic file about set.

jcommelin · 2021-11-10T20:41:34Z

src/group_theory/iwasawa.lean

+  by rw [← set.image_univ, ← set.image_inter_preimage f set.univ t, set.univ_inter]
+
+/-- If f is surjective, then f(f⁻¹(t)) = t -/
+lemma map_comap_of_surjective {α β : Type*} (f : α → β) (t : set β) :


How to guess whether they exist in some form ?

You can try to prove them by library_search. That might tell you they already exist.

tb65536

Golfed the last two proofs.

src/group_theory/iwasawa.lean

AntoineChambert-Loir · 2021-11-14T13:02:58Z

I have one question about lines 202, 203, 214, where I want to use exists_ne.
Lean was not able of getting the hypothesis hX : nontrivial X by itself, so I resorted to use the full form, typing @exists_ne _ hX x form. Is there a better way to do this?

src/group_theory/iwasawa.lean

AntoineChambert-Loir · 2021-11-19T17:24:25Z

Some checks fail, I don't understand why, nor whether it's important.

tb65536

In addition to these comments, can you also refactor the PR to comply with https://leanprover-community.github.io/contribute/style.html

In particular, 2 spaces to indent, spaces after binders, hypotheses before colon, single tactic per line, braces should not be alone on a line.

tb65536 · 2021-11-19T21:14:10Z

src/group_theory/iwasawa.lean

+  intros is_surj is_comm,
+  apply is_commutative.mk,
+  intros a b,
+    obtain ⟨a', ha'⟩ := is_surj a, obtain ⟨b', hb'⟩ := is_surj b,
+    rw ← ha', rw ← hb',
+    let z := ⇑φ, let z₂ := φ.to_fun, have : z = z₂  , by refl,
+    rw ← mul_hom.map_mul φ a' b',
+    rw ← mul_hom.map_mul φ b' a',
+    apply φ.congr_arg,
+    refine is_commutative.cases_on is_comm _, intro,
+    exact comm a' b',


Suggested change

intros is_surj is_comm,

apply is_commutative.mk,

intros a b,

obtain ⟨a', ha'⟩ := is_surj a, obtain ⟨b', hb'⟩ := is_surj b,

rw ← ha', rw ← hb',

let z := ⇑φ, let z₂ := φ.to_fun, have : z = z₂ , by refl,

rw ← mul_hom.map_mul φ a' b',

rw ← mul_hom.map_mul φ b' a',

apply φ.congr_arg,

refine is_commutative.cases_on is_comm _, intro,

exact comm a' b',

refine λ hφ hG, ⟨λ a b, _⟩,

obtain ⟨a, rfl⟩ := hφ a,

obtain ⟨b, rfl⟩ := hφ b,

rw [←φ.map_mul, ←φ.map_mul, hG.comm],

tb65536 · 2021-11-19T21:20:01Z

src/group_theory/iwasawa.lean

+
+variables (G X)
+structure is_primitive
+extends is_transitive G X : Prop :=


Why not just use is_pretransitive? The only serious issue arises in the proof of Iwasawa_mk, but there you can deduce nonempty X from mul_action.fixed_points N X ≠ ⊤.

Suggested change

extends is_transitive G X : Prop :=

extends is_pretransitive G X : Prop :=

The name of the structure should reflect its mathematical name.
As you notice, the Iwasawa lemma uses two properties of is_primitive, is_transitive and has_maximal_stabilizers, while the third one, as you indicate, could be derived from the other hypothesis.
Does it make sense to define is_preprimitive which would just remove the is_nonempty field?

Either is_primitive or is_preprimitive is fine with me.

eric-wieser · 2021-11-24T13:50:48Z

src/group_theory/iwasawa.lean

+lemma surj_to_comm {G H : Type*} [has_mul G] [has_mul H] (φ: mul_hom G H) :
+   function.surjective φ → is_commutative G (*) → is_commutative H (*) :=
+begin
+  intros is_surj is_comm,


If your proof starts with intros then you should have put something before the colon:

Suggested change

lemma surj_to_comm {G H : Type*} [has_mul G] [has_mul H] (φ: mul_hom G H) :

function.surjective φ → is_commutative G (*) → is_commutative H (*) :=

begin

intros is_surj is_comm,

lemma surj_to_comm {G H : Type*} [has_mul G] [has_mul H] (φ : mul_hom G H)

(is_surj : function.surjective φ) (is_comm : is_commutative G (*)) : is_commutative H (*) :=

begin

Oh yes ! I learned recently about the style convention for universal assumptions.

eric-wieser · 2021-11-24T13:55:53Z

src/group_theory/specific_groups/alternating.lean

+  }
+end
+
+private lemma stupid_lemma {A : Type*} [group A] (B : subgroup A) :


This should be called subgroup.comap_subtype_self to match submodule.comap_subtype_self, and should go in subgroup/basic.lean.

pechersky · 2021-11-24T13:59:02Z

src/group_theory/iwasawa.lean

+
+namespace subgroup
+/-- An subgroup is maximal if it is maximal in the collection of proper subgroups. -/
+class is_maximal (K : subgroup G) : Prop :=


You make this a class, yet you never have [is_maximal K] anywhere.

I just copied what was done for maximal ideals.

I definitely agree with this being a class to be consistent - I imagine that instances will accumulate as people do more group theory.

eric-wieser · 2021-11-24T13:59:59Z

src/group_theory/iwasawa.lean

+lemma surj_to_comm {G H : Type*} [has_mul G] [has_mul H] (φ: mul_hom G H)
+   (is_surj : function.surjective φ) (is_comm : is_commutative G (*)) :
+    is_commutative H (*) :=


mathlib indent style, and a better name:

Suggested change

lemma surj_to_comm {G H : Type*} [has_mul G] [has_mul H] (φ: mul_hom G H)

(is_surj : function.surjective φ) (is_comm : is_commutative G (*)) :

is_commutative H (*) :=

lemma function.surjective.mul_commutative {G H : Type*} [has_mul G] [has_mul H] (φ : mul_hom G H)

(is_surj : function.surjective φ) (is_comm : is_commutative G (*)) :

is_commutative H (*) :=

Also, I recommend using commutative ((*) → G → G) instead of is_commutative G (*), which will eliminate the is_commutative.mk and is_commutative.cases_on below.

Do you mean : commutative ((*) : G → G → G) ?

(In any case, that worked as you indicated with this modification…)

Yes I did, whoops!

There are a lot of other is_commutative to rewrite and I wonder whether it is not clearer to refer to the structural properties of objects (groups, etc.) rather than going back to their internal law.

Is there a way to shorten : commutative ((*) : (quotient_group.quotient N) → (quotient_group.quotient N) → (quotient_group.quotient N)) ?

Does commutative ((*) : _ → _ → quotient_group.quotient N) work?

No, but you certainly know how to recover, if G is a group/monoid/... its mul law, or any of its types that are part of its structure. (What if there are many of them?)

I don't understand the question

I had hoped that something like (quotient_group.quotient N).mul would give me the mul part of the group (monoid) structure of quotient_group.quotient N. But that didn't work like that.

eric-wieser · 2021-11-24T14:01:06Z

src/group_theory/iwasawa.lean

+    obtain ⟨a', ha'⟩ := is_surj a, obtain ⟨b', hb'⟩ := is_surj b,
+    rw ← ha', rw ← hb',
+    let z := ⇑φ, let z₂ := φ.to_fun, have : z = z₂  , by refl,


Suggested change

obtain ⟨a', ha'⟩ := is_surj a, obtain ⟨b', hb'⟩ := is_surj b,

rw ← ha', rw ← hb',

let z := ⇑φ, let z₂ := φ.to_fun, have : z = z₂ , by refl,

obtain ⟨a', rfl⟩ := is_surj a,

obtain ⟨b', rfl⟩ := is_surj b,

you never used this have or let.

… for simplicity Add the Iwasawa criterion for simplicity. This criterion can be used in the proof of simplicity of some classical groups such as the alternating group or the projective special linear group (these applications are TODO).

@tb65536

…tuff Use shortened proofs as suggested by @tb65536 Use set.image_preimage and remove unused basic lemmas Use nontrivial and remove useless intermediate results

…he alternating group is perfect Prove what is said: the alternating group on α, with 5 ≤ fintype.card α, is perfect, aka equal to its commutator subgroup. Prove two intermediate lemmas, that 3-cycles are commutators and are contained in the commutator subgroup Prove two ugly lemmas that should be (and certainly will) golfed by people more competent than me.

…into hypotheses

… lemmas Shorten the proof of `alternating_group_is_perfect` using a simplification by Johan Commelin

AntoineChambert-Loir · 2021-12-09T11:40:07Z

As I wrote to Patrick this morning, I am self-disappointed. The plan I had to write this proof broke down 5 minutes before its conclusion.
The Iwasawa criterion is formalized, it should be used to prove simplicity of PSL(n) (as Iwasawa did), but for the alternating group, what it nicely proves, and this is now formalized, is that the normal subgroups of the symmetric groups are \bot, \top, and the alternating group. I am not sure how to derive the simplicity of the alternating group from that.

alexjbest · 2021-12-09T12:17:47Z

Can you elaborate a bit @AntoineChambert-Loir ? The things you say are now formalized are they in this PR or somewhere else?
I guess I see why knowing the normal subgroups of S_n doesn't automatically give you simplicity of A_n, but what application of Iwaswa's criterion are you using to get the normal subgroups of S_n (i.e. what set and action?).

AntoineChambert-Loir · 2021-12-09T22:14:34Z

@alexjbest
It is planned to belong to this PR, but I have worked on separate files, I will push them tomorrow or next week, after some polishing, because it is quite a mess.

I applied the Iwasawa criterion (which already belongs to this PR) to the action of the symmetric_group X on pairs of elements of X, and the structure maps a pair {a,b} to the subgroup generated by the transposition equiv.swap a b. An intermediate result is that the stabilizer of such a pair is a maximal subgroup of symmetric_group X (this uses card X \geq 5!). With a proof (that I have formalized) that commutator(symmetric_group X)=alternating_group X, this proves that the normal subgroups of symmetric_group X are \top, \bot and alternating_group X, but this falls short of proving the simplicity of alternating_group X.

Presumably, one can apply the criterion to the action of alternating_group X on 3-element sets of X, mapping such a triple to the subgroup generated by the 3-cycles on this triple s (it is the subgroup of alternating_group X which fixes every element out of s). But for this I need to prove (is it only true ?) that the stabilizers are maximal subgroups of alternating_group X. Wait and see.

The files of the formalization are certainly worth of drastic refactoring. I did a lot of stuff by bare hands, probably because I don't know some idioms, or some parts of the library.

AntoineChambert-Loir · 2021-12-13T22:52:44Z

I have explained a bit of the math on the blog post : https://freedommathdance.blogspot.com/2021/12/not-simple-proofs-of-simplicity.html

AntoineChambert-Loir added the awaiting-review The author would like community review of the PR label Nov 9, 2021

jcommelin reviewed Nov 10, 2021

View reviewed changes

tb65536 reviewed Nov 11, 2021

View reviewed changes

src/group_theory/iwasawa.lean Outdated Show resolved Hide resolved

src/group_theory/iwasawa.lean Outdated Show resolved Hide resolved

tb65536 reviewed Nov 14, 2021

View reviewed changes

src/group_theory/iwasawa.lean Outdated Show resolved Hide resolved

src/group_theory/iwasawa.lean Outdated Show resolved Hide resolved

tb65536 reviewed Nov 14, 2021

View reviewed changes

src/group_theory/iwasawa.lean Outdated Show resolved Hide resolved

tb65536 reviewed Nov 19, 2021

View reviewed changes

tb65536 added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Nov 19, 2021

eric-wieser reviewed Nov 24, 2021

View reviewed changes

pechersky reviewed Nov 24, 2021

View reviewed changes

eric-wieser reviewed Nov 24, 2021

View reviewed changes

Antoine Chambert-Loir added 11 commits November 24, 2021 15:53

style: remove the final #lint

1b0b36f

style (group_theory/iwasawa.lean): shorten proofs and remove unused s…

86839bc

…tuff Use shortened proofs as suggested by @tb65536 Use set.image_preimage and remove unused basic lemmas Use nontrivial and remove useless intermediate results

style(group_theory/iwasawa.lean): add copyright, remove #print

ab8c6bb

style(group_theory/iwasawa.lean): put docstring first

83231db

style: remove some @

d5ef3ac

style: adjust comment for docstring

5eff16d

style: adjust comment for docstring

5a77a4c

style(src/group_theory/iwasawa.lean): put some universal quantifiers …

1157ed0

…into hypotheses

style(src/group_theory/specific_groups/alternating.lean): remove ugly…

d1ca2d4

… lemmas Shorten the proof of `alternating_group_is_perfect` using a simplification by Johan Commelin

AntoineChambert-Loir force-pushed the iwasawa_lemma branch from 71667a8 to d1ca2d4 Compare November 24, 2021 15:55

Antoine Chambert-Loir added 2 commits November 24, 2021 16:56

the good files, finally

41f90a4

style: implementing suggestions of Eric Wieser

af23e25

AntoineChambert-Loir added the bug label Nov 25, 2021

Antoine Chambert-Loir added 2 commits November 25, 2021 21:21

additional corrections which were overlooked in the previous commit

6444a00

style: shorten a line (>100 chars)

b804f5d

blocks and primitive actions

74c53f6

alreadydone changed the title ~~feat(group_theory/iwasawa.lean): add a proof of the Iwasawa criterion…~~ feat(group_theory/iwasawa.lean): add a proof of the Iwasawa criterion for simplicity Oct 29, 2022

kim-em added the too-late This PR was ready too late for inclusion in mathlib3 label Jul 16, 2023


		Lemma. If the action is 2-transitive, then it is primitive.

		Theorem (Iwasawa criterion). Let G be a group with a primitive action on a set X.

	extends is_transitive G X : Prop :=
	extends is_pretransitive G X : Prop :=

Conversation

AntoineChambert-Loir commented Nov 9, 2021 • edited by alreadydone Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

tb65536 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

AntoineChambert-Loir commented Nov 14, 2021

Uh oh!

Uh oh!

Uh oh!

Uh oh!

AntoineChambert-Loir commented Nov 19, 2021

Uh oh!

tb65536 left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

eric-wieser Nov 24, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

eric-wieser Nov 24, 2021 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

AntoineChambert-Loir commented Nov 9, 2021 •

edited by alreadydone

Loading

eric-wieser Nov 24, 2021 •

edited

Loading

eric-wieser Nov 24, 2021 •

edited

Loading