proof ideas

Stream: new members

[Newell Jensen]

I have been having a hard time attacking this proof (sorry'd to save you from having to look at all the failed attempts!).

import Mathlib.GroupTheory.PresentedGroup

variable {α β : Type*} {rels : Set (FreeGroup α)}

@[simp]
def relationsEquiv (e : α ≃ β) : Set (FreeGroup α) ≃ Set (FreeGroup β) :=
  Equiv.Set.congr (FreeGroup.freeGroupCongr e).toEquiv

lemma mapEq (e : α ≃ β) : Subgroup.map (FreeGroup.freeGroupCongr e) (Subgroup.normalClosure rels) =
    Subgroup.normalClosure (relationsEquiv e rels) := by
  sorry -- tried `ext` etc but to no avail

Anyone have any good ideas on how to attack this proof?

Also, does my use of relationsEquiv seem reasonable for pushing through the equivalence of types?

[Riccardo Brasca]

Why not simply using e ''?

[Riccardo Brasca]

Sorry, (freeGroupCongr e) ''

[Riccardo Brasca]

Let me see if I can make some progress

[Newell Jensen]

I didn't try that so, yeah, maybe that will help.

[Riccardo Brasca]

Voilà

import Mathlib

variable {α β : Type*} {rels : Set (FreeGroup α)}

open Subgroup FreeGroup

@[simp]
def relationsEquiv (e : α ≃ β) : Set (FreeGroup α) ≃ Set (FreeGroup β) :=
  Equiv.Set.congr (freeGroupCongr e).toEquiv

lemma mapEq (e : α ≃ β) : (Subgroup.normalClosure rels).map (freeGroupCongr e) =
    Subgroup.normalClosure ((freeGroupCongr e)'' rels) := by
  have : Normal (G := (FreeGroup β)) (map ((freeGroupCongr e)) (Subgroup.normalClosure rels)) := by
    show Normal (map ((freeGroupCongr e).toMonoidHom) (Subgroup.normalClosure rels))
    rw [map_equiv_eq_comap_symm]
    infer_instance
  apply le_antisymm
  · rw [map_le_iff_le_comap]
    apply normalClosure_le_normal
    intro r hr
    simp only [freeGroupCongr_apply, coe_comap, MonoidHom.coe_coe, Set.mem_preimage,
      SetLike.mem_coe]
    apply subset_normalClosure
    simp only [Set.mem_image]
    refine ⟨r, hr, rfl⟩
  · apply Subgroup.normalClosure_le_normal
    simp only [freeGroupCongr_apply, coe_map, MonoidHom.coe_coe, Set.image_subset_iff]
    intro r hr
    simp only [Set.mem_preimage, Set.mem_image, SetLike.mem_coe]
    exact ⟨r, subset_normalClosure hr, rfl⟩

[Riccardo Brasca]

I didn't use relationsEquiv, but I guess the proof is the same.

[Riccardo Brasca]

The main point is docs#Subgroup.normalClosure_le_normal, all the rest is not very difficult

[Newell Jensen]

Thanks!

[Newell Jensen]

I have never used ' ' before but now after all the pain I had ...I won't forget

[Riccardo Brasca]

It's just the image

[Newell Jensen]

I was going to PR this but since you found the proof, feel free

[Riccardo Brasca]

You can use my code, no problem

[Riccardo Brasca]

Anyway we should fix the statement of docs#Subgroup.map_equiv_eq_comap_symm

[Riccardo Brasca]

It contains a weird MulEquiv.toMonoidHom

[Yaël Dillies]

Yeah that's because docs#Subgroup.map and docs#Subgroup.comap take in docs#MonoidHom.

[Riccardo Brasca]

Sure, but if it were a coercion we can apply it directly I think

[Riccardo Brasca]

Like docs#Subring.map_equiv_eq_comap_symm

[Yaël Dillies]

The coercion ought to be syntactically equal though?

[Riccardo Brasca]

Hmm... I want the version that allows to avoid the show line above. Let me see

[Riccardo Brasca]

Something like this

import Mathlib

variable {α β : Type*} {rels : Set (FreeGroup α)}

open Subgroup FreeGroup

@[to_additive]
theorem Subgroup.map_equiv_eq_comap_symm' {G N : Type*} [Group G] [Group N] (f : G ≃* N)
    (K : Subgroup G) : K.map f = K.comap (G := N) f.symm :=
  SetLike.coe_injective (f.toEquiv.image_eq_preimage K)

lemma mapEq (e : α ≃ β) : (Subgroup.normalClosure rels).map (freeGroupCongr e) =
    Subgroup.normalClosure ((freeGroupCongr e)'' rels) := by
  have : Normal (G := (FreeGroup β)) (map ((freeGroupCongr e)) (Subgroup.normalClosure rels)) := by
    rw [map_equiv_eq_comap_symm']
    infer_instance
  apply le_antisymm
  · rw [map_le_iff_le_comap]
    apply normalClosure_le_normal
    intro r hr
    simp only [freeGroupCongr_apply, coe_comap, MonoidHom.coe_coe, Set.mem_preimage,
      SetLike.mem_coe]
    apply subset_normalClosure
    simp only [Set.mem_image]
    refine ⟨r, hr, rfl⟩
  · apply Subgroup.normalClosure_le_normal
    simp only [freeGroupCongr_apply, coe_map, MonoidHom.coe_coe, Set.image_subset_iff]
    intro r hr
    simp only [Set.mem_preimage, Set.mem_image, SetLike.mem_coe]
    exact ⟨r, subset_normalClosure hr, rfl⟩

[Yaël Dillies]

My question is: Are you sure the show was even needed in the first place?

[Riccardo Brasca]

Yes

[Yaël Dillies]

Hmm, that's bad. Where is the coercion (α ≃* β) → (α →* β) defined?

[Riccardo Brasca]

The coercion used by Lean is docs#MonoidHomClass.toMonoidHom

[Riccardo Brasca]

That is not docs#MulEquiv.toMonoidHom

[Riccardo Brasca]

of course they're definitionally equal

[Yaël Dillies]

Ah yes, we still have to decide whether we want to keep those coercions in the first place

[Newell Jensen]

Yaël Dillies said:

Ah yes, we still have to decide whether we want to keep those coercions in the first place

In the time being before this decision is made, for the PR I am putting together, should this include Subgroup.map_equiv_eq_comap_symm'? The main theorem I am proving is the statement PresentedGroup rels ≃* PresentedGroup ((freeGroupCongr e)'' rels) but for generality the above changes probably should go in a new section in Mathlib.GroupTheory.QuotientGroup where Subgroup.map_equiv_eq_comap_symm' could be placed. I can have a lemma in PresentedGroup using the above.

[Eric Wieser]

I think you'd do better to use (freeGroupCongr e.symm ⁻¹' rels) which usually has a better defeq

[Newell Jensen]

Okay, will try that out, thanks.

[Newell Jensen]

In the process of generalizing the code and the below compiles fine by itself:

import Mathlib.GroupTheory.Subgroup.Basic

variable {G G' N : Type*} [Group G] [Group G'] [Group N] {s : Set G}

open Subgroup

@[to_additive]
theorem Subgroup.map_equiv_eq_comap_symm'' (f : G ≃* N) (K : Subgroup G) :
    K.map f = K.comap (G := N) f.symm :=
  SetLike.coe_injective (f.toEquiv.image_eq_preimage K)

theorem normalClosure_map_equiv_eq_normalClosure_comap (f : G ≃* G') :
    (normalClosure s).map f = normalClosure (f '' s) := by
  have : Normal (G := G') (map f (normalClosure s)) := by
    rw [map_equiv_eq_comap_symm']
    infer_instance
  apply le_antisymm
  · rw [map_le_iff_le_comap]
    apply normalClosure_le_normal
    intro r hr
    simp only [coe_comap, MonoidHom.coe_coe, Set.mem_preimage, SetLike.mem_coe]
    apply subset_normalClosure
    simp only [Set.mem_image]
    refine ⟨r, hr, rfl⟩
  · apply Subgroup.normalClosure_le_normal
    simp only [coe_map, MonoidHom.coe_coe, Set.image_subset_iff]
    intro r hr
    simp only [Set.mem_preimage, Set.mem_image, SetLike.mem_coe]
    exact ⟨r, subset_normalClosure hr, rfl⟩

but when I put the associated lemmas in Mathlib.GroupTheory.Subgroup.Basic the infer_instance errors with:

failed to synthesize instance
  Normal (comap (↑(MulEquiv.symm f)) (normalClosure s))

Any ideas?

For added (but probably irrelevant) information I have put normalClosure_map_equiv_eq_normalClosure_comap below the other normalClosure lemmas in Mathlib.GroupTheory.Subgroup.Basic.

Ah, seems that when I put it at the very bottom of the file it compiles fine...will try and find what is causing this!

[Newell Jensen]

@Riccardo Brasca #9185

[Kevin Buzzard]

You can #synth the instance to find out where exactly in the file it is

[Newell Jensen]

@Eric Wieser when you get time for another look #9185

[Newell Jensen]

@Eric Wieser what are your thoughts on what @Thomas Browning said in the conversation for #9185? If possible, I would like to get this PR merged as I have a couple other branches that could be made into PRs that are blocked on this.

Actually, this brings up a question I have for others and what they do when you have multiple dependent PRs? Is there one convention that most contributors use?

[Eric Wieser]

This toMonoidHom vs MonoidHomClass.coe thing is a mess, though obviously not one of your making

[Yaël Dillies]

Mostly my making, but I'm not sure which way we should fix it :sad:

[Newell Jensen]

Yes, understood on that front. What about his second comment for the snippet he provided which would remove the equivalence assumption from the comap lemma?

[Newell Jensen]

Just saw your comment, thanks!

[Newell Jensen]

@Eric Wieser I say we can just do that in a follow up PR then.

[Newell Jensen]

#9403 is an easy extension of #9185 if anyone is up for a review

[Newell Jensen]

#9403 has been awaiting review for 2 weeks now. Is there a better way to get a review besides pinging Zulip (which I did above as well but that didn't seem to help)?

[Kyle Miller]

When I just looked at it, I saw that building failed (and maybe you just restarted CI just now?). Reviewers tend to look through #queue, which excludes PRs with failed builds.

[Bryan Gin-ge Chen]

Hi Newell. Sorry that your PR and messages seem to have been missed. One possible reason your PR hasn't gotten a review is that the latest commit on the PR had a red X, i.e. it wasn't passing CI. I took a look and it seemed to me that the failure was possibly an artifact from when our cache was broken so I've re-triggered the CI job just now. Hopefully your PR will soon pass CI and show up on the reviewers and maintainers' radar.

[Newell Jensen]

I had suspected it might have been the build fail (which as you mentioned was due to the cache issues we faced two weeks ago) that was making it so it wasn't reviewed. Thanks for the verification.

[Newell Jensen]

@Kyle Miller I reverted the last commit but CI is failing on check the cache. I have never seen this before. Do you know if a new CI run needs to be re-triggered or is it something else?

[Kyle Miller]

I'm not sure. Maybe try merging the master branch?

[victoria]

I'm trying to prove lemma vec_in_K by lemmas t1 and t2. The problem is that I do not know how to deal with summation in Lean.

import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Matrix.Reflection
import Mathlib.Data.Matrix.RowCol
import Mathlib.Algebra.BigOperators.Finprod
open BigOperators
open Finset
open Matrix

noncomputable section

def zero_vec(n: ℕ ): Fin n → ℝ := λ x => 0
variable {n m:ℕ} [NeZero m]


def sumK (s : Fin m → NNReal) (v : Fin m → Fin n → ℝ)
:= ∑ i in range m, s i • v i
-- Define K cone 1.2
variable (vmatrix : Fin m → Fin n → ℝ)

def K: Set (Fin n → ℝ) := {x | ∃ s, x = (sumK s vmatrix)}

def s_lambda(i : Fin m): (Fin m) → NNReal:= λ x =>
if x = i then 1 else 0

lemma t1(i: Fin m): (s_lambda i i) • vmatrix i = vmatrix i := by
  ext
  simp [s_lambda]

lemma t2(i: Fin m)(t: Fin m)(h: t ≠ i): (s_lambda i t ) • vmatrix i = zero_vec n:= by
  ext x
  have: s_lambda i t = 0 := by
    ext
    simp [s_lambda]
    by_contra
    apply h
    assumption
  rw[this]
  rw[zero_vec]
  apply zero_mul
-- all column vectors are in the cone
lemma vec_in_K(i': Fin m): vmatrix i' ∈ K vmatrix:= by
  rw[K]
  use s_lambda i'
  unfold sumK
  sorry

[Kevin Buzzard]

Don't mix range m and Fin m, these are two different ways of counting to m-1 and they're not equal.
Try

def sumK (s : Fin m → NNReal) (v : Fin m → Fin n → ℝ)
:= ∑ i : Fin m, s i • v i

instead.

[Kevin Buzzard]

Fin m is a type, and range m is a term.

[victoria]

I've changed range m into Fin m. But I'm still stuck on the proof of the lemma vec_in_K. Should I try something like "cases" here?

[Kevin Buzzard]

You should post a #mwe so we can be stuck at exactly the same point as you

[Jawad Ali]

Hi, i'm new here. i'm facing problem to solve this, anyone please help me to tackle this problem
Screenshot-2024-05-15-023937.png
2+2=4 ? how can I solve this one?
natural number game

[Jawad Ali]

Hi, I am New here, i need your help regarding proving the 2+2=4 ??? how can I tackle this problem?

[Rida Hamadani]

example : 2 + 2 = 4 := rfl

works. Do you mean in the natural numbers game?

[Notification Bot]

A message was moved here from #general > generalize_proofs failed by Kyle Miller.

[Kyle Miller]

@Jawad Ali I moved the context of your question here. (It appears before the message that Rida initially saw.)

[Jawad Ali]

Rida Hamadani said:

example : 2 + 2 = 4 := rfl

works. Do you mean in the natural numbers game?

yes in natural number game

[Jawad Ali]

you can check this SS as well
Screenshot-2024-05-15-023937.png

[Rida Hamadani]

Can you rewrite both sides of the equation as succ(succ(succ(1)))?

[Jawad Ali]

Rida Hamadani said:

Can you rewrite both sides of the equation as succ(succ(succ(1)))?

BTW how can I do that?

[Rida Hamadani]

First, use the lemmas for 4 = succ 3, 3 = succ 2, and 2 = succ 1.
You should end up with succ 1 + succ 1 = succ (succ (succ 1))
After that, you can use the lemma you proved in the previous level.

[Jawad Ali]

Rida Hamadani said:

First, use the lemmas for 4 = succ 3, 3 = succ 2, and 2 = succ 1.
You should end up with succ 1 + succ 1 = succ (succ (succ 1))
After that, you can use the lemma you proved in the previous level.

succ1+succ 1= succ(succ(succ1)) how can I solve this? so sorry for more questions

[Rida Hamadani]

Have you tried add_succ? After that you will only need 1 more step.

[Jawad Ali]

Rida Hamadani said:

Have you tried add_succ? After that you will only need 1 more step.

yes I tried, succ (succ 1 + 1) = succ (succ (succ 1))?

[Rida Hamadani]

That's the equality provided by succ_eq_add_one

[Jawad Ali]

Rida Hamadani said:

That's the equality provided by succ_eq_add_one

still stuck with this problem: succ 1 + 1 + 1 = succ (succ (succ 1))

[Rida Hamadani]

Use the other side of the equality in succ_eq_add_one

[Jawad Ali]

Rida Hamadani said:

Use the other side of the equality in succ_eq_add_one

Finally its done, Thanks you so much
:smile: