feat(Group Theory/Presentation): define group presentations#41936
feat(Group Theory/Presentation): define group presentations#41936homeowmorphism wants to merge 5 commits into
Conversation
|
This pull request is now in draft mode. No active bors state needed cleanup. While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like |
🚨 PR Title Needs FormattingPlease update the title to match our commit style conventions. Errors from script: Details on the required title formatThe title should fit the following format:
|
PR summary 5a49e3f7ddImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type (weak) |
|---|---|---|
| 5015 | 1 | exposed public sections |
Current commit 5a49e3f7dd
Reference commit 4608056c77
This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
1a1bc92 to
b48a9df
Compare
tb65536
added
the
LLM-generated
| with finitely many generators and finitely many relators. -/ | ||
| theorem Group.isFinitelyPresented_iff_nonempty_finite_presentation : | ||
| Group.IsFinitelyPresented G ↔ | ||
| ∃ (α ρ : Type) (_ : Finite α) (_ : Finite ρ), Nonempty (Group.Presentation G α ρ) := by |
There was a problem hiding this comment.
You way as well use Set here rather than quantifying over Type.
There was a problem hiding this comment.
I wasn't able to get a nice proof with Set, I think because of the way Presentation is structured it's more natural to quantify over types unless I'm missing something?
There was a problem hiding this comment.
Here's a proof attempt in case it helps. Just feels like the coersion going on here is clunky?
/-- A group is finitely presented if and only if it admits a `Group.Presentation` on a finite
generating family whose relators are indexed by a finite set of words in those generators, which
then indexes itself. -/
theorem Group.isFinitelyPresented_iff_nonempty_finite_presentation :
Group.IsFinitelyPresented G ↔
∃ (S : Set G) (_ : Finite S) (R : Set (FreeGroup S)) (_ : Finite R),
Nonempty (Group.Presentation G S R) := by
constructor
· rintro h
obtain ⟨n, φ, hφ, hker⟩ := h.out
obtain ⟨v, rfl⟩ := FreeGroup.lift.surjective φ
obtain ⟨t, htfin, ht⟩ :
(FreeGroup.lift (Subtype.val : Set.range v → G)).ker.IsFinitelyNormallyGenerated :=
Subgroup.IsFinitelyNormallyGenerated.of_comp_surjective
(π := FreeGroup.map (Set.rangeFactorization v))
(by rwa [FreeGroup.lift_comp_map, Set.rangeFactorization_eq])
(FreeGroup.map_surjective Set.rangeFactorization_surjective)
exact ⟨_, (Set.finite_range v).to_subtype, t, htfin.to_subtype,
⟨{ val := Subtype.val
closure_eq_top := by
rw [Subtype.range_coe, ← FreeGroup.range_lift_eq_closure]
exact MonoidHom.range_eq_top.mpr hφ
rel := Subtype.val
ker_eq_normalClosure := by rw [Subtype.range_coe]; exact ht.symm }⟩⟩
· rintro ⟨S, hS, R, hR, ⟨P⟩⟩
exact P.isFinitelyPresented
…f a lemma Reword the `Group.Presentation` structure and `ker_eq_normalClosure` docstrings for clarity, simplify the `isFinitelyPresented_iff` docstring, and change `presentedGroupEquiv_of` from `theorem` to `lemma`. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
2 participants
Group.Presentationpackages a chosen presentation of a given groupG: a generating family together with relators (wordsr, each read asr = 1) whose generated normal subgroup is exactly the kernel ofFreeGroup.lift val : FreeGroup α →* G. This the complementary toPresentedGroup rels, which constructs the group presented by a set of generators and relations.PR #33233 by @jazzits previously was made to implement this feature but I am making a new PR due to inactivity. I have credited the original author.
Claude Fable assisted heavily in the making on this API, but I have done my best to review and steer it before putting this out.