JordanHolderLattice for Subgroup

Stream: maths

[Marcus Camilus]

Hi, everyone. I am trying to find a subgroup Lattice instance of JordanHolderLattice. However, I found it is hard toconsruct a appropriate quotient group for iso case.
since the common subgroup is not necessarily normal so Lean fail to failed to synthesize
HasQuotient (↥K₁) (Subgroup G) in Iso part. Is there a way to slove this?

variable (G : Type*) [Group G]
instance : JordanHolderLattice (Subgroup G) where
  IsMaximal := fun H K => H.Normal ∧ H < K ∧
    ∀ L : Subgroup G, L.Normal → H < L → L ≤ K → L = K
  Iso := fun (H₁, K₁) (H₂, K₂) =>
    Nonempty (K₁ ⧸ H₁ ≃* K₂ ⧸ H₂)
  lt_of_isMaximal := by
    intros H K h
    exact h.2.1
  sup_eq_of_isMaximal := by
    sorry
  isMaximal_inf_left_of_isMaximal_sup := by
    sorry
  iso_symm := by
    sorry
  iso_trans := by
    sorry
  second_iso := by
    sorry

[Kenny Lau]

you usually use (object : typeYouWant) to force coercion

[Marcus Camilus]

Kenny Lau said:

you usually use (object : typeYouWant) to force coercion

How does that works?

[Kenny Lau]

Lean searches the typeclass database for a coercion

[Marcus Camilus]

Kenny Lau said:

Lean searches the typeclass database for a coercion

I tried, but I do not know how to convert the type of H1 to the normal subgroup of K1

[Kenny Lau]

@Marcus Camilus right, that's because you can't (think about what this means in maths)

[Kenny Lau]

https://github.com/leanprover-community/mathlib4/blob/f6b3bf487bff9b227d4435ac186541716ea54978/Mathlib/RingTheory/SimpleModule/Basic.lean#L484

[Kenny Lau]

you can look at a working implementation to see how they do it

[Marcus Camilus]

Kenny Lau said:

Marcus Camilus right, that's because you can't (think about what this means in maths)
```

Kenny Lau said:

https://github.com/leanprover-community/mathlib4/blob/f6b3bf487bff9b227d4435ac186541716ea54978/Mathlib/RingTheory/SimpleModule/Basic.lean#L484

Kenny Lau
Thanks.

[Marcus Camilus]

Kenny Lau said:

Lean searches the typeclass database for a coercion

Kenny Lau said:

Marcus Camilus right, that's because you can't (think about what this means in maths)

Actually, I found a way to solve it.

def Iso1 (X Y : Subgroup G × Subgroup G) : Prop :=
  (Nonempty <| (X.2 ⧸ (X.1.comap X.2.subtype).normalCore) ≃* (Y.2 ⧸ (Y.1.comap Y.2.subtype).normalCore))

But then I encounter another question: it is hard to apply second isomorphism theorem to:

theorem second_iso1 {X Y : Subgroup G} (_ : X ⋖ X ⊔ Y) :
    Iso1 (X,X ⊔ Y) (X ⊓ Y,Y) := by
  constructor
  rw [sup_comm, inf_comm]
  dsimp
  symm
  sorry

[Marcus Camilus]

Marcus Camilus said:

Kenny Lau said:

Lean searches the typeclass database for a coercion

Kenny Lau said:

Marcus Camilus right, that's because you can't (think about what this means in maths)

Actually, I found a way to solve it.

def Iso1 (X Y : Subgroup G × Subgroup G) : Prop :=
  (Nonempty <| (X.2 ⧸ (X.1.comap X.2.subtype).normalCore) ≃* (Y.2 ⧸ (Y.1.comap Y.2.subtype).normalCore))

But then I encounter another question: it is hard to apply second isomorphism theorem to:

theorem second_iso1 {X Y : Subgroup G} (_ : X ⋖ X ⊔ Y) :
    Iso1 (X,X ⊔ Y) (X ⊓ Y,Y) := by
  constructor
  rw [sup_comm, inf_comm]
  dsimp
  symm
  sorry

When I add .normalcore, it is hard to prove the second_iso1. Is there a hint?

[Junyan Xu]

fun H K => H.Normal ∧ H < K ∧ looks too restrictive since H is usually only required to be normal in K rather than in the whole group G. And you can use the Subgroup.subgroupOf API instead of using comap subtype directly. You can also include the normal hypotheses when defining Iso.

The following might be a better start; notice I'm not using pattern matches when defining Iso which is a habit from Lean 3; maybe in Lean 4 they work well now. BTW you might be interested in the discussions at #maths > Jordan Hölder theorem @ 💬.

import Mathlib

variable (G : Type*) [Group G]
instance : JordanHolderLattice (Subgroup G) where
  IsMaximal H K := H < K ∧ (H.subgroupOf K).Normal ∧
    ∀ L : Subgroup G, (L.subgroupOf K).Normal → H < L → L ≤ K → L = K
  Iso HK₁ HK₂ :=
    ∃ (_ : (HK₁.1.subgroupOf HK₁.2).Normal) (_ : (HK₂.1.subgroupOf HK₂.2).Normal),
      Nonempty (HK₁.2 ⧸ HK₁.1.subgroupOf HK₁.2 ≃* HK₂.2 ⧸ HK₂.1.subgroupOf HK₂.2)
  lt_of_isMaximal h := h.1
  sup_eq_of_isMaximal := by
    sorry
  isMaximal_inf_left_of_isMaximal_sup := by
    sorry
  iso_symm := by
    sorry
  iso_trans := by
    sorry
  second_iso := by
    sorry

[Junyan Xu]

And why are you replacing IsMaximal by ⋖? I don't think they're equivalent.