2^n = 2^m => n = m?

Stream: new members

[Laurent Bartholdi]

I'm thinking about going through the beginnings of Lyndon&Schupp, "Combinatorial group theory", to see what can be added on free groups. The literally first theorem says that free groups have a well-defined rank. I have in mind

universe u

def FreeGroup.rank (F : Type u) [Group F] [IsFreeGroup F] : Cardinal
  := Cardinal.mk (IsFreeGroup.Generators F)

theorem FreeGroup.unique_rank {F₁ F₂ : Type u} [Group F₁] [Group F₂] [IsFreeGroup F₁] (h : F₁ ≃* F₂) :
  FreeGroup.rank F₁ = @FreeGroup.rank _ _ (IsFreeGroup.ofMulEquiv h) := by
  -- consider the subgroup generated by squares
  -- it has index 2^rank
  -- then from 2^{rank F₁}=2^{rank F₂} deduce rank F₁ = rank F₂
  sorry

But it seems that the last statement, "2^m = 2^n => m = n", is not part of Mathlib. Did I miss it, or do I have to prove something there, or am I following the wrong track?

Taking inspiration from ranks of modules, it seems also that there could/should be "rank" and "finrank" which is guaranteed to be a Nat.

Comments and encouragement are welcome!

[Ruben Van de Velde]

Is it true for cardinals?

[Yaël Dillies]

It is very much false, and that's a fact examiners love to ask in the Cambridge Part II exams :wink:

[Sébastien Gouëzel]

Another way to phrase your statement (maybe more natural) is to say that, if you have two FreeGroupBasis on F, then their indexing sets have the same cardinality.

I don't think the statement 2^m = 2^n => m = nis in mathlib for cardinals, because it's not provable according to https://mathoverflow.net/questions/67473/equality-of-cardinality-of-power-set. Still, I think the result is true. In the case of finite rank, it's the argument you give. For the infinite rank case, say that you have two (infinite) generating sets S and T in a given group (not necessarily free). Then any element of T is a word in the elements of S, and the set of words over S has the same cardinality as S, so #T <= #S (and conversely).

[Sébastien Gouëzel]

Yaël Dillies said:

It is very much false, and that's a fact examiners love to ask in the Cambridge Part II exams :wink:

It's not false, it's just not true :-)

[Sébastien Gouëzel]

But in fact I don't think the index of the subgroup generated by the squares is really 2^n when n is infinite. In fact, the cardinality of the free group over n is equal to n when n is infinite, so it can't have subgroups with index 2^n. I'd guess the index is probably n, and then the issue disappears: the function which maps n to 2^n if n is finite, and to n if n is infinite, is indeed injective.

[Junyan Xu]

It's easier to consider the abelianization (you get the free abelian group, isomorphic to Finsupp) and the result is already in mathlib as FreeAbelianGroup.Equiv.ofIsFreeGroupEquiv:

import Mathlib.GroupTheory.FreeAbelianGroupFinsupp

universe u

def FreeGroup.rank (F : Type u) [Group F] [IsFreeGroup F] : Cardinal :=
  Cardinal.mk (IsFreeGroup.Generators F)

theorem FreeGroup.unique_rank {F₁ F₂ : Type u} [Group F₁] [Group F₂] [IsFreeGroup F₁] (h : F₁ ≃* F₂) :
    FreeGroup.rank F₁ = @FreeGroup.rank _ _ (IsFreeGroup.ofMulEquiv h) :=
  have := IsFreeGroup.ofMulEquiv h
  (FreeAbelianGroup.Equiv.ofIsFreeGroupEquiv h).cardinal_eq

[Martin Dvořák]

FYI: https://github.com/leanprover-community/mathlib4/blob/master/Counterexamples/CanonicallyOrderedCommSemiringTwoMul.lean

[Laurent Bartholdi]

A different approach: I see `LinearEquiv.nonempty_equiv_iff_lift_rank_eq for modules; so perhaps it would be nice to prove

• the abelianization of a free group with basis \iota is isomorphic to the free abelian group on \iota
• the free abelian group on \iota is isomorphic to the free Z-module on \iota

[Junyan Xu]

Free modules are spelt as docs#Finsupp in mathlib, and docs#FreeAbelianGroup is defined as the abelianization of FreeGroup, so FreeAbelianGroup.equivFinsupp gives the whole thing.

[Laurent Bartholdi]

:tada:

theorem rank_free_abelian_group (α : Type*) : Module.rank ℤ (FreeAbelianGroup α) = Cardinal.mk α := by
  calc
    Module.rank ℤ (FreeAbelianGroup α) = Module.rank ℤ (α →₀ ℤ) :=
      rank_eq_of_equiv_equiv (ZeroHom.id ℤ) (FreeAbelianGroup.equivFinsupp α)
        (Function.Involutive.bijective (congrFun rfl)) (map_zsmul _)
    _ = Cardinal.mk α := by
      rw [rank_finsupp]
      simp only [Cardinal.lift_id', rank_self, Cardinal.lift_one, mul_one]

theorem FreeGroup.unique_rank₂ {F : Type*} {ι₁ ι₂ : Type u} [Group F] :
  FreeGroupBasis ι₁ F → FreeGroupBasis ι₂ F → Cardinal.mk ι₁ = Cardinal.mk ι₂ := by
  intro β₁ β₂
  let abelian_iso := MulEquiv.abelianizationCongr (β₁.repr.symm.trans β₂.repr) |> MulEquiv.toAdditive
  calc
    Cardinal.mk ι₁ = Module.rank ℤ (FreeAbelianGroup ι₁) := (rank_free_abelian_group ι₁).symm
    _ = Module.rank ℤ (FreeAbelianGroup ι₂) := rank_eq_of_equiv_equiv (ZeroHom.id ℤ) abelian_iso
      (Function.Involutive.bijective (congrFun rfl)) (map_zsmul _)
    _ = Cardinal.mk ι₂ := rank_free_abelian_group ι₂

[Junyan Xu]

Shorter versions

import Mathlib

theorem rank_free_abelian_group (α : Type*) : Module.rank ℤ (FreeAbelianGroup α) = Cardinal.mk α := by
  rw [(FreeAbelianGroup.equivFinsupp α).toIntLinearEquiv.rank_eq, rank_finsupp_self, Cardinal.lift_id']

theorem FreeGroup.unique_rank₂ {F : Type*} {ι₁ ι₂ : Type u} [Group F] :
    FreeGroupBasis ι₁ F → FreeGroupBasis ι₂ F → Cardinal.mk ι₁ = Cardinal.mk ι₂ :=
  fun β₁ β₂ ↦ (FreeAbelianGroup.Equiv.ofFreeGroupEquiv <| β₁.repr.symm.trans β₂.repr).cardinal_eq

[Rida Hamadani]

The proof above gave me unsolved goals, so here is a proof of rank_free_abelian_group that worked for me:

import Mathlib

theorem rank_free_abelian_group (α : Type*) : Module.rank ℤ (FreeAbelianGroup α) = Cardinal.mk α :=
  (FreeAbelianGroup.basis α).mk_eq_rank''.symm

[Junyan Xu]

Thanks, I fixed my proof, but your is better!

[Kevin Buzzard]

(deleted)