Commit 2022-03-08 10:54 07980376

View on Github →

refactor(algebra/group/inj_surj): add npow and zpow to all definitions (#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:

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.
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.
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:

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) ℕ