[Merged by Bors] - feat(GroupTheory/Complement): the equivalence and some corresponding lemmas #6899
Conversation
ChrisHughes24
commented
Aug 31, 2023
ChrisHughes24
commented
ChrisHughes24
added
the
awaiting-review
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
…community/mathlib4 into ComplementGroupChris
There was a problem hiding this comment.
This is fine by me. Would anyone else like to review? @kbuzzard, you seem to know the maths?
| · exact hST.equiv_snd_eq_self_of_mem_of_one_mem h1 | ||
|
|
||
| theorem equiv_fst_eq_one_iff_mem {g : G} (h1 : 1 ∈ S) : | ||
| ((hST.equiv g).fst : G) = 1 ↔ g ∈ T := by |
There was a problem hiding this comment.
Could you have coe in the name somewhere to distinguish from the similar lemma that would talk about equality in the subtype?
There was a problem hiding this comment.
I prefer to leave it, because the coe in the name feels like noise to me, but I'll change it anyway.
I don't think there's a huge amount of maths to need to know here. For context, the motivation is that when defining normal forms for words in the amalgamated product or HNN extension, I need to choose a canonical element of each coset of a subgroup that's involved in some quotient I'm doing. And the canconical element of the subgroup itself has to be one. Mostly I care about the case where one of the sets is a subgroup, but some lemmas are randomly true in other cases. |
| exact Subtype.prop _ | ||
| · exact hST.equiv_fst_eq_self_of_mem_of_one_mem h1 | ||
|
|
||
| theorem equiv_snd_eq_self_iff_mem {g : G} (h1 : 1 ∈ S) : |
There was a problem hiding this comment.
| theorem equiv_snd_eq_self_iff_mem {g : G} (h1 : 1 ∈ S) : | |
| theorem coe_equiv_snd_eq_self_iff_mem {g : G} (h1 : 1 ∈ S) : |
| hST.equiv 1 = (⟨1, hs1⟩, ⟨1, ht1⟩) := by | ||
| rw [Equiv.apply_eq_iff_eq_symm_apply]; simp [equiv] | ||
|
|
||
| theorem equiv_fst_eq_self_iff_mem {g : G} (h1 : 1 ∈ T) : |
There was a problem hiding this comment.
| theorem equiv_fst_eq_self_iff_mem {g : G} (h1 : 1 ∈ T) : | |
| theorem coe_equiv_fst_eq_self_iff_mem {g : G} (h1 : 1 ∈ T) : |
There was a problem hiding this comment.
There's no corresponding lemma without a coe here.
Mathlib/GroupTheory/Complement.lean
Outdated
| theorem leftCosetEquivalence_iff_equiv_fst_eq {g₁ g₂ : G} : | ||
| LeftCosetEquivalence K g₁ g₂ ↔ (hSK.equiv g₁).fst = (hSK.equiv g₂).fst := by |
There was a problem hiding this comment.
I think the LHS is currently simpler than the RHS? What about turning it around and making it a simp lemma?
There was a problem hiding this comment.
I swapped it, but I'm slightly nervous about simplifying away equalities which can be used for simplification elsewhere.
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
|
Thanks! bors r+ |
github-actions
bot
added
ready-to-merge
…lemmas (#6899) Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
