feat(data/pi): provide pi.mul_single (#11849)

the additive version was previously called `pi.single`, to this requires refactoring existing code.



Co-authored-by: Vierkantor <vierkantor@vierkantor.com>

Author: nomeata

src/algebra/group/pi.lean

@@ -172,51 +172,62 @@ open pi
 
 variables (f)
 
-/-- The zero-preserving homomorphism including a single value
+/-- The one-preserving homomorphism including a single value
 into a dependent family of values, as functions supported at a point.
 
-This is the `zero_hom` version of `pi.single`. -/
-@[simps] def zero_hom.single [Π i, has_zero $ f i] (i : I) : zero_hom (f i) (Π i, f i) :=
-{ to_fun := single i,
-  map_zero' := single_zero i }
+This is the `one_hom` version of `pi.mul_single`. -/
+@[to_additive zero_hom.single "The zero-preserving homomorphism including a single value
+into a dependent family of values, as functions supported at a point.
 
-/-- The additive monoid homomorphism including a single additive monoid
-into a dependent family of additive monoids, as functions supported at a point.
+This is the `zero_hom` version of `pi.single`.", simps]
+def one_hom.single [Π i, has_one $ f i] (i : I) : one_hom (f i) (Π i, f i) :=
+{ to_fun := mul_single i,
+  map_one' := mul_single_one i }
 
-This is the `add_monoid_hom` version of `pi.single`. -/
-@[simps] def add_monoid_hom.single [Π i, add_zero_class $ f i] (i : I) : f i →+ Π i, f i :=
-{ to_fun := single i,
-  map_add' := single_op₂ (λ _, (+)) (λ _, zero_add _) _,
-  .. (zero_hom.single f i) }
+/-- The monoid homomorphism including a single monoid into a dependent family of additive monoids,
+as functions supported at a point.
+
+This is the `monoid_hom` version of `pi.mul_single`. -/
+@[to_additive "The additive monoid homomorphism including a single additive
+monoid into a dependent family of additive monoids, as functions supported at a point.
+
+This is the `add_monoid_hom` version of `pi.single`.", simps]
+def monoid_hom.single [Π i, mul_one_class $ f i] (i : I) : f i →* Π i, f i :=
+{ map_mul' := mul_single_op₂ (λ _, (*)) (λ _, one_mul _) _,
+  .. (one_hom.single f i) }
 
 /-- The multiplicative homomorphism including a single `mul_zero_class`
 into a dependent family of `mul_zero_class`es, as functions supported at a point.
 
 This is the `mul_hom` version of `pi.single`. -/
 @[simps] def mul_hom.single [Π i, mul_zero_class $ f i] (i : I) : mul_hom (f i) (Π i, f i) :=
 { to_fun := single i,
-  map_mul' := single_op₂ (λ _, (*)) (λ _, zero_mul _) _, }
+  map_mul' := pi.single_op₂ (λ _, (*)) (λ _, zero_mul _) _, }
 
 variables {f}
 
-lemma pi.single_add [Π i, add_zero_class $ f i] (i : I) (x y : f i) :
-  single i (x + y) = single i x + single i y :=
-(add_monoid_hom.single f i).map_add x y
+@[to_additive]
+lemma pi.mul_single_mul [Π i, mul_one_class $ f i] (i : I) (x y : f i) :
+  mul_single i (x * y) = mul_single i x * mul_single i y :=
+(monoid_hom.single f i).map_mul x y
 
-lemma pi.single_neg [Π i, add_group $ f i] (i : I) (x : f i) :
-  single i (-x) = -single i x :=
-(add_monoid_hom.single f i).map_neg x
+@[to_additive]
+lemma pi.mul_single_inv [Π i, group $ f i] (i : I) (x : f i) :
+  mul_single i (x⁻¹) = (mul_single i x)⁻¹ :=
+(monoid_hom.single f i).map_inv x
 
-lemma pi.single_sub [Π i, add_group $ f i] (i : I) (x y : f i) :
-  single i (x - y) = single i x - single i y :=
-(add_monoid_hom.single f i).map_sub x y
+@[to_additive]
+lemma pi.single_div [Π i, group $ f i] (i : I) (x y : f i) :
+  mul_single i (x / y) = mul_single i x / mul_single i y :=
+(monoid_hom.single f i).map_div x y
 
 lemma pi.single_mul [Π i, mul_zero_class $ f i] (i : I) (x y : f i) :
   single i (x * y) = single i x * single i y :=
 (mul_hom.single f i).map_mul x y
 
-lemma pi.update_eq_sub_add_single [Π i, add_group $ f i] (g : Π (i : I), f i) (x : f i) :
-  function.update g i x = g - single i (g i) + single i x :=
+@[to_additive update_eq_sub_add_single]
+lemma pi.update_eq_div_mul_single [Π i, group $ f i] (g : Π (i : I), f i) (x : f i) :
+  function.update g i x = g / mul_single i (g i) * mul_single i x :=
 begin
   ext j,
   rcases eq_or_ne i j with rfl|h,

src/algebra/group/to_additive.lean

@@ -202,6 +202,7 @@ meta def tr : bool → list string → list string
 | is_comm ("one" :: "lt" :: s)        := add_comm_prefix is_comm "pos"       :: tr ff s
 | is_comm ("le" :: "one" :: s)        := add_comm_prefix is_comm "nonpos"    :: tr ff s
 | is_comm ("lt" :: "one" :: s)        := add_comm_prefix is_comm "neg"       :: tr ff s
+| is_comm ("mul" :: "single" :: s)    := add_comm_prefix is_comm "single"    :: tr ff s
 | is_comm ("mul" :: "support" :: s)   := add_comm_prefix is_comm "support"   :: tr ff s
 | is_comm ("mul" :: "indicator" :: s) := add_comm_prefix is_comm "indicator" :: tr ff s
 | is_comm ("mul" :: s)                := add_comm_prefix is_comm "add"       :: tr ff s

src/data/pi.lean

@@ -85,65 +85,80 @@ instance has_mul [∀ i, has_mul $ f i] :
 section
 
 variables [decidable_eq I]
-variables [Π i, has_zero (f i)] [Π i, has_zero (g i)] [Π i, has_zero (h i)]
+variables [Π i, has_one (f i)] [Π i, has_one (g i)] [Π i, has_one (h i)]
 
-/-- The function supported at `i`, with value `x` there. -/
-def single (i : I) (x : f i) : Π i, f i :=
-function.update 0 i x
+/-- The function supported at `i`, with value `x` there, and `1` elsewhere. -/
+@[to_additive pi.single "The function supported at `i`, with value `x` there, and `0` elsewhere." ]
+def mul_single (i : I) (x : f i) : Π i, f i :=
+function.update 1 i x
 
-@[simp] lemma single_eq_same (i : I) (x : f i) : single i x i = x :=
+@[simp, to_additive]
+lemma mul_single_eq_same (i : I) (x : f i) : mul_single i x i = x :=
 function.update_same i x _
 
-@[simp] lemma single_eq_of_ne {i i' : I} (h : i' ≠ i) (x : f i) : single i x i' = 0 :=
+@[simp, to_additive]
+lemma mul_single_eq_of_ne {i i' : I} (h : i' ≠ i) (x : f i) : mul_single i x i' = 1 :=
 function.update_noteq h x _
 
-/-- Abbreviation for `single_eq_of_ne h.symm`, for ease of use by `simp`. -/
-@[simp] lemma single_eq_of_ne' {i i' : I} (h : i ≠ i') (x : f i) : single i x i' = 0 :=
-single_eq_of_ne h.symm x
+/-- Abbreviation for `mul_single_eq_of_ne h.symm`, for ease of use by `simp`. -/
+@[simp, to_additive "Abbreviation for `single_eq_of_ne h.symm`, for ease of
+use by `simp`."]
+lemma mul_single_eq_of_ne' {i i' : I} (h : i ≠ i') (x : f i) : mul_single i x i' = 1 :=
+mul_single_eq_of_ne h.symm x
 
-@[simp] lemma single_zero (i : I) : single i (0 : f i) = 0 :=
+@[simp, to_additive]
+lemma mul_single_one (i : I) : mul_single i (1 : f i) = 1 :=
 function.update_eq_self _ _
 
-/-- On non-dependent functions, `pi.single` can be expressed as an `ite` -/
-lemma single_apply {β : Sort*} [has_zero β] (i : I) (x : β) (i' : I) :
-  single i x i' = if i' = i then x else 0 :=
-function.update_apply 0 i x i'
+/-- On non-dependent functions, `pi.mul_single` can be expressed as an `ite` -/
+@[to_additive "On non-dependent functions, `pi.single` can be expressed as an `ite`"]
+lemma mul_single_apply {β : Sort*} [has_one β] (i : I) (x : β) (i' : I) :
+  mul_single i x i' = if i' = i then x else 1 :=
+function.update_apply 1 i x i'
 
-/-- On non-dependent functions, `pi.single` is symmetric in the two indices. -/
-lemma single_comm {β : Sort*} [has_zero β] (i : I) (x : β) (i' : I) :
-  single i x i' = single i' x i :=
-by simp [single_apply, eq_comm]
+/-- On non-dependent functions, `pi.mul_single` is symmetric in the two indices. -/
+@[to_additive "On non-dependent functions, `pi.single` is symmetric in the two
+indices."]
+lemma mul_single_comm {β : Sort*} [has_one β] (i : I) (x : β) (i' : I) :
+  mul_single i x i' = mul_single i' x i :=
+by simp [mul_single_apply, eq_comm]
 
-lemma apply_single (f' : Π i, f i → g i) (hf' : ∀ i, f' i 0 = 0) (i : I) (x : f i) (j : I):
-  f' j (single i x j) = single i (f' i x) j :=
-by simpa only [pi.zero_apply, hf', single] using function.apply_update f' 0 i x j
+@[to_additive]
+lemma apply_mul_single (f' : Π i, f i → g i) (hf' : ∀ i, f' i 1 = 1) (i : I) (x : f i) (j : I):
+  f' j (mul_single i x j) = mul_single i (f' i x) j :=
+by simpa only [pi.one_apply, hf', mul_single] using function.apply_update f' 1 i x j
 
-lemma apply_single₂ (f' : Π i, f i → g i → h i) (hf' : ∀ i, f' i 0 0 = 0)
+@[to_additive apply_single₂]
+lemma apply_mul_single₂ (f' : Π i, f i → g i → h i) (hf' : ∀ i, f' i 1 1 = 1)
   (i : I) (x : f i) (y : g i) (j : I):
-  f' j (single i x j) (single i y j) = single i (f' i x y) j :=
+  f' j (mul_single i x j) (mul_single i y j) = mul_single i (f' i x y) j :=
 begin
   by_cases h : j = i,
-  { subst h, simp only [single_eq_same] },
-  { simp only [single_eq_of_ne h, hf'] },
+  { subst h, simp only [mul_single_eq_same] },
+  { simp only [mul_single_eq_of_ne h, hf'] },
 end
 
-lemma single_op {g : I → Type*} [Π i, has_zero (g i)] (op : Π i, f i → g i) (h : ∀ i, op i 0 = 0)
+@[to_additive]
+lemma mul_single_op {g : I → Type*} [Π i, has_one (g i)] (op : Π i, f i → g i) (h : ∀ i, op i 1 = 1)
   (i : I) (x : f i) :
-  single i (op i x) = λ j, op j (single i x j) :=
-eq.symm $ funext $ apply_single op h i x
+  mul_single i (op i x) = λ j, op j (mul_single i x j) :=
+eq.symm $ funext $ apply_mul_single op h i x
 
-lemma single_op₂ {g₁ g₂ : I → Type*} [Π i, has_zero (g₁ i)] [Π i, has_zero (g₂ i)]
-  (op : Π i, g₁ i → g₂ i → f i) (h : ∀ i, op i 0 0 = 0) (i : I) (x₁ : g₁ i) (x₂ : g₂ i) :
-  single i (op i x₁ x₂) = λ j, op j (single i x₁ j) (single i x₂ j) :=
-eq.symm $ funext $ apply_single₂ op h i x₁ x₂
+@[to_additive]
+lemma mul_single_op₂ {g₁ g₂ : I → Type*} [Π i, has_one (g₁ i)] [Π i, has_one (g₂ i)]
+  (op : Π i, g₁ i → g₂ i → f i) (h : ∀ i, op i 1 1 = 1) (i : I) (x₁ : g₁ i) (x₂ : g₂ i) :
+  mul_single i (op i x₁ x₂) = λ j, op j (mul_single i x₁ j) (mul_single i x₂ j) :=
+eq.symm $ funext $ apply_mul_single₂ op h i x₁ x₂
 
 variables (f)
 
-lemma single_injective (i : I) : function.injective (single i : f i → Π i, f i) :=
+@[to_additive]
+lemma mul_single_injective (i : I) : function.injective (mul_single i : f i → Π i, f i) :=
 function.update_injective _ i
 
-@[simp] lemma single_inj (i : I) {x y : f i} : pi.single i x = pi.single i y ↔ x = y :=
-(pi.single_injective _ _).eq_iff
+@[simp, to_additive]
+lemma mul_single_inj (i : I) {x y : f i} : mul_single i x = mul_single i y ↔ x = y :=
+(pi.mul_single_injective _ _).eq_iff
 
 end
 
@@ -197,7 +212,8 @@ lemma bijective_pi_map {F : Π i, f i → g i} (hF : ∀ i, bijective (F i)) :
 
 end function
 
-lemma subsingleton.pi_single_eq {α : Type*} [decidable_eq I] [subsingleton I] [has_zero α]
+@[to_additive subsingleton.pi_single_eq]
+lemma subsingleton.pi_mul_single_eq {α : Type*} [decidable_eq I] [subsingleton I] [has_one α]
   (i : I) (x : α) :
-  pi.single i x = λ _, x :=
-funext $ λ j, by rw [subsingleton.elim j i, pi.single_eq_same]
+  pi.mul_single i x = λ _, x :=
+funext $ λ j, by rw [subsingleton.elim j i, pi.mul_single_eq_same]