Group presentation hom injective

Stream: new members

[Newell Jensen]

I want to show that the homomorphism I have for the quotient group of the free group modulo the normal closure of the relations is injective but I am having some difficulties. I tried doing it similar to kerLift in QuotientGroup but couldn't since the normal closure is a only subgroup of the kernel (from what we know at this point) . Actually, the whole point of doing this injective proof is so that I can use it to prove that the normal closure is equal to the kernel of the hom between the free group and Dihedral group (the lift of genMap). I have code for everything else but left it out to keep #mwe a reasonable size.

In addition to trying some form of induction similar to kerLift, I also tried doing by rcases on the terms of DihedralPresentedGroup but this ended up giving me some Setoids and Quot.mk. For these types, I also tried using an appropriate induction theorem similar to what kerLift, but to no avail. Below I have the start of proof by contradiction which I was hoping I could continue on if the other aforementioned ideas are not a better course of action, however I am not even sure how to proceed beyond what I have. I have been looking at cosets but no good ideas at the moment. One may be remiss to not have an informal proof in hand before venturing forward on this but I have looked through multiple textbooks and haven't found any good examples as they just brush over these details (for group presentations). Either that, or I am more dense than I care to believe. I feel like I am starting to run out of ideas and looking for suggestions.

Here is an #mwe:

import Mathlib.GroupTheory.PresentedGroup
import Mathlib.GroupTheory.SpecificGroups.Dihedral

-- set_option maxHeartbeats 10000000

namespace DihedralGroup

@[simp]
theorem r_inv_eq_r_neg {i : ZMod n} : (r i)⁻¹ = r (-i) := rfl

@[simp]
theorem r_one_zpow (n : ℕ) (i : ℤ) :
    r (1 : ZMod n) ^ i = r i := by
  obtain ⟨j, hj⟩ := i.eq_nat_or_neg
  rcases hj with rfl | rfl
  · simp only [zpow_coe_nat, r_one_pow, Int.cast_ofNat]
  · simp only [zpow_neg, zpow_coe_nat, r_one_pow, Int.cast_neg, Int.cast_ofNat, r_inv_eq_r_neg]

@[simp]
theorem r_z_pow_n {i : ZMod n} [NeZero n] : r i ^ n = 1 := by
  have h1 : r 1 ^ i.val = r i := by
    simp only [r_one_pow, r.injEq]
    exact ZMod.nat_cast_zmod_val i
  have h2 : (r 1 ^ i.val) ^ n = r 1 ^ (i.val * n) := by
    exact Eq.symm (pow_mul (r 1 : DihedralGroup n) i.val n)
  have h3 : (r 1) ^ (i.val * n) = (1 : DihedralGroup n) := by
    simp only [r_one_pow, Nat.cast_mul, ZMod.nat_cast_val, ZMod.cast_id',
      id_eq, CharP.cast_eq_zero, mul_zero, one_def]
  rw [← h1, h2, h3]

end DihedralGroup

open DihedralGroup

namespace DihedralPresentedGroup

inductive generator (n : ℕ)
  | a : generator n
  | b : generator n

def genMap (n : ℕ) : generator n → DihedralGroup n
  | generator.a => sr 1
  | generator.b => sr 1 * r 1

/-- Presentation ⟨a, b | a² = 1, b² = 1, (a * b)ⁿ = 1⟩  -/
def Rels (n : ℕ) : Set (FreeGroup (generator n)) :=
  {FreeGroup.of generator.a * FreeGroup.of generator.a} ∪
  {FreeGroup.of generator.b * FreeGroup.of generator.b} ∪
  {(FreeGroup.of generator.a * FreeGroup.of generator.b) ^ n}

@[simp] abbrev DihedralPresentedGroup (n : ℕ) := PresentedGroup <| Rels n
@[simp] abbrev KerQuotClosure (n : ℕ) := Subgroup.map (QuotientGroup.mk'
  (Subgroup.normalClosure (Rels n))) (MonoidHom.ker (FreeGroup.lift (genMap n)))
@[simp] abbrev FreeGroupQuotLift (n : ℕ) :=
  FreeGroup (generator n) ⧸ MonoidHom.ker (FreeGroup.lift (genMap n))

def genHom (n : ℕ) : FreeGroupQuotLift n →* DihedralGroup n :=
  QuotientGroup.kerLift <| FreeGroup.lift (genMap n)

theorem injective_genHom : Function.Injective <| genHom n :=
  QuotientGroup.kerLift_injective <| FreeGroup.lift (genMap n)

theorem surjective_genHom : Function.Surjective <| genHom n := by
  let a : FreeGroup (generator n) := FreeGroup.of generator.a
  let b : FreeGroup (generator n) := FreeGroup.of generator.b
  intro g
  rcases g with i | i
  · use (a * b) ^ (i : ℤ)
    simp [genHom, genMap]
  · use a * (a * b) ^ (i - 1 : ℤ)
    simp [genHom, genMap]

theorem bijective_genHom : Function.Bijective <| genHom n :=
  ⟨injective_genHom, surjective_genHom⟩

noncomputable
def FreeGroupQuotLift_eq_DihedralGroup : FreeGroupQuotLift n ≃* DihedralGroup n :=
  MulEquiv.ofBijective (genHom n) (bijective_genHom)

@[simp]
theorem genHom' (n : ℕ) : DihedralPresentedGroup n →* DihedralGroup n :=
    PresentedGroup.toGroup (f := genMap n) <| by
  intro r hr
  rw [Rels] at hr
  simp only [Set.union_singleton, Set.mem_singleton_iff, Set.mem_insert_iff] at hr
  rcases hr with hr₁ | hr₂ | hr₃
  · rw [hr₁]
    simp only [map_pow, map_mul, FreeGroup.lift.of]
    simp_rw [genMap]
    simp only [sr_mul_r, add_zero, sr_mul_sr, sub_self, add_sub_cancel]
    cases' n with n
    · simp only [Nat.zero_eq, pow_zero]
    · exact r_z_pow_n
  · rw [hr₂]
    simp only [map_mul, FreeGroup.lift.of, genMap]
    simp only [sr_mul_r, sr_mul_sr, sub_self, one_def]
  · rw [hr₃]
    simp only [map_mul, FreeGroup.lift.of, genMap]
    simp only [sr_mul_sr, sub_self, one_def]

lemma a_relsGenMap : (genMap n generator.a) * (genMap n generator.a) = (1 : DihedralGroup n) := by
  rw [genMap]; split
  · simp only [sr_mul_sr, sub_self, one_def]
  · simp only [sr_mul_r, sr_mul_sr, sub_self, one_def]

lemma b_relsGenMap : (genMap n generator.b) * (genMap n generator.b) = (1 : DihedralGroup n) := by
  rw [genMap]; split
  · simp only [sr_mul_sr, sub_self, one_def]
  · simp only [sr_mul_r, sr_mul_sr, sub_self, one_def]

lemma a_b_relsGenMap
    : ((genMap n generator.a) * (genMap n generator.b)) ^ n = (1 : DihedralGroup n) := by
  simp_rw [genMap]
  simp only [sr_mul_r, sr_mul_sr, add_sub_cancel]
  cases n with
  | zero => simp only [Nat.zero_eq, pow_zero]
  | succ n => simp only [r_z_pow_n]

theorem one_of_Rels : ∀ r ∈ Rels n, FreeGroup.lift (genMap n) r = 1 := by
  intro r hr
  simp only [Rels] at hr
  simp only [Set.union_singleton, Set.mem_singleton_iff, Set.mem_insert_iff] at hr
  rcases hr with hr₁ | hr₂ | hr₃
  · rw [hr₁]
    simp only [map_pow, map_mul, FreeGroup.lift.of, a_b_relsGenMap]
  · rw [hr₂]
    simp only [map_mul, FreeGroup.lift.of, b_relsGenMap]
  · rw [hr₃]
    simp only [map_mul, FreeGroup.lift.of, a_relsGenMap]

theorem injective_genHom' : Function.Injective <| genHom' n := by
  rw [injective_iff_map_eq_one (genHom' n)]
  intro x h
  by_contra H
  sorry

-- This gives term of type : Subgroup.normalClosure rels ≤ MonoidHom.ker (↑FreeGroup.lift f)
-- (PresentedGroup.closure_rels_subset_ker (@one_of_Rels n))

end DihedralPresentedGroup

[Newell Jensen]

Since nobody has replied, maybe it is best that I put the entire branch up in a PR and put it as WIP and Help Wanted for the last sorry?

[Kevin Buzzard]

I tried to read your code on my phone this morning but when I realised I'd ploughed through a bunch of it and wasn't even half way through I gave up. Is there a way to summarise the question for busy people?

[Newell Jensen]

To summarize I am just completely stuck on the injective proof that is sorry'd. In the message I tried to convey what I had already tried, to show that I have at least put the effort in before asking for help and to give an idea of what I had been attempting. Where I ended up was trying to construct a proof by contradiction of some sort since if the kernel of the hom is not injective this would mean that there would be a coset of the normal closure that maps to the identity in the Dihedral group which means that some other relation exists that was not taken into account.

[Newell Jensen]

That is also why I mentioned putting it in a PR and labeling help wanted, as it might take more time than a quick pass. This is the last theorem I need, as I already have everything else.

[Kevin Buzzard]

What's the maths statement?

[Newell Jensen]

Of the branch? $\langle a, b\ |\ a^2 = 1, b^2 = 1, (a * b) ^ n = 1 \rangle \cong D_n$.

[Kevin Buzzard]

And what's the maths proof? That looks tricky to me.

[Kevin Buzzard]

I can see the map and it's obviously a surjection but why is it an injection mathematically?

[Kevin Buzzard]

I would be tempted to write down an inverse explicitly and then it's a bit of a grind to prove it's a group hom but that would get you over the line.

[Julian Külshammer]

One standard maths proof would count elements after showing it is a surjection.

[Kevin Buzzard]

How do you count the elements in a finitely presented group? I guess there's no algorithm in general but here you're just saying "well a^2=1 and b^2=1 so every element is either abababab...a or abababab...b or bababa...a or bababab...b". Now what though? Looks like things could get messy (even stating what I just wrote there in Lean sounds pretty horrible) :-/

[Kevin Buzzard]

@Newell Jensen so are you saying that you posted a whole bunch of Lean code but actually your question was just a maths question?

[Newell Jensen]

@Kevin Buzzard no, not that I think. The group presentation is isomorphic to the Dihedral group (the texbooks teach us this) and therefore the hom must be injective (assuming you have the proper mapping of course). Thus, I wanted to see how to do it in lean. It sould be possible and this was stumping me and when I can't figure something I like to try and understand why.

[Patrick Massot]

See Kevin? He already had a math proof: "the Textbooks teach us this".

[Kevin Buzzard]

Do we have a tactic for that?

[Newell Jensen]

My point is, I think this should be possible in lean and I would like to see how to do it is all.

[Patrick Massot]

Kevin Buzzard said:

Do we have a tactic for that?

Sure, it's spelled 's', 'o', 'r', 'r', 'y'.

[Kevin Buzzard]

Right, but Lean doesn't do magic: if you don't know the maths proof then Lean isn't going to solve it for you. Your question is a maths question, not a Lean question (yet)

[Newell Jensen]

Point taken, will see if I can figure this out. Cheers.

[Kevin Buzzard]

Some suggestions have been made above but both of them look pretty painful to me right now (although once this is done I think it would be a nice result to put in the library)

[Newell Jensen]

Yes, thanks for the suggestions. I appreciate it.

[Kevin Buzzard]

First you need a paper proof with no gaps -- that's your strategy for the Lean proof.

[Kevin Buzzard]

and you might want to choose wisely :-)

[Patrick Massot]

Joking aside, this is a very deep fundamental laws of formalized mathematics as it exists today (as opposed to dreams of AI that don't exist yet): you need to understand why something is true before formalizing it. Somewhat fuzzy understanding could be enough, but you need some kind of understanding.

[Johan Commelin]

Yes, and we need to work hard on changing that, I think. But that's a really hard problem. I want to get to a point where you can bring your math problem to Lean, and work on solving it in Lean.

[Yaël Dillies]

To be quite honest, this is how I use Lean sometimes. In my LeanAPAP project, I am following a long paper proof whose parts are written to a varying degree of precision.

[Yaël Dillies]

I take each statement, then try formalising it. If I get stuck, I read a bit more of the proof. If I get stuck, I ask Thomas Bloom to expand a bit more.

[Patrick Massot]

This is why I wrote "somewhat fuzzy understanding could be enough". I'm sure you still roughly understand what is going on.

[Yaël Dillies]

Eh, sometimes :grinning:

[Kevin Buzzard]

Martin Escardo, who works in higher type theory, told me that he uses Agda like an electronic blackboard for experimentation. Here we have a situation where the fundamental objects he's working with (infinity groupoids) are so complex that he appreciates being able to use the prover to manage what is going on. But I'm not sure I've experienced this myself yet (although I have experienced this when using computer algebra packages do to clarifying calculations).

[Newell Jensen]

Was able to prove the hom is surjective...now let's see if I can find a counting argument...

[Newell Jensen]

But I did that just to see if I could...seems like an inverse map like Kevin suggested is probably my best bet.

[Kevin Buzzard]

The issue with that is that the definition of D_n in Lean is "either a rotation or a reflection" so you say where the rotations go, you say where the reflections go, and now to check it's a group hom you need to check it preserves multiplication and there will be 4 cases. I guess it's not that bad at the end of the day.

[Julian Külshammer]

It seems the easier way to make the argument work is to first prove the isomorphism of your presentation with the presentation $\langle r,s| r^n=s^2=1, rsr=s\rangle$ and then use the counting argument or directly prove the isomorphism with the Dn in mathlib, see e.g. https://math.stackexchange.com/q/1019593/15416

[Kevin Buzzard]

The arguments there all seem to be of the form "the textbooks teach us the standard presentation and now given another presentation we can manipulate it to get the presentation we want". So this technique changes the goal into proving that some other presentation gives the right answer and in some sense this is the hard part, because the definition in mathlib is not via a presentation.

Concretely, the standard presentation r^n=s^2=(rs)^2=1 certainly also maps to our D_n, but now what? We still have to either write down an inverse or count. I'm not convinced that either problem is substantially easier than before. As far as I can see, counting involves defining an algorithm to put the element of the finitely presented group into a normal form, whatever presentation you use. That's the sort of thing a computer scientist might enjoy but not me. Writing down the inverse function will still involve the case split and hence the four cases when proving it's a group hom but it's still looking to me like this is the cheaper option and here the change of presentation doesn't buy you anything, it just changes the calculations rather than making them any easier. Am I missing something?

[Julian Külshammer]

The counting seems easier in the standard presentation since you don't count sets of alternating words but instead words of the form $r^i s^j$. You are probably right that just writing down the map is preferable.

[Kevin Buzzard]

Aah how about this: for the counting argument you just have to write down an explicit set of reps and then prove by induction on word length that you have everything, which just boils down to checking that the identity is in and that the set of reps is closed under multiplication on the right by the generators. Again you have four cases because the coset reps are of two kinds and there are two generators. And here you're right Julian in that the standard presentation will be easier to work with because the coset reps are a bit nicer.

[Siddhartha Gadgil]

I don't know what definition of the dihedral group you use, but I would try to prove isomorphism by constructing the reverse homomorphim and checking both compositions are the identity (by checking on generators).

[Kevin Buzzard]

The definition in lean is just an inductive type docs#DihedralGroup .

[Kalle Kytölä]

I don't notice that anyone mentioned what I view as the standard argument --- apologies if I missed something (I only did a cursory read). The standard argument is especially nice for the dihedral group which has an "obvious" 2-dimensional faithful representation. That argument involves checking distinctness of 2-by-2 matrices, rather than distinctness of elements of a something abstract (a quotient).

The group $D_n$ is defined by some generators and relations (so quotient of free group), for example $\langle r, m \; | \; m^2 = 1, r^n = 1, r m r m = 1 \rangle$. By the relations one first indeed needs to combinatorially show that any element can be reduced to one of $2n$ words (say $m^b r^j$ with $b \in \{0,1\}$, $j \in \{0,1,\ldots, n-1\}$). The mathematically "nontrivial" task, then, is to show that these words are distict group elements. For that, note that the (universal property of the) quotient construction exactly tells how to construct homomorphisms from the group, so by just verifying that the $2 \times 2$ matrices

$$M = \left[ \begin{array}{cc} 1 & 0 \\ 0 & -1 \end{array} \right] \qquad R = \left[ \begin{array}{cc} \cos(2\pi/n) & -\sin(2\pi/n) \\ \sin(2\pi/n) & \cos(2\pi/n) \end{array} \right]$$

satisfy $M^2 = \mathbf{1}$, $R^n = \mathbf{1}$, $R M R M = \mathbf{1}$, one gets a homomorphism $D_n \to \mathrm{GL}_2(\R)$. Now it is trivial to write down the images of the $2n$ elements: $m^b r^j \mapsto M^b R^j$. These are 2-by-2 matrices that are easy to show distinct (ok, you may need to know that $\theta \mapsto (\cos(\theta),\sin(\theta))$ is injective on $[0,2\pi)$, and you might want to write down the determinants, but still, comparisons of explicit $2 \times 2$ matrices).

[Kevin Buzzard]

The issue here is that lean's D_n is not defined by generators and relations.

[Kalle Kytölä]

Oh, that never crossed my mind! (Clearly I didn't really read the thread...) Sorry!

But I still think surprisingly many textbooks omit the counting argument.

[Kalle Kytölä]

There is work on Coxeter groups being done now, right? (Another thread.) Shouldn't we change the definition of dihedral group to match, then? Those will surely be generators and relations constructions, right?

[Newell Jensen]

@Kalle Kytölä yes, that is why I am working on this branch (to show that the Coxeter group for $n=2$ is equal to the presentation I have here).

[Junyan Xu]

I don't think we should define docs#ZMod as Z/nZ, so for the same reason I don't think we should change the definition of dihedral group. Concrete types and efficient operations are great for computations.

[Kevin Buzzard]

On the other hand, adding to mathlib the isomorphism would almost certainly be a welcome PR.

[Newell Jensen]

Junyan Xu said:

I don't think we should define docs#ZMod as Z/nZ, so for the same reason I don't think we should change the definition of dihedral group. Concrete types and efficient operations are great for computations.

No plans on my side to do that. You are probably referring to what @Kalle Kytölä mentioned.

[Kalle Kytölä]

The efficiency of computation did not occur to me, although I very much like the idea that dihedral groups will be computable (hopefully also in practice!) in Mathlib. Thanks for pointing that out, @Junyan Xu!

So given the Mathlib definition, the counting argument purely in terms of combinatorial objects indeed seems better, and the faithful representation counting argument does not look optimal (it is still one quite reasonable way to count and could be used for injectivity, just not the most direct way given Mathlib definition).