[Merged by Bors] - feat(algebra/group/inj_surj): add injective.monoid_pow etc
#10152
Conversation
github-actions
bot
added
the
blocked-by-other-PR
github-actions
bot
removed
the
blocked-by-other-PR
|
🎉 Great news! Looks like all the dependencies have been resolved: 💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
| "A type endowed with `0` and `+` is an additive monoid, | ||
| if it admits an injective map that preserves `0` and `+` to an additive monoid. | ||
| This version takes a custom `nsmul` as a `[has_scalar ℕ M₁]` argument."] | ||
| protected def monoid_pow [has_pow M₁ ℕ] [monoid M₂] (f : M₁ → M₂) (hf : injective f) |
There was a problem hiding this comment.
I would argue we should call this monoid and rename the existing monoid to monoid_default_pow. IMO, in the long run we do not really want to be using the default npow anywhere, meaning with my suggested name we eventually end up with the clearer monoid spelling everywere.
There was a problem hiding this comment.
While I agree that we should do this in the long run, I think that this renaming should be done together with migration of all/most applications to the new API. I would prefer to do this migration on a case by case basis, then search&replace s/monoid_pow/monoid/.
There was a problem hiding this comment.
In particular, I already have branches for ulift and opposite, and I would prefer to merge them before we rename definitions.
groupdoesn't seem particularly special compared to these.
It is special because you can't define ulift.group as { .. ulift.div_inv_monoid, .. ulift.some_other_instance }.
There was a problem hiding this comment.
Thanks, I get the idea behind group then.
I assume the same argument applies to group_with_zero, as that has non-inherited fields?
There was a problem hiding this comment.
Do we not also want to do this for comm_monoid, cancel_monoid, left_cancel_monoid, etc in the same file? group doesn't seem particularly special compared to these.
We certainly needs these definitions in some form, so
bors d+
but I think we probably need to pull off the bandaid and replace all the function.injective.algebraic_structure instances with ones that take {n,z}{pow,smul}; and it might be easiest to do them all at once rather have two versions of each.
|
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
|
bors r+ |
github-actions
bot
added
the
ready-to-merge
Add versions of some constructors that take `pow`/`zpow`/`nsmul`/`zsmul` as explicit arguments. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
injective.monoid_pow etcinjective.monoid_pow etc
Add versions of some constructors that take `pow`/`zpow`/`nsmul`/`zsmul` as explicit arguments. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
#12126) Currently, we have a small handful of helpers to construct algebraic structures via pushforwards and pullbacks that preserve `has_pow` and `has_scalar` instances (added in #10152 and #10832): * `function.{inj,surj}ective.add_monoid_smul` * `function.{inj,surj}ective.monoid_pow` * `function.{inj,surj}ective.sub_neg_monoid_smul` * `function.{inj,surj}ective.div_inv_monoid_smul` * `function.{inj,surj}ective.add_group_smul` * `function.{inj,surj}ective.group_pow` Predating these, we have a very large collection of helpers that construct new `has_pow` and `has_scalar` instances, for all the above and also for every other one-argument algebraic structure (`comm_monoid`, `ring`, `linear_ordered_field`, ...). This puts the user in an awkward position; either: 1. They are unaware of the complexity here, and use `add_monoid_smul` and `add_comm_monoid` within the same file, which create two nonequal scalar instances. 2. They use only the large collection, and don't get definitional control of `has_scalar` and `has_pow`, which can cause typeclass diamonds with generic `has_scalar` instances. 3. They use only the small handful of helpers (which requires remembering which ones are safe to use), and have to remember to manually construct `add_comm_monoid` as `{..add_comm_semigroup, ..add_monoid}`. If they screw up and construct it as `{..add_comm_semigroup, ..add_zero_class}`, then they're in the same position as (1) without knowing it. This change converts every helper in the large collection to _also_ preserve scalar and power instances; as a result, these pullback and pushforward helpers once again no longer construct any new data. As a result, all these helpers now take `nsmul`, `zsmul`, `npow`, and `zpow` arguments as necessary, to indicate that these operations are preserved by the function in question. As a result of this change, all existing callers are now expected to have a `has_pow` or `has_scalar` implementation available ahead of time. In many cases the `has_scalar` instances already exist as a more general case, and maybe just need reordering within the file. Sometimes the general case of `has_scalar` is stated in a way that isn't general enough to describe `int` and `nat`. In these cases and the `has_pow` cases, we define new instance manually. Grepping reveals a rough summary of the new instances: ```lean instance : has_pow (A 0) ℕ instance has_nsmul : has_scalar ℕ (C ⟶ D) instance has_zsmul : has_scalar ℤ (C ⟶ D) instance has_nsmul : has_scalar ℕ (M →ₗ⁅R,L⁆ N) instance has_zsmul : has_scalar ℤ (M →ₗ⁅R,L⁆ N) instance has_nsmul : has_scalar ℕ {x : α // 0 ≤ x} instance has_pow : α // 0 ≤ x} ℕ instance : has_scalar R (ι →ᵇᵃ[I₀] M) instance has_nat_scalar : has_scalar ℕ (normed_group_hom V₁ V₂) instance has_int_scalar : has_scalar ℤ (normed_group_hom V₁ V₂) instance : has_pow ℕ+ ℕ instance subfield.has_zpow : has_pow s ℤ instance has_nat_scalar : has_scalar ℕ (left_invariant_derivation I G) instance has_int_scalar : has_scalar ℤ (left_invariant_derivation I G) instance add_subgroup.has_nsmul : has_scalar ℕ H instance subgroup.has_npow : has_pow H ℕ instance add_subgroup.has_zsmul : has_scalar ℤ H instance subgroup.has_zpow : has_pow H ℤ instance add_submonoid.has_nsmul : has_scalar ℕ S instance submonoid.has_pow : has_pow S ℕ instance : has_pow (special_linear_group n R) ℕ instance : has_pow (α →ₘ[μ] γ) ℕ instance has_int_pow : has_pow (α →ₘ[μ] γ) ℤ instance : div_inv_monoid (α →ₘ[μ] γ) instance has_nat_pow : has_pow (α →ₛ β) ℕ instance has_int_pow : has_pow (α →ₛ β) ℤ instance has_nat_pow : has_pow (germ l G) ℕ instance has_int_pow : has_pow (germ l G) ℤ instance : has_scalar ℕ (fractional_ideal S P) instance has_nat_scalar : has_scalar ℕ (𝕎 R) instance has_int_scalar : has_scalar ℤ (𝕎 R) instance has_nat_pow : has_pow (𝕎 R) ℕ instance has_nat_scalar : has_scalar ℕ (truncated_witt_vector p n R) instance has_int_scalar : has_scalar ℤ (truncated_witt_vector p n R) instance has_nat_pow : has_pow (truncated_witt_vector p n R) ℕ instance has_nat_scalar : has_scalar ℕ (α →ᵇ β) instance has_int_scalar : has_scalar ℤ (α →ᵇ β) instance has_nat_pow : has_pow (α →ᵇ R) ℕ ```
Add versions of some constructors that take
pow/zpow/nsmul/zsmulas explicit arguments.monoid.has_powetc toalgebra.group.defs#10147