useful group theory lemmas

Stream: general

[Frederick Pu]

While doing some group theory assignment questions I came across some lemmas that I can't find in mathlib that may be useful:

theorem card_subgroupOf {G : Type*} [Group G] (H K : Subgroup G) (h : H ≤ K) : Nat.card (H.subgroupOf K) = Nat.card H := by
  conv =>
    enter [2]
    rw [← Subgroup.map_subgroupOf_eq_of_le h]
  symm
  apply Subgroup.card_map_of_injective
  exact Subgroup.subtype_injective K

theorem term_match {G : Type*} [Group G] (a1 a2 b1 b2 : G) : a1 * b1 = a2 * b2 → a2⁻¹ * a1 = b2 * b1⁻¹ := by
  intro h
  have : a1 = (a2 * b2) * b1⁻¹ := by exact eq_mul_inv_of_mul_eq h
  rw [this]
  group

#check Subgroup
open Classical
theorem card_mul_disjoint {G : Type*} [Group G] [Fintype G] (H K : Subgroup G) (hHK : Disjoint H K) : Finset.card {g | ∃ h ∈ H, ∃ k ∈ K, g = h * k } = Nat.card H * Nat.card K := by sorry

If anyone has a way of phrasing theorem card_mul_disjoint {G : Type*} [Group G] [Fintype G] (H K : Subgroup G) (hHK : Disjoint H K) : Finset.card {g | ∃ h ∈ H, ∃ k ∈ K, g = h * k } = Nat.card H * Nat.card K := by sorry in terms of set multiplication that would be great

[Aaron Liu]

definitely don't open Classical for the statement

[Frederick Pu]

I cant get access to the set mul operation for some reason

[Aaron Liu]

how about this

open scoped Pointwise in
theorem card_mul_disjoint {G : Type*} [Group G] [Fintype G] (H K : Subgroup G) (hHK : Disjoint H K) :
    Nat.card ((H : Set G) * (K : Set G)) = Nat.card H * Nat.card K := by
  sorry

[Frederick Pu]

ah that was the issue lol

[Frederick Pu]

i didnt know what pointwise was

[Frederick Pu]

so is + the minkowski sum then

[Aaron Liu]

correct

[Aaron Liu]

but it's scoped to Pointwise

[Aaron Liu]

since it's pointwise

[Frederick Pu]

is card_mul_disjoint something that is already in mathlib

[Aaron Liu]

I don't know

[Aaron Liu]

probably something more useful would be the equiv version

[Aaron Liu]

open scoped Pointwise in
def Subgroup.coeMulCoeEquivProdOfDisjoint {G : Type*} [Group G] (H K : Subgroup G) (hHK : Disjoint H K) :
    ((H : Set G) * (K : Set G)) ≃ H × K := by
  sorry

[Frederick Pu]

Here's the proof btw

open scoped Pointwise in
theorem card_mul_disjoint {G : Type*} [Group G] [Fintype G] (H K : Subgroup G) (hHK : Disjoint H K) : Set.ncard ((H.carrier : Set G) * (K.carrier : Set G) : Set G) = Nat.card H * Nat.card K := by
  have : Nat.card H = Set.ncard H.carrier := by exact rfl
  rw [this]
  have : Nat.card K = Set.ncard K.carrier := by exact rfl
  rw [this]
  rw [← Set.ncard_prod]
  symm
  apply Set.ncard_congr (fun (h, k) _ => h * k)
  intro ⟨h, k⟩ HH
  simp at HH
  simp
  use h
  use HH.1
  use k
  use HH.2
  simp only [Finset.coe_product, Set.coe_toFinset]
  intro ⟨h1, k1⟩ ⟨h2, k2⟩
  intro H1 H2
  intro HH
  simp at HH
  have crux := term_match _ _ _ _ HH
  rw [Subgroup.disjoint_def] at hHK
  have : h2⁻¹ * h1 ∈ H := by
    have : h2⁻¹ ∈ H := by exact (Subgroup.inv_mem_iff H).mpr (H2.1)
    exact (Subgroup.mul_mem_cancel_right H H1.1).mpr this
  specialize hHK this
  have : k2 * k1⁻¹ ∈ K := by
    have : k1⁻¹ ∈ K := by exact (Subgroup.inv_mem_iff K).mpr (H1.2)
    exact (Subgroup.mul_mem_cancel_right K this).mpr H2.2
  rw [← crux] at this
  specialize hHK this
  have : h2 * (h2 ⁻¹ * h1) = h2 * 1 := by
    rw [hHK]
  group at this
  have : (k2 * k1⁻¹) * k1 = 1 * k1 := by
    rw [← crux, hHK]
  group at this
  simp
  tauto

  intro g hg
  simp at hg
  obtain ⟨h, hh, k, hk, HH⟩ := hg
  simp only [Finset.coe_product, Set.coe_toFinset, Set.image_prod, Set.image2_mul]
  use ⟨h, k⟩
  simp only [mem_prod, Subsemigroup.mem_carrier, Submonoid.mem_toSubsemigroup,
    Subgroup.mem_toSubmonoid, exists_prop]
  tauto

[Aaron Liu]

since this equiv version is now applicable to infinite groups

[Frederick Pu]

could you even make teh equivalence a group hom ?

[Frederick Pu]

like≃* or whateer

[Aaron Liu]

I don't think this pointwise product is always a subgroup

[Frederick Pu]

oh yeah it isnt for non abelian groups

[Aaron Liu]

unless they normalize each other or something

[Frederick Pu]

is there a linarith but for groups?

[Frederick Pu]

i find i have to prove a lot of trivial things a lot

[Aaron Liu]

like a tactic for groups?

[Aaron Liu]

well there's group for multiplicatively written groups

[Frederick Pu]

but group is only a terminal tactic anddoesnt use local hyps

[Aaron Liu]

and there's abel for additively written commutative groups

[Frederick Pu]

so i you have multiple equalities you want to combine

[Aaron Liu]

Frederick Pu said:

so i you have multiple equalities you want to combine

isn't that the word problem then which is undecidable

[Frederick Pu]

i mean yeah but in a lot of cases it's something that grind could solve with the right lemmas

[Frederick Pu]

presumably if you're writing a proof your expressions will be quite simple

[Frederick Pu]

like i had to congrArg + group a lot which is just very tedious

[Frederick Pu]

like maybe if group was a grind ruleset rather than a simp one it could be stronger

[Aaron Liu]

do you know about rw and calc and congr()

[Frederick Pu]

i also use calc sometimes

[Aaron Liu]

and cc oh cc was replaced by grind

[Frederick Pu]

i usually have to multiple on both sides somehting or cancel on both sides

[Frederick Pu]

so you cant use calc for that

[Aaron Liu]

and simp is really great too

[Aaron Liu]

lots of things I think you could probably just do simpa using congr(...) for some appropriately chosen ...

[Frederick Pu]

can you give an example im not too familiar with this syntax

[Aaron Liu]

Frederick Pu said:

so you cant use calc for that

well having a group is really great since cancelling is just congrarg with multiplying by the inverse

[Aaron Liu]

Frederick Pu said:

can you give an example im not too familiar with this syntax

do you have an example lemma for me to prove

[Frederick Pu]

still cant use calc tho cause you're chaging the goal so it's technically not transitive you're using injectivitiy

[Aaron Liu]

alright here's your term_match lemma

import Mathlib

theorem term_match {G : Type*} [Group G] (a1 a2 b1 b2 : G)
    (h : a1 * b1 = a2 * b2) : a2⁻¹ * a1 = b2 * b1⁻¹ := by
  simpa only [mul_assoc, mul_inv_cancel, mul_one, inv_mul_cancel_left] using congr(a2⁻¹ * $h * b1⁻¹)

[Frederick Pu]

so is $h a metavriable hole?

[Aaron Liu]

it's an antiquotation

[Aaron Liu]

read the docstring of congr()

[Aaron Liu]

it should appear if you hover over the congr( part

[Frederick Pu]

if we're proving the version of the theorem for the equiv would it need to be noncomputable?

[Aaron Liu]

yes

[Aaron Liu]

since there's no algorithm to compute it

[Aaron Liu]

well, one direction has no algorithm

[Aaron Liu]

the other direction is just the group operation

[Frederick Pu]

do you think i could submit a pr?

[Aaron Liu]

yes I think you could

[Chris Henson]

Here's an attempt to keep your proof structure, but golf a bit with grind:

import Mathlib

@[grind]
theorem term_match {G : Type*} [Group G] (a1 a2 b1 b2 : G)
    (h : a1 * b1 = a2 * b2) : a2⁻¹ * a1 = b2 * b1⁻¹ := by
  simpa only [mul_assoc, mul_inv_cancel, mul_one, inv_mul_cancel_left] using congr(a2⁻¹ * $h * b1⁻¹)

open scoped Pointwise in
theorem card_mul_disjoint {G : Type*} [Group G] [Fintype G] (H K : Subgroup G) (hHK : Disjoint H K) : Set.ncard ((H.carrier : Set G) * (K.carrier : Set G) : Set G) = Nat.card H * Nat.card K := by
  have : Nat.card H = Set.ncard H.carrier := rfl
  have : Nat.card K = Set.ncard K.carrier := rfl
  suffices h : (H.carrier ×ˢ K.carrier).ncard = (H.carrier * K.carrier).ncard by grind [Set.ncard_prod]
  apply Set.ncard_congr (fun p _ => p.1 * p.2)
  · intro ⟨h, k⟩ ⟨hc, kc⟩
    exact ⟨h, hc, k, kc, rfl⟩
  · intro ⟨h₁, k₁⟩ ⟨h₂, k₂⟩ ⟨hc₁, kc₁⟩ ⟨hc₂, kc₂⟩ _
    have : h₂⁻¹ * h₁ ∈ H := (Subgroup.inv_mem_iff H).mpr hc₂ |> (Subgroup.mul_mem_cancel_right H hc₁).mpr
    have : k₂ * k₁⁻¹ ∈ K := ((Subgroup.inv_mem_iff K).mpr kc₁ |> Subgroup.mul_mem_cancel_right K).mpr kc₂
    have : h₂ * (h₂ ⁻¹ * h₁) = h₂ * 1 := by grind [Subgroup.disjoint_def]
    have : k₂ * k₁⁻¹ * k₁ = 1 * k₁ := by grind [Subgroup.disjoint_def]
    grind [inv_mul_cancel_right, one_mul, mul_inv_cancel_left, mul_one]
  · intro _ ⟨h, _, k, _, _⟩
    use ⟨h, k⟩
    grind

[Frederick Pu]

here's the version with equiv:

theorem term_match {G : Type*} [Group G] (a1 a2 b1 b2 : G) : a1 * b1 = a2 * b2 → a2⁻¹ * a1 = b2 * b1⁻¹ := by
  intro h
  have : a1 = (a2 * b2) * b1⁻¹ := by exact eq_mul_inv_of_mul_eq h
  rw [this]
  group

open scoped Pointwise in
noncomputable def card_mul_disjoint {G : Type*} [Group G] (H K : Subgroup G) (hHK : Disjoint H K) : ((H.carrier : Set G) * (K.carrier : Set G) : Set G) ≃ (H:Set G) ×ˢ (K:Set G) := by
  symm
  apply Set.BijOn.equiv (fun (h, k) => h * k)
  apply And.intro
  · intro ⟨h, k⟩ HH
    simp at HH
    simp
    use h
    use HH.1
    use k
    use HH.2
  simp only [Finset.coe_product, Set.coe_toFinset]
  apply And.intro
  intro ⟨h1, k1⟩ H1 ⟨h2, k2⟩ H2
  intro HH
  simp at HH
  have crux : h2⁻¹ * h1 = k2 * k1⁻¹ := term_match _ _ _ _ HH
  rw [Subgroup.disjoint_def] at hHK
  have : h2⁻¹ * h1 ∈ H := by
    have : h2⁻¹ ∈ H := by exact (Subgroup.inv_mem_iff H).mpr (H2.1)
    exact (Subgroup.mul_mem_cancel_right H H1.1).mpr this
  specialize hHK this
  have : k2 * k1⁻¹ ∈ K := by
    have : k1⁻¹ ∈ K := by exact (Subgroup.inv_mem_iff K).mpr (H1.2)
    exact (Subgroup.mul_mem_cancel_right K this).mpr H2.2
  rw [← crux] at this
  specialize hHK this
  have : h2 * (h2 ⁻¹ * h1) = h2 * 1 := by
    rw [hHK]
  group at this
  have : (k2 * k1⁻¹) * k1 = 1 * k1 := by
    rw [← crux, hHK]
  group at this
  simp
  tauto
  intro g hg
  obtain ⟨h, hh, k, hk, HH⟩ := hg
  simp only [Finset.coe_product, Set.coe_toFinset, Set.image_prod, Set.image2_mul]
  rw [Set.mem_mul]
  use h
  use hh
  use k
  use hk

[Eric Wieser]

Aaron Liu said:

open scoped Pointwise in
def Subgroup.coeMulCoeEquivProdOfDisjoint {G : Type*} [Group G] (H K : Subgroup G) (hHK : Disjoint H K) :
    ((H : Set G) * (K : Set G)) ≃ H × K := by
  sorry

Doesn't this require commutativity? Also, I think the LHS is more canonically spelt ↥(H ⊔ K)

[Michael Stoll]

Eric Wieser said:

Doesn't this require commutativity? Also, I think the LHS is more canonically spelt ↥(H ⊔ K)

It does not. And note that the LHS is in general not a subgroup.

[Frederick Pu]

here's teh pull request: https://github.com/leanprover-community/mathlib4/pull/30667

[Frederick Pu]

here are some other lemmas I found useful:

theorem card_subgroupOf {G : Type*} [Group G] (H K : Subgroup G) (h : H ≤ K) : Nat.card (H.subgroupOf K) = Nat.card H := by
  conv =>
    enter [2]
    rw [← Subgroup.map_subgroupOf_eq_of_le h]
  symm
  apply Subgroup.card_map_of_injective
  exact Subgroup.subtype_injective K

theorem eq_of_le_card_eq {G : Type*} [Group G] [Fintype G] (H K : Subgroup G) (h : H ≤ K) : Nat.card H = Nat.card K → H = K := by
  intro hh
  rw [← card_subgroupOf H K h, Subgroup.card_eq_iff_eq_top] at hh
  simp only [Subgroup.subgroupOf_eq_top] at hh
  order

[Frederick Pu]

also is there somehting along the lines of if all generators of a group commute then all elements of the group commute?

[Eric Wieser]

Here's a slightly shorter version of that first theorem:

@[to_additive]
theorem Subgroup.card_subgroupOf_of_le {G : Type*} [Group G] (H K : Subgroup G) (h : H ≤ K) :
    Nat.card (H.subgroupOf K) = Nat.card H := by
  conv_rhs => rw [← map_subgroupOf_eq_of_le h]
  rw [card_map_of_injective Subtype.coe_injective]

[Frederick Pu]

also is there something along these lines?

every decompositino of the idenetity elemebt into trapsnpositions will have an even number of transpotions

[Aaron Liu]

Frederick Pu said:

also is there something along these lines?

every decompositino of the idenetity elemebt into trapsnpositions will have an even number of transpotions

try docs#Equiv.Perm.sign

[Frederick Pu]

is there a proof that the sign for permutation is unique/well defined anywhere?

[Aaron Liu]

what do you mean by "well defined"?

[Aaron Liu]

I guess uniqueness is docs#Equiv.Perm.eq_sign_of_surjective_hom

[Frederick Pu]

like for example every decomposition into transpoisitions will have sign parity number of elements

[Aaron Liu]

I think that follows from docs#Equiv.Perm.sign_swap and the fact that it's a monoid hom

[Frederick Pu]

where in mathlib should these lemmas go?

theorem card_subgroupOf {G : Type*} [Group G] (H K : Subgroup G) (h : H ≤ K) : Nat.card (H.subgroupOf K) = Nat.card H := by
  conv =>
    enter [2]
    rw [← Subgroup.map_subgroupOf_eq_of_le h]
  symm
  apply Subgroup.card_map_of_injective
  exact Subgroup.subtype_injective K

theorem eq_of_le_card_eq {G : Type*} [Group G] [Fintype G] (H K : Subgroup G) (h : H ≤ K) : Nat.card H = Nat.card K → H = K := by
  intro hh
  rw [← card_subgroupOf H K h, Subgroup.card_eq_iff_eq_top] at hh
  simp only [Subgroup.subgroupOf_eq_top] at hh
  order

[Frederick Pu]

should there be a thing like to_additive for automatically getting lemmas about subgroupof from lemmas abotu group. like a to_subgroup

[Kenny Lau]

but we do have @[to_additive]

[Ruben Van de Velde]

The question was whether there should be something analogous for subgroups

[Frederick Pu]

Frederick Pu said:

also is there somehting along the lines of if all generators of a group commute then all elements of the

[Frederick Pu]

also i just realize there is no usable mem_closure_iff for non abelian groups

[Frederick Pu]

here's what i have so far:

import Mathlib

#check Finsupp

theorem Subgroup.mem_closure_range_iff' {ι : Type*} {G : Type*} [Group G]  {f : ι → G} : ∀ x, x ∈ Subgroup.closure (Set.range f) ↔ ∃ l : List ι, x = (l.map f).prod := sorry

example {G : Type*} [Group G] (s : Set G) (hs : ∀ g ∈ s, ∀ g' ∈ s, Commute g g') : CommGroup (Subgroup.closure s) := by
    constructor
    intro ⟨x, hx⟩ ⟨y, hy⟩
    simp only [MulMemClass.mk_mul_mk, Subtype.mk.injEq]
    have hss : Set.range (fun x : s => (x.val:G)) = s := by simp only [Set.range_id', Set.image_univ,
      Subtype.range_coe_subtype, Set.setOf_mem_eq]
    rw [← hss, Subgroup.mem_closure_range_iff'] at hx hy
    obtain ⟨xl, hxl⟩ := hx
    obtain ⟨yl, hyl⟩ := hy
    /-
    case mul_comm
    G : Type u_1
    inst✝ : Group G
    s : Set G
    hs : ∀ g ∈ s, ∀ g' ∈ s, Commute g g'
    x y : G
    hss : (Set.range fun x => ↑x) = s
    xl : List ↑s
    hxl : x = (List.map (fun x => ↑x) xl).prod
    yl : List ↑s
    hyl : y = (List.map (fun x => ↑x) yl).prod
    ⊢ x * y = y * x
    -/
    sorry

[Frederick Pu]

i think the way to prove it is probably double induction on the length of both representative lists

[Aaron Liu]

I think the way to prove it involves docs#Subgroup.centralizer and some universal properties

[Aaron Liu]

no need to get into lists

[Frederick Pu]

so we would need something like centralizer (closure s) = centralizer s right?

[Frederick Pu]

i have no idea what is going on in this proof but after chasing the tail a bunch i got this:

example {G : Type*} [Group G] (s : Set G) (hs : ∀ g ∈ s, ∀ g' ∈ s, Commute g g') : IsMulCommutative (Subgroup.closure s) := by
    rw [← Subgroup.le_centralizer_iff_isMulCommutative]
    have : Subgroup.closure s ≤ Subgroup.centralizer (Subgroup.centralizer s) := by
        apply Subgroup.closure_le_centralizer_centralizer
    suffices : Subgroup.centralizer (Subgroup.centralizer s) ≤ (Subgroup.centralizer (Subgroup.closure s : Subgroup G) : Subgroup G)
    (expose_names; exact fun ⦃x⦄ a => this (this_1 a))
    suffices : Subgroup.closure s ≤ Subgroup.centralizer s
    apply Subgroup.centralizer_le
    exact this
    suffices : Subgroup.centralizer (Subgroup.centralizer s) ≤ Subgroup.centralizer s
    (expose_names; exact fun ⦃x⦄ a => this (this_1 a))
    intro x hx y hy
    rw [Subgroup.mem_centralizer_iff] at hx
    specialize hx y
    apply hx
    exact fun m a => hs m a y hy

[Kevin Buzzard]

You could just prove it using one of the induction principles for Subgroup.closure (you could prove your mem lemma that way, but I wouldn't bother; you can just prove the application that way too). I did one sorry as an example but all 7 look straightforward to me.

import Mathlib

example {G : Type*} [Group G] (s : Set G) (hs : ∀ g ∈ s, ∀ g' ∈ s, Commute g g') : CommGroup (Subgroup.closure s) := by
  constructor
  intro ⟨x, hx⟩ ⟨y, hy⟩
  refine Subgroup.closure_induction₂ ?_ ?_ ?_ ?_ ?_ ?_ ?_ hx hy
  · sorry -- hs
  · sorry -- easy
  · sorry -- easy
  · intros x y z _ _ _ h1 h2
    ext
    simp_all
    rw [mul_assoc, h2, ← mul_assoc, h1, mul_assoc]
  · sorry -- similar
  · sorry -- easy group theory
  · sorry -- easy group theory

Induction principles are almost always easier than some kind of attempt to find a way to represent a general object.

[Frederick Pu]

i think there's a enough machinary with the cnetralizer to not require induction

[Frederick Pu]

this is really good to know for the future tho!

[Frederick Pu]

here's the golfed version:

example {G : Type*} [Group G] (s : Set G) (hs : ∀ g ∈ s, ∀ g' ∈ s, Commute g g') : IsMulCommutative (Subgroup.closure s) := by
    rw [← Subgroup.le_centralizer_iff_isMulCommutative]
    apply (Subgroup.closure_le_centralizer_centralizer s).trans
    apply Subgroup.centralizer_le
    apply (Subgroup.closure_le_centralizer_centralizer s).trans
    intro x hx y hy
    rw [Subgroup.mem_centralizer_iff] at hx
    exact hx y (fun m a => hs m a y hy)

[Chris Henson]

You can omit that last rw.

[Yury G. Kudryashov]

Please make it an iff lemma when you PR it.

[Frederick Pu]

where would this go in mathlib?

[Yury G. Kudryashov]

#find_home could help

[Yury G. Kudryashov]

BTW, I've just found out that we use both docs#Std.Commutative and docs#IsMulCommutative for lemmas/instances about groups.

[Frederick Pu]

i think it should probably be IsMulCommutative so we can use the typeclass instance. Also you can better use to_additive with IsMulCommutative i thihnk

[Yury G. Kudryashov]

UPD: we already have docs#Subgroup.closureCommGroupOfComm

[Frederick Pu]

it's weird that I wasn't able to find that using mathlibsearch

[Frederick Pu]

Kevin Buzzard said:

You could just prove it using one of the induction principles for Subgroup.closure (you could prove your mem lemma that way, but I wouldn't bother; you can just prove the application that way too). I did one sorry as an example but all 7 look straightforward to me.

import Mathlib

example {G : Type*} [Group G] (s : Set G) (hs : ∀ g ∈ s, ∀ g' ∈ s, Commute g g') : CommGroup (Subgroup.closure s) := by
  constructor
  intro ⟨x, hx⟩ ⟨y, hy⟩
  refine Subgroup.closure_induction₂ ?_ ?_ ?_ ?_ ?_ ?_ ?_ hx hy
  · sorry -- hs
  · sorry -- easy
  · sorry -- easy
  · intros x y z _ _ _ h1 h2
    ext
    simp_all
    rw [mul_assoc, h2, ← mul_assoc, h1, mul_assoc]
  · sorry -- similar
  · sorry -- easy group theory
  · sorry -- easy group theory

Induction principles are almost always easier than some kind of attempt to find a way to represent a general object.

should we put this inducton rule in the docstring for Subgroup.closure i feel like that would be really helpful

[Yury G. Kudryashov]

I found it using loogle.

[Yury G. Kudryashov]

We have many ways to say "commutative".

[Yury G. Kudryashov]

Frederick Pu said:

i think it should probably be IsMulCommutative so we can use the typeclass instance. Also you can better use to_additive with IsMulCommutative i thihnk

@Xavier Roblot added this class.

[Frederick Pu]

do we want to change docs#Subgroup.closureCommGroupOfComm to be an if and only if using IsMulCommutative?

[Alex Meiburg]

Yury G. Kudryashov said:

We have many ways to say "commutative".

Not to mention docs#Commute. And there's not a single lemma relating Commute with Std.Commutative or IsMulCommutative! And having an IsMulCommutative lying around is also always equivalent (propositionally, and in terms of the data-carrying instances available) to CommMagma.

[Frederick Pu]

should we also prove the general version where teh H, K aren't disjoint for

theorem card_mul_disjoint {G : Type*} [Group G] [Fintype G] (H K : Subgroup G) (hHK : Disjoint H K) : Set.ncard ((H.carrier : Set G) * (K.carrier : Set G) : Set G) = Nat.card H * Nat.card K := by sorry