chore(linear_algebra/affine_space/affine_map,topology/algebra/continuous_affine_map): generalized scalar instances (#11978)

The main result here is that `distrib_mul_action`s are available on affine maps to a module, inherited from their codomain.

This fixes a diamond in the `int`-action that was already present for `int`-affine maps, and prevents the new `nat`-action introducing a diamond.

This also removes the requirement for `R` to be a `topological_space` in the scalar action for `continuous_affine_map` by using `has_continuous_const_smul` instead of `has_continuous_smul`.

Author: eric-wieser

src/linear_algebra/affine_space/affine_map.lean

@@ -189,7 +189,14 @@ instance : add_comm_group (P1 →ᵃ[k] V2) :=
   zero_add := λ f, ext $ λ p, zero_add (f p),
   add_zero := λ f, ext $ λ p, add_zero (f p),
   add_comm := λ f g, ext $ λ p, add_comm (f p) (g p),
-  add_left_neg := λ f, ext $ λ p, add_left_neg (f p) }
+  add_left_neg := λ f, ext $ λ p, add_left_neg (f p),
+  nsmul := λ n f, ⟨n • f, n • f.linear, λ p v, by simp⟩,
+  nsmul_zero' := λ f, ext $ λ p, add_monoid.nsmul_zero' _,
+  nsmul_succ' := λ n f, ext $ λ p, add_monoid.nsmul_succ' _ _,
+  zsmul := λ z f, ⟨z • f, z • f.linear, λ p v, by simp⟩,
+  zsmul_zero' := λ f, ext $ λ p, sub_neg_monoid.zsmul_zero' _,
+  zsmul_succ' := λ z f, ext $ λ p, sub_neg_monoid.zsmul_succ' _ _,
+  zsmul_neg' := λ z f, ext $ λ p, sub_neg_monoid.zsmul_neg' _ _, }
 
 @[simp, norm_cast] lemma coe_zero : ⇑(0 : P1 →ᵃ[k] V2) = 0 := rfl
 @[simp] lemma zero_linear : (0 : P1 →ᵃ[k] V2).linear = 0 := rfl
@@ -502,36 +509,69 @@ end affine_map
 
 namespace affine_map
 
-variables {k : Type*} {V1 : Type*} {P1 : Type*} {V2 : Type*} [comm_ring k]
-    [add_comm_group V1] [module k V1] [affine_space V1 P1] [add_comm_group V2] [module k V2]
+variables {R k V1 P1 V2 : Type*}
+
+section ring
+variables [ring k] [add_comm_group V1] [affine_space V1 P1] [add_comm_group V2]
+variables [module k V1] [module k V2]
 include V1
 
-/-- If `k` is a commutative ring, then the set of affine maps with codomain in a `k`-module
-is a `k`-module. -/
-instance : module k (P1 →ᵃ[k] V2) :=
+section distrib_mul_action
+variables [monoid R] [distrib_mul_action R V2] [smul_comm_class k R V2]
+
+/-- The space of affine maps to a module inherits an `R`-action from the action on its codomain. -/
+instance : distrib_mul_action R (P1 →ᵃ[k] V2) :=
 { smul := λ c f, ⟨c • f, c • f.linear, λ p v, by simp [smul_add]⟩,
   one_smul := λ f, ext $ λ p, one_smul _ _,
   mul_smul := λ c₁ c₂ f, ext $ λ p, mul_smul _ _ _,
   smul_add := λ c f g, ext $ λ p, smul_add _ _ _,
-  smul_zero := λ c, ext $ λ p, smul_zero _,
-  add_smul := λ c₁ c₂ f, ext $ λ p, add_smul _ _ _,
-  zero_smul := λ f, ext $ λ p, zero_smul _ _ }
+  smul_zero := λ c, ext $ λ p, smul_zero _ }
+
+@[simp] lemma coe_smul (c : R) (f : P1 →ᵃ[k] V2) : ⇑(c • f) = c • f := rfl
+
+@[simp] lemma smul_linear (t : R) (f : P1 →ᵃ[k] V2) : (t • f).linear = t • f.linear := rfl
+
+instance [distrib_mul_action Rᵐᵒᵖ V2] [is_central_scalar R V2] :
+  is_central_scalar R (P1 →ᵃ[k] V2) :=
+{ op_smul_eq_smul := λ r x, ext $ λ _, op_smul_eq_smul _ _ }
+
+end distrib_mul_action
+
+section module
+variables [semiring R] [module R V2] [smul_comm_class k R V2]
 
-@[simp] lemma coe_smul (c : k) (f : P1 →ᵃ[k] V2) : ⇑(c • f) = c • f := rfl
+/-- The space of affine maps taking values in an `R`-module is an `R`-module. -/
+instance : module R (P1 →ᵃ[k] V2) :=
+{ smul := (•),
+  add_smul := λ c₁ c₂ f, ext $ λ p, add_smul _ _ _,
+  zero_smul := λ f, ext $ λ p, zero_smul _ _,
+  .. affine_map.distrib_mul_action }
 
-@[simp] lemma smul_linear (t : k) (f : P1 →ᵃ[k] V2) : (t • f).linear = t • f.linear := rfl
+variables (R)
 
 /-- The space of affine maps between two modules is linearly equivalent to the product of the
 domain with the space of linear maps, by taking the value of the affine map at `(0 : V1)` and the
-linear part. -/
-@[simps] def to_const_prod_linear_map : (V1 →ᵃ[k] V2) ≃ₗ[k] V2 × (V1 →ₗ[k] V2) :=
+linear part.
+
+See note [bundled maps over different rings]-/
+@[simps] def to_const_prod_linear_map : (V1 →ᵃ[k] V2) ≃ₗ[R] V2 × (V1 →ₗ[k] V2) :=
 { to_fun    := λ f, ⟨f 0, f.linear⟩,
   inv_fun   := λ p, p.2.to_affine_map + const k V1 p.1,
   left_inv  := λ f, by { ext, rw f.decomp, simp, },
   right_inv := by { rintros ⟨v, f⟩, ext; simp, },
   map_add'  := by simp,
   map_smul' := by simp, }
 
+end module
+
+end ring
+
+section comm_ring
+
+variables [comm_ring k] [add_comm_group V1] [affine_space V1 P1] [add_comm_group V2]
+variables [module k V1] [module k V2]
+include V1
+
 /-- `homothety c r` is the homothety (also known as dilation) about `c` with scale factor `r`. -/
 def homothety (c : P1) (r : k) : P1 →ᵃ[k] P1 :=
 r • (id k P1 -ᵥ const k P1 c) +ᵥ const k P1 c
@@ -575,4 +615,6 @@ def homothety_affine (c : P1) : k →ᵃ[k] (P1 →ᵃ[k] P1) :=
   ⇑(homothety_affine c : k →ᵃ[k] _) = homothety c :=
 rfl
 
+end comm_ring
+
 end affine_map

src/topology/algebra/continuous_affine_map.lean

@@ -154,21 +154,33 @@ omit W₂
 
 section module_valued_maps
 
-variables {S : Type*} [comm_ring S] [module S V] [module S W]
-variables [topological_space W] [topological_space S] [has_continuous_smul S W]
+variables {S : Type*}
+variables [topological_space W]
 
 instance : has_zero (P →A[R] W) := ⟨continuous_affine_map.const R P 0⟩
 
 @[norm_cast, simp] lemma coe_zero : ((0 : P →A[R] W) : P → W) = 0 := rfl
 
 lemma zero_apply (x : P) : (0 : P →A[R] W) x = 0 := rfl
 
-instance : has_scalar S (P →A[S] W) :=
-{ smul := λ t f, { cont := f.continuous.const_smul t, .. (t • (f : P →ᵃ[S] W)) } }
+section mul_action
+variables [monoid S] [distrib_mul_action S W] [smul_comm_class R S W]
+variables [has_continuous_const_smul S W]
 
-@[norm_cast, simp] lemma coe_smul (t : S) (f : P →A[S] W) : ⇑(t • f) = t • f := rfl
+instance : has_scalar S (P →A[R] W) :=
+{ smul := λ t f, { cont := f.continuous.const_smul t, .. (t • (f : P →ᵃ[R] W)) } }
 
-lemma smul_apply (t : S) (f : P →A[S] W) (x : P) : (t • f) x = t • (f x) := rfl
+@[norm_cast, simp] lemma coe_smul (t : S) (f : P →A[R] W) : ⇑(t • f) = t • f := rfl
+
+lemma smul_apply (t : S) (f : P →A[R] W) (x : P) : (t • f) x = t • (f x) := rfl
+
+instance [distrib_mul_action Sᵐᵒᵖ W] [is_central_scalar S W] : is_central_scalar S (P →A[R] W) :=
+{ op_smul_eq_smul := λ t f, ext $ λ _, op_smul_eq_smul _ _ }
+
+instance : mul_action S (P →A[R] W) :=
+function.injective.mul_action _ coe_injective coe_smul
+
+end mul_action
 
 variables [topological_add_group W]
 
@@ -201,7 +213,14 @@ instance : add_comm_group (P →A[R] W) :=
   .. (coe_injective.add_comm_group _ coe_zero coe_add coe_neg coe_sub :
     add_comm_group (P →A[R] W)) }
 
-instance : module S (P →A[S] W) :=
+instance [monoid S] [distrib_mul_action S W] [smul_comm_class R S W]
+  [has_continuous_const_smul S W] :
+  distrib_mul_action S (P →A[R] W) :=
+function.injective.distrib_mul_action ⟨λ f, f.to_affine_map.to_fun, rfl, coe_add⟩
+  coe_injective coe_smul
+
+instance [semiring S] [module S W] [smul_comm_class R S W] [has_continuous_const_smul S W] :
+  module S (P →A[R] W) :=
 function.injective.module S ⟨λ f, f.to_affine_map.to_fun, rfl, coe_add⟩ coe_injective coe_smul
 
 end module_valued_maps