direct product of normal disjoint subgroups mulEquiv to join

Stream: new members

[Alex Brodbelt]

Hi,

I have thought about this for a while and gradually I am able to state more and more of this result in lean, but I suspect there is some roadblock for why it cannot be done?

Otherwise, surely such a theorem should be/is(???) in mathlib?

My idea is to use docs#mul_normal and maybe make it noncomputable as I need to choose $h \in H$ and $k \in K$

(I believe these are the exact assumptions that are necessary - but it is late so I could be wrong ...Anyway, the assumptions are at least a subset of the assumptions below)

import Mathlib

open Subgroup

def prod_iso_join_of_disjoint_of_normal {G : Type*} [Group G] (H K : Subgroup G)
 (hHK : H ⊓ K = ⊥) [hH : Normal H] [hK : Normal K] : H × K ≃* (H ⊔ K :) where
  toFun := fun h_k => ⟨h_k.1 * h_k.2, mul_mem_sup h_k.1.property h_k.2.property⟩
  invFun := fun h_k => sorry
-- How can I use Subgroup.mul_normal to extract h ∈ H and k ∈ K? Ideally the proofs then don't become horrendous... I don't have high hopes.
-- rewrites in term mode are hard...
  left_inv := sorry
  right_inv := sorry
  map_mul' := sorry

This might be a silly question, but I suspect other undergrads will be asking themselves this as well if this has not been asked already.

[Aaron Liu]

This requires an algorithm to "factor" an element of H ⊔ K into an element of H and an element of G. As stated this can't be computable, because such an algorithm does not always exist.

[Kevin Buzzard]

I would first define the group hom, then prove that it's bijective, and then make the noncomputable iso using docs#MulEquiv.ofBijective . The proofs shouldn't be horrendous, they should be short and quite nice!

[Kevin Buzzard]

It's not unimaginable that it's not there, because you're jumping between subgroups and groups, which are unfortunately different things in type theory. People often prefer to stick with one or the other.

[Kevin Buzzard]

PS disjoint should only be in the name of a declaration if docs#Disjoint is used in the statement somewhere, and iso should only be there if docs#CategoryTheory.Iso is present. Check out #naming to learn more.

[Alex Brodbelt]

Ah of course - and I suppose it is better if I call it MulEquiv then?

[Kevin Buzzard]

Alex Brodbelt said:

Ah of course - and I suppose it is better if I call it MulEquiv then?

mulEquiv but yes!

[Alex Brodbelt]

Forgot to come back and post the formalization in case it is useful for someone else...

import Mathlib

open Subgroup

def prod_monoidHom_join {G : Type*} [Group G] (H K : Subgroup G) [hH : Normal H] [hK : Normal K]
  (hHK : Disjoint H K) : H × K →* (H ⊔ K :) where
  toFun h_k := ⟨h_k.1 * h_k.2, mul_mem_sup h_k.1.property h_k.2.property⟩
  map_one' := by simp
  map_mul' := by
    rintro ⟨⟨h₁, hh₁⟩, ⟨k₁, hk₁⟩⟩ ⟨⟨h₂, hh₂⟩, ⟨k₂, hk₂⟩⟩
    simp
    rw [mul_assoc, mul_assoc, ← mul_assoc k₁,
      (Commute.eq (commute_of_normal_of_disjoint K H hK hH (Disjoint.symm hHK) k₁ h₂ hk₁ hh₂))]
    group

open Function

lemma Bijective_prod_monoidHom_join {G : Type*} [Group G] (H K : Subgroup G) [hH : Normal H]
  [hK : Normal K] (hHK : Disjoint H K) : Bijective (prod_monoidHom_join H K hHK) :=  by
  refine ⟨?injective, ?surjective⟩
  case injective =>
    rintro ⟨⟨h₁, h₁_in_H⟩, k₁, k₁_in_K⟩ ⟨⟨h₂, h₂_in_H⟩, k₂, k₂_in_K⟩ h
    simp [prod_monoidHom_join] at h
    have : h₁⁻¹ * h₂ * k₂ * k₁⁻¹ = 1 := by
      rw [mul_assoc, mul_assoc, ← mul_assoc h₂, ← h]
      group
    -- show h₁ * h₂⁻¹  = 1 and k₁ * k₂⁻¹ = 1
    have H₁ : k₂ * k₁⁻¹ = (k₁ * k₂⁻¹)⁻¹ := by
      group
    have key₁ : h₁⁻¹ * h₂ = k₁ * k₂⁻¹ := by
      rw [mul_assoc] at this
      rw [H₁, mul_inv_eq_one] at this
      exact this
    have mul_in_H : k₁ * k₂⁻¹ ∈ H := key₁.symm ▸ mul_mem (inv_mem h₁_in_H) h₂_in_H
    have mul_in_K : k₁ * k₂⁻¹ ∈ K := mul_mem k₁_in_K (inv_mem k₂_in_K)
    rw [disjoint_iff_inf_le] at hHK
    have key₂ : k₁ * k₂⁻¹ = 1 := by
      rw [← mem_bot]
      apply hHK
      refine mem_inf.mpr ⟨mul_in_H, mul_in_K⟩
    rw [key₂] at key₁
    rw [inv_mul_eq_one] at key₁
    rw [mul_inv_eq_one] at key₂
    ext <;> simp [key₁, key₂]
  case surjective =>
    rintro ⟨x, hx⟩
    rw [← SetLike.mem_coe, mul_normal] at hx
    obtain ⟨h, h_in_H, k, k_in_K, hh⟩ := hx
    use ⟨⟨h, h_in_H⟩, ⟨k, k_in_K⟩⟩
    simp [prod_monoidHom_join, hh]

noncomputable def prod_mulEquiv_join_of_normal {G : Type*} [Group G] (H K : Subgroup G)
  (hHK : Disjoint H K) [hH : Normal H] [hK : Normal K] : H × K ≃* (H ⊔ K :) :=
  MulEquiv.ofBijective (prod_monoidHom_join H K hHK) (Bijective_prod_monoidHom_join H K hHK)

[Kevin Buzzard]

Nice!

I feel like it's golfable but I couldn't immediately see how to make it much shorter. You should probably get out of the habit of using non-terminal simps though.

[Eric Wieser]

docs#Subgroup.IsComplement might be of interest here

[Alex Brodbelt]

Kevin Buzzard said:

Nice!

I feel like it's golfable but I couldn't immediately see how to make it much shorter. You should probably get out of the habit of using non-terminal simps though.

What do you mean? How are you simplifying otherwise? By hand? Or is there some other tactic that is preferred?

[Alex Brodbelt]

Eric Wieser said:

docs#Subgroup.IsComplement might be of interest here

I see - so this is where this type of result lives in mathlib!

[Ruben Van de Velde]

You can use simp? and click the "try this" message

[Alex Brodbelt]

º

[Alex Brodbelt]

I see

[Alex Brodbelt]

To be clear, you modify it to a simp only?

[Ruben Van de Velde]

Yes, exactly

[Ruben Van de Velde]

That means that if someone adds new lemmas for simp to try, they don't affect your code. (This is less of an issue if simp closes the goal, because there should be nothing else left to do for the new lemma)