[Merged by Bors] - feat(Algebra/Group): some API lemmas for powMonoidHom#36458
[Merged by Bors] - feat(Algebra/Group): some API lemmas for powMonoidHom#36458MichaelStollBayreuth wants to merge 13 commits intoleanprover-community:masterfrom
Conversation
PR summary 7d8e8ab565
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Algebra.Group.Subgroup.Ker | 411 | 412 | +1 (+0.24%) |
Import changes for all files
| Files | Import difference |
|---|---|
9 filesMathlib.Algebra.Group.Graph Mathlib.Algebra.Group.Subgroup.Ker Mathlib.GroupTheory.Coprod.Basic Mathlib.GroupTheory.FreeGroup.Basic Mathlib.GroupTheory.FreeGroup.IsFreeGroup Mathlib.GroupTheory.FreeGroup.Orbit Mathlib.GroupTheory.FreeGroup.Reduce Mathlib.GroupTheory.NoncommCoprod Mathlib.GroupTheory.Subgroup.Saturated |
1 |
Declarations diff
+ map_range_powMonoidHom
+ mulEquivPiModRangePowMonoidHom
+ mulEquivPiModRangePowMonoidHom_apply
+ range_castAddHom
+ range_eq_top
+ range_nsmulAddMonoidHom
+ subgroupOf_map_powMonoidHom_eq_range
- Int.range_castAddHom
You can run this locally as follows
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./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).
| /-- The multiplication-by-`n` map commutes with isomorphisms. -/] | ||
| lemma powMonoidHom_comm (e : M ≃* N) (n : ℕ) : | ||
| (e : M →* N).comp (powMonoidHom n) = (powMonoidHom n).comp e := by | ||
| ext1 |
There was a problem hiding this comment.
I think we should just use ext, so not to suggest that we need a particular depth.
| ext1 | |
| ext |
There was a problem hiding this comment.
I thought ext1 is more efficient as it doesn't have to check whether further extensionality lemmas can be applied after the first. Are there guidelines regarding this?
There was a problem hiding this comment.
Following the discussion on Zulip (#mathlib4 > ext1 vs. ext @ 💬) I have now changed ext1 to ext : 1.
@Vierkantor Is this OK for you now? I'd like to get this in; I have a follow-up PR that depends on it...
Vierkantor
added
the
awaiting-author
|
@Vierkantor Thanks! I've implemented your suggestions except |
MichaelStollBayreuth
removed
the
awaiting-author
| map and the product of the quotients by the images of the multiplication-by-`n` maps | ||
| on the factors. -/ ] | ||
| noncomputable | ||
| def mulEquivPiModRangePowMonoidHom {ι : Type*} (A : ι → Type*) [∀ i, CommGroup (A i)] (n : ℕ) : |
There was a problem hiding this comment.
Can you add a small API around this definition? Also, I wonder if it can generalized to a product of morphisms in a useful way.
There was a problem hiding this comment.
What kind of API lemmas are you thinking of?
The point here is that powMonoidHom n is a "universal" endomorphism of abelian groups.
To generalize this, one needs to
- define the "product MonoidHom"
((i : ι) → (A i →* B i)) → (((i : ι) → A i) →* ((i : ι) → B i)), which doesn't seem to be there yet; - prove the general result (with the range of the product hom in the quotient on the left);
- show that the product hom of
powMonoidHom nis againpowMonoidHom n; - deduce the definition as given.
While I agree that this could be useful, it smells a bit of mission creep. I could add a TODO.
There was a problem hiding this comment.
The generalization is maybe too long for this PR, but the API saying what the map actually does on classes should be easy.
There was a problem hiding this comment.
OK; I'll add _apply and lemmas (made _apply_applysimp).
By now I also have code for the generalization (~50 lines); I'll make another PR for that after this is merged.
(The _apply_apply lemma is proved by simp using _apply, so should not be necessary.)
This adds a few lemmas about `powMonoidHom`/`nsmulAddMonoidHom` and one convenience lemma that says that the range (as a `MonoidHom`/`AddMonoidHom`) of a `MulEquiv`/`AddEquiv` is the top subobject. It also defines the isomorphism `((i : ι) → A i) ⧸ (powMonoidHom n).range ≃* ((i : ι) → A i ⧸ (powMonoidHom n).range)` and its additive version.
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
…munity#36458) This adds a few lemmas about `powMonoidHom`/`nsmulAddMonoidHom` and one convenience lemma that says that the range (as a `MonoidHom`/`AddMonoidHom`) of a `MulEquiv`/`AddEquiv` is the top subobject. It also defines the isomorphism `((i : ι) → A i) ⧸ (powMonoidHom n).range ≃* ((i : ι) → A i ⧸ (powMonoidHom n).range)` and its additive version.
5 participants
This adds a few lemmas about
powMonoidHom/nsmulAddMonoidHomand one convenience lemma that says that the range (as aMonoidHom/AddMonoidHom) of aMulEquiv/AddEquivis the top subobject.It also defines the isomorphism
((i : ι) → A i) ⧸ (powMonoidHom n).range ≃* ((i : ι) → A i ⧸ (powMonoidHom n).range)and its additive version.