Conversation
YaelDillies
commented
Jan 24, 2025
PR summary 58f4dfcb3c
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Algebra.Group.Hom.Defs | 111 | 112 | +1 (+0.90%) |
| Mathlib.Algebra.GroupWithZero.Hom | 124 | 125 | +1 (+0.81%) |
| Mathlib.Algebra.Group.Equiv.Defs | 126 | 127 | +1 (+0.79%) |
| Mathlib.Algebra.Group.Units.Hom | 138 | 139 | +1 (+0.72%) |
Import changes for all files
| Files | Import difference |
|---|---|
15 filesMathlib.Algebra.Free Mathlib.Algebra.Group.Commute.Hom Mathlib.Algebra.Group.Equiv.Defs Mathlib.Algebra.Group.Ext Mathlib.Algebra.Group.Hom.Basic Mathlib.Algebra.Group.Hom.CompTypeclasses Mathlib.Algebra.Group.Hom.Defs Mathlib.Algebra.Group.Idempotent Mathlib.Algebra.Group.Invertible.Basic Mathlib.Algebra.Group.ModEq Mathlib.Algebra.Group.TypeTags.Hom Mathlib.Algebra.Group.Units.Hom Mathlib.Algebra.GroupWithZero.Equiv Mathlib.Algebra.GroupWithZero.Hom Mathlib.Algebra.GroupWithZero.Idempotent |
1 |
Declarations diff
+ MonoidHom.ofClass
+ MulEquiv.ofClass
+ MulEquiv.ofClass_injective
+ MulHom.coe_ofClass
+ MulHom.ofClass
+ OneHom.coe_ofClass
+ OneHom.ofClass
+ apply_ofClass_symm_apply
+ coe_symm_ofClass
+ coe_toMulEquiv
+ instFunLike
+ instance : Coe (M ≃* N) (M →* N) := ⟨toMonoidHom⟩
+ instance : Coe (α →*o β) (α →* β) := ⟨toMonoidHom⟩
+ instance : Coe (α →ₙ+* β) (α →+ β) := ⟨toAddMonoidHom⟩
+ instance : CoeOut (r ≃r s) (α ≃ β) := ⟨toEquiv⟩
+ isLocalHom_monoidHomOfClass
+ isLocalRingHom_toMonoidHom
+ mapEquiv
+ map_id
+ map_map
+ ofClass_symm
+ ofClass_symm_apply_apply
+ ofClass_symm_comp_self
+ refl_toMonoidHom
+ self_comp_ofClass_symm
+ symm_ofClass
+ symm_toEquiv
+ toEquiv_eq_ofClass
+ toMonoidHom_comp_toMonoidHom_symm
+ toMonoidHom_eq_ofClass
+ toMonoidHom_symm_comp_toMonoidHom
+ toMulHom_eq_ofClass
+ trans_toMonoidHom
++ coe_ofClass
++ ofClass
++ symm_toOrderIso
- EquivLike.toEquiv
- MonoidHom.coe_coe
- MonoidHomClass.toMonoidHom
- MulEquivClass.toMulEquiv_injective
- MulHom.coe_coe
- MulHomClass.toMulHom
- OneHom.coe_coe
- OneHomClass.toOneHom
- RingHomClass.toRingHom
- _root_.EquivLike.apply_coe_symm_apply
- _root_.EquivLike.coe_coe
- _root_.EquivLike.coe_symm_apply_apply
- _root_.EquivLike.coe_symm_comp_self
- _root_.EquivLike.self_comp_coe_symm
- coe_monoidHom_comp_coe_monoidHom_symm
- coe_monoidHom_refl
- coe_monoidHom_symm_comp_coe_monoidHom
- coe_monoidHom_trans
- instance : CoeTC F (α →+* β)
- instance [MonoidHomClass F M N] : CoeTC F (M →* N)
- instance [MulHomClass F M N] : CoeTC F (M →ₙ* N)
- instance [OneHomClass F M N] : CoeTC F (OneHom M N)
- instance {F} [EquivLike F α β] : CoeTC F (α ≃ β)
- isLocalHom_toMonoidHom
- map_apply
- toEquiv_eq_coe
- toMulHom_eq_coe
-- coe_toEquiv_symm
-- toEquiv_symm
-- toMonoidHom_eq_coe
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/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).
4cf814d to
c03f676
Compare
Vierkantor
left a comment
There was a problem hiding this comment.
Overall I agree that the generic hom coercions didn't turn out to be particularly useful, so I would be in favour of the PR.
Could you also check that the documentation on how to set up FunLikes is appropriately updated?
| section coe | ||
|
|
||
| @[to_additive] | ||
| instance : EquivLike (M ≃* N) M N where |
There was a problem hiding this comment.
Isn't this section double with Group/Equiv/Defs.lean?
There was a problem hiding this comment.
Very likely. I seem to have botched a rebase
|
|
||
| /-- Symmetry of multiplication-preserving order isomorphisms -/ | ||
| @[to_additive (attr := symm) "Symmetry of addition-preserving order isomorphisms"] | ||
| def symm (f : α ≃*o β) : β ≃*o α where |
There was a problem hiding this comment.
Surprising that we didn't have this before but it seems to indeed have been the case!
There was a problem hiding this comment.
This ended up being added independently in #22402
|
|
||
| /-- A `≤`-preserving group homomorphism `Γ₀ → Γ'₀` induces a map `Valuation R Γ₀ → Valuation R Γ'₀`. | ||
| -/ | ||
| def map (f : Γ₀ →*₀ Γ'₀) (hf : Monotone f) (v : Valuation R Γ₀) : Valuation R Γ'₀ := |
There was a problem hiding this comment.
Are these changes supposed to be included?
There was a problem hiding this comment.
No indeed, I will fix when I get back to that PR (possibly in a while)
|
I am not touching this PR for a while by lack of time. Feel free to take over if you feel like it! |
c03f676 to
f3abcc1
Compare
f3abcc1 to
3b3673c
Compare
|
This pull request has conflicts, please merge |
3b3673c to
5ec8b43
Compare
|
Please add some explanations to the commit message. |
It's a big issue that this coercion even exists, but it is difficult to remove at the moment, cf #21031.
It's a big issue that this coercion even exists, but it is difficult to remove at the moment, cf #21031. From Toric
It's a big issue that this coercion even exists, but it is difficult to remove at the moment, cf #21031. From Toric
…rover-community#24779) It's a big issue that this coercion even exists, but it is difficult to remove at the moment, cf leanprover-community#21031. From Toric
|
This pull request has conflicts, please merge |
19f923f to
310b04d
Compare
|
This pull request has conflicts, please merge |
310b04d to
878c341
Compare
|
This pull request has conflicts, please merge |
878c341 to
5360aeb
Compare
|
What is the status of this PR? Because this is work that we want to get into Mathlib at some point, but I've been holding off on reviewing because of the empty PR description and WIP tag. |
|
The status is that it needs a lot more work before it's reviewable. I'm expecting the final diff to be around +-3k lines. @j-loreaux suggested preliminary steps to this PR but I am not sure that one can actually take those steps before the whole PR. Concretely, he suggests to first remove uses of hom classes in definitions, and then remove the generic coercions. The issue I see is that this will change the syntactic form of a lot of lemmas, and simp won't yet have been upgraded to handle that. My suggestion instead is to do the refactor one type of morphisms at a time, starting from the leaves of the morphism hierarchy and working towards the roots. |
|
This pull request has conflicts, please merge |
5360aeb to
c44e862
Compare
|
This pull request has conflicts, please merge |
c44e862 to
762fa61
Compare