Trying to define maximal subgroups

Stream: maths

[Antoine Chambert-Loir]

In the idea of continuing my Lean-apprenticeship, I was in the mood of proving the Iwasawa criterion for simplicity.
One hypothesis is that the stabilizer of a point for the action is maximal subgroup.
I tried this:

variables (G : Type*) [group G] (X : Type*) [mul_action G X]
def is_maximal_subgroup {G: Type*} {hG: group G}
    :=  λ (K: subgroup G), ( G ≠ K ∧ (∀ H: subgroup G, K < H → H = ⊤))
def has_maximal_stabilizers {G : Type*} {hG: group G}  {X: Type*} {aGX: mul_action G X}: Prop
    := ∀ x:X, is_maximal_subgroup (stabilizer G x))

but that does not work, and I don't see why.

Moreover, is there a more idiosyncrasic way of saying this?
For comparison, I couldn't understand how (nor where in mathlib) maximal ideals are defined.

[Johan Commelin]

docs#ideal.is_maximal is maximal ideals

[Riccardo Brasca]

I think that (copying maximal ideals)

class is_maximal (K : subgroup G) : Prop := (out : is_coatom K)

it's OK

[Yaël Dillies]

You can also probably use docs#is_coatom.

[Yaël Dillies]

Aaaaah Riccardo

[Riccardo Brasca]

ahahahah

[Riccardo Brasca]

In any case what you want is a class, since you want to write something like

example {G : Type*} [group G] (K : subgroup G) [is_maximal K] : ...

so Lean will know automatically that K is maximal and you usually don't need to write explicitly the assumption.

[Yaël Dillies]

We're one big mind.

[Antoine Chambert-Loir]

Johan Commelin said:

docs#ideal.is_maximal is maximal ideals

I'm learning about docs here, this is sorcery! How do you use it in practice? Just type sth in the search bar, and pray?

[Riccardo Brasca]

is_coatom is a typical mathlib thing in my opinion. It's used in "standard" math (at least, I didn't know this notation), but if we need the same notion twice, it's better to axiomatize it.

[Yaël Dillies]

ideal.is_maximal could also just be generalized to work in any docs#order_top. It's really just a wrapper around is_coatom.

[Yaël Dillies]

Antoine Chambert-Loir said:

I'm learning about docs here, this is sorcery! How do you use it in practice? Just type sth in the search bar, and pray?

Read, pray, code.

[Johan Commelin]

@Antoine Chambert-Loir I usually just use grep.

[Antoine Chambert-Loir]

Riccardo Brasca said:

is_coatom is a typical mathlib thing in my opinion. It's used in "standard" math (at least, I didn't know this notation), but if we need the same notion twice, it's better to axiomatize it.

It is used, I believe, but for the math that we teach, hence for the one that we have been taught, we have to stay inbetween naming useful concepts and avoiding to introduce too many new stuff.

[Riccardo Brasca]

Antoine Chambert-Loir said:

Johan Commelin said:

docs#ideal.is_maximal is maximal ideals

I'm learning about docs here, this is sorcery! How do you use it in practice? Just type sth in the search bar, and pray?

The search bar works pretty well when you become used to the name convention. Usually you can guess the name of any theorem/def.
Sometimes it is slow, but I think that @Eric Wieser suggested a trick of leaving opened a tab in the browser and then searching in another tab, to avoid to download all the database or something like that.

[Eric Wieser]

Yeah, what's going on is:

• When you start a search for the first time, the docs kick off a background worker to load up the search cache
• Any open tabs will use that background worker
• If you have only a single tab open, and click a link to elsewhere in the docs, chrome says "oh you're navigating away so I can kill this worker", and your search cache has to be built from scratch.

This feels like a bug to me, but I don't think we have much control over it

[Kevin Buzzard]

but that does not work, and I don't see why.

Your brackets don't match (thank you bracket pair colorizer), maybe you didn't open or import the right things (you didn't make a #mwe so it's hard to tell), and {hG : group G} is usually not a good idea -- group has the class attribute so [group G] is usually the right thing.