feat(GroupExtension/Abelian): define conjClassesEquivH1#26670
feat(GroupExtension/Abelian): define conjClassesEquivH1#26670yu-yama wants to merge 6 commits intoleanprover-community:masterfrom
conjClassesEquivH1#26670Conversation
chore: use existing `groupCohomology.cocyclesOfIsMulCocycle₁` def
lint: suppress `linter.directoryDependency` error
chore: add simps lemmas
chore: add ext lemmas to `GroupExtension.{Section,Splitting}`
Comments from Original PR #21837This section contains 3 comment(s) from the original PR, excluding bot comments. @erdOne (2025-06-26 19:51 UTC): @erdOne (2025-06-27 10:59 UTC): @YaelDillies (2025-06-27 12:31 UTC): Yesterday, Edison spent an hour updating this file to v4.19.0. I didn't want his work to be lost, so I rebased this branch and moved over his changes (as well as the ones necessary to go from v4.19.0 to v4.21.0-rc3). That's all. I didn't intend to act on your review, and haven't done so. |
PR summary 5beabdc14eImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
There was a problem hiding this comment.
Why was this lemma removed?
theorem isConj_iff_sub_mem_oneCoboundaries (s₁ s₂ : (toGroupExtension φ).Splitting) :
(toGroupExtension φ).IsConj s₁ s₂ ↔
⇑s₁.toCocycles₁ - s₂.toCocycles₁ ∈ groupCohomology.coboundaries₁ (toRep φ) := by
rw [sub_mem_comm_iff]
apply Additive.ofMul.exists_congr
intro n
rw [funext_iff, funext_iff]
apply forall_congr'
intro g
trans (s₁ g).left = n * (s₂ g).left * (φ g n)⁻¹
· simp [toGroupExtension_inl, SemidirectProduct.ext_iff, right_splitting]
rw [eq_mul_inv_iff_mul_eq, mul_comm, ← eq_mul_inv_iff_mul_eq, mul_assoc, mul_comm,
← mul_inv_eq_iff_eq_mul]
simp only [← div_eq_mul_inv, Splitting.toCocycles₁, Pi.sub_apply]
rfl
I think you should still show equiv to H1 instead of that thing, and the proof is something like (with the lemma above)
def conjClassesEquivH1' : (toGroupExtension φ).ConjClasses ≃ groupCohomology.H1 (toRep φ) := by
refine .ofBijective (Quotient.lift (H1π _ ∘ Splitting.equivCocycles₁) ?_) ⟨?_, ?_⟩
· intro a b H
exact (groupCohomology.H1π_eq_iff _ _).mpr <| (isConj_iff_sub_mem_oneCoboundaries ..).mp H
· exact Quotient.ind₂ fun a b H ↦ Quotient.sound <|
(isConj_iff_sub_mem_oneCoboundaries ..).mpr <| (groupCohomology.H1π_eq_iff _ _).mp H
· exact Quotient.lift_surjective _ _ (((ModuleCat.epi_iff_surjective ..).mp inferInstance).comp
Splitting.equivCocycles₁.surjective)
|
This pull request has conflicts, please merge |
This PR continues the work from #21837.
Original PR: #21837