refactor(algebra/pi_instance): delete pi_instance file, and move instances to group/ring etc appropriately (#3513)

Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Chris Hughes <chrishughes24@gmail.com>

Author: 3 people

src/algebra/add_torsor.lean

@@ -5,7 +5,7 @@ Authors: Joseph Myers, Yury Kudryashov.
 -/
 import algebra.group.prod
 import algebra.group.type_tags
-import algebra.pi_instances
+import algebra.group.pi
 import data.equiv.basic
 
 /-!

src/algebra/big_operators/pi.lean

@@ -0,0 +1,104 @@
+/-
+Copyright (c) 2018 Simon Hudon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Simon Hudon, Patrick Massot
+-/
+import algebra.ring.pi
+import algebra.big_operators
+import data.fintype.basic
+import algebra.group.prod
+/-!
+# Big operators for Pi Types
+
+This file contains theorems relevant to big operators in binary and arbitrary product
+of monoids and groups
+-/
+
+open_locale big_operators
+
+namespace pi
+
+@[to_additive]
+lemma list_prod_apply {α : Type*} {β : α → Type*} [∀a, monoid (β a)] (a : α) :
+  ∀ (l : list (Πa, β a)), l.prod a = (l.map (λf:Πa, β a, f a)).prod
+| []       := rfl
+| (f :: l) := by simp [mul_apply f l.prod a, list_prod_apply l]
+
+@[to_additive]
+lemma multiset_prod_apply {α : Type*} {β : α → Type*} [∀a, comm_monoid (β a)] (a : α)
+  (s : multiset (Πa, β a)) : s.prod a = (s.map (λf:Πa, β a, f a)).prod :=
+quotient.induction_on s $ assume l, begin simp [list_prod_apply a l] end
+
+end pi
+
+@[simp, to_additive]
+lemma finset.prod_apply {α : Type*} {β : α → Type*} {γ} [∀a, comm_monoid (β a)] (a : α)
+  (s : finset γ) (g : γ → Πa, β a) : (∏ c in s, g c) a = ∏ c in s, g c a :=
+show (s.val.map g).prod a = (s.val.map (λc, g c a)).prod,
+  by rw [pi.multiset_prod_apply, multiset.map_map]
+
+@[to_additive prod_mk_sum]
+lemma prod_mk_prod {α β γ : Type*} [comm_monoid α] [comm_monoid β] (s : finset γ)
+  (f : γ → α) (g : γ → β) : (∏ x in s, f x, ∏ x in s, g x) = ∏ x in s, (f x, g x) :=
+by haveI := classical.dec_eq γ; exact
+finset.induction_on s rfl (by simp [prod.ext_iff] {contextual := tt})
+
+section single
+variables {I : Type*} [decidable_eq I] {Z : I → Type*}
+variables [Π i, add_comm_monoid (Z i)]
+
+-- As we only defined `single` into `add_monoid`, we only prove the `finset.sum` version here.
+lemma finset.univ_sum_single [fintype I] (f : Π i, Z i) :
+  ∑ i, pi.single i (f i) = f :=
+begin
+  ext a,
+  rw [finset.sum_apply, finset.sum_eq_single a],
+  { simp, },
+  { intros b _ h, simp [h.symm], },
+  { intro h, exfalso, simpa using h, },
+end
+
+@[ext]
+lemma add_monoid_hom.functions_ext [fintype I] (G : Type*)
+  [add_comm_monoid G] (g h : (Π i, Z i) →+ G)
+  (w : ∀ (i : I) (x : Z i), g (pi.single i x) = h (pi.single i x)) : g = h :=
+begin
+  ext k,
+  rw [←finset.univ_sum_single k, add_monoid_hom.map_sum, add_monoid_hom.map_sum],
+  apply finset.sum_congr rfl,
+  intros,
+  apply w,
+end
+
+end single
+
+section ring_hom
+open pi
+variables {I : Type*} [decidable_eq I] {f : I → Type*}
+variables [Π i, semiring (f i)]
+
+-- we need `apply`+`convert` because Lean fails to unify different `add_monoid` instances
+-- on `Π i, f i`
+@[ext]
+lemma ring_hom.functions_ext [fintype I] (G : Type*) [semiring G] (g h : (Π i, f i) →+* G)
+  (w : ∀ (i : I) (x : f i), g (single i x) = h (single i x)) : g = h :=
+begin
+  apply ring_hom.coe_add_monoid_hom_injective,
+  convert add_monoid_hom.functions_ext _ _ _ _; assumption
+end
+
+end ring_hom
+
+namespace prod
+
+variables {α β γ : Type*} [comm_monoid α] [comm_monoid β] {s : finset γ} {f : γ → α × β}
+
+@[to_additive]
+lemma fst_prod : (∏ c in s, f c).1 = ∏ c in s, (f c).1 :=
+(monoid_hom.fst α β).map_prod f s
+
+@[to_additive]
+lemma snd_prod  : (∏ c in s, f c).2 = ∏ c in s, (f c).2 :=
+(monoid_hom.snd α β).map_prod f s
+
+end prod

src/algebra/category/CommRing/limits.lean

@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import algebra.category.CommRing.basic
+import ring_theory.subring
+import algebra.ring.pi
 
 /-!
 # The category of commutative rings has all limits

src/algebra/category/Group/biproducts.lean

@@ -6,7 +6,7 @@ Authors: Scott Morrison
 import algebra.category.Group.basic
 import algebra.category.Group.preadditive
 import category_theory.limits.shapes.biproducts
-import algebra.pi_instances
+import algebra.group.pi
 
 /-!
 # The category of abelian groups has finite biproducts

src/algebra/category/Group/limits.lean

@@ -6,7 +6,7 @@ Authors: Scott Morrison
 import algebra.category.Group.basic
 import category_theory.limits.types
 import category_theory.limits.preserves
-import algebra.pi_instances
+import algebra.group.pi
 
 /-!
 # The category of abelian groups has all limits

src/algebra/char_p.lean

@@ -7,7 +7,7 @@ Author: Kenny Lau, Joey van Langen, Casper Putz
 import data.fintype.basic
 import data.nat.choose
 import data.int.modeq
-import algebra.module
+import algebra.module.basic
 import algebra.iterate_hom
 
 /-!

src/algebra/default.lean

@@ -1,2 +1,2 @@
 import algebra.group
-import algebra.module
+import algebra.module.basic

src/algebra/field.lean

@@ -3,7 +3,7 @@ Copyright (c) 2014 Robert Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Lewis, Leonardo de Moura, Johannes Hölzl, Mario Carneiro
 -/
-import algebra.ring
+import algebra.ring.basic
 import algebra.group_with_zero
 open set
 

src/algebra/group/pi.lean

@@ -0,0 +1,155 @@
+/-
+Copyright (c) 2018 Simon Hudon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Simon Hudon, Patrick Massot
+-/
+import algebra.ordered_group tactic.pi_instances
+/-!
+# Pi instances for groups and monoids
+
+This file defines instances for group, monoid, semigroup and related structures on Pi Types
+-/
+
+universes u v w
+variable {I : Type u}     -- The indexing type
+variable {f : I → Type v} -- The family of types already equipped with instances
+variables (x y : Π i, f i) (i : I)
+
+namespace pi
+
+@[to_additive] instance has_one [∀ i, has_one $ f i] : has_one (Π i : I, f i) := ⟨λ _, 1⟩
+@[simp, to_additive] lemma one_apply [∀ i, has_one $ f i] : (1 : Π i, f i) i = 1 := rfl
+
+@[to_additive]
+instance has_mul [∀ i, has_mul $ f i] : has_mul (Π i : I, f i) := ⟨λ f g i, f i * g i⟩
+@[simp, to_additive] lemma mul_apply [∀ i, has_mul $ f i] : (x * y) i = x i * y i := rfl
+
+@[to_additive] instance has_inv [∀ i, has_inv $ f i] : has_inv (Π i : I, f i) := ⟨λ f i, (f i)⁻¹⟩
+@[simp, to_additive] lemma inv_apply [∀ i, has_inv $ f i] : x⁻¹ i = (x i)⁻¹ := rfl
+
+@[to_additive add_semigroup]
+instance semigroup [∀ i, semigroup $ f i] : semigroup (Π i : I, f i) :=
+by refine_struct { mul := (*), .. }; tactic.pi_instance_derive_field
+
+@[to_additive add_comm_semigroup]
+instance comm_semigroup [∀ i, comm_semigroup $ f i] : comm_semigroup (Π i : I, f i) :=
+by refine_struct { mul := (*), .. }; tactic.pi_instance_derive_field
+
+@[to_additive add_monoid]
+instance monoid [∀ i, monoid $ f i] : monoid (Π i : I, f i) :=
+by refine_struct { one := (1 : Π i, f i), mul := (*), .. }; tactic.pi_instance_derive_field
+
+@[to_additive add_comm_monoid]
+instance comm_monoid [∀ i, comm_monoid $ f i] : comm_monoid (Π i : I, f i) :=
+by refine_struct { one := (1 : Π i, f i), mul := (*), .. }; tactic.pi_instance_derive_field
+
+@[to_additive add_group]
+instance group [∀ i, group $ f i] : group (Π i : I, f i) :=
+by refine_struct { one := (1 : Π i, f i), mul := (*), inv := has_inv.inv, .. };
+  tactic.pi_instance_derive_field
+
+@[simp] lemma sub_apply [∀ i, add_group $ f i] : (x - y) i = x i - y i := rfl
+
+@[to_additive add_comm_group]
+instance comm_group [∀ i, comm_group $ f i] : comm_group (Π i : I, f i) :=
+by refine_struct { one := (1 : Π i, f i), mul := (*), inv := has_inv.inv, .. };
+  tactic.pi_instance_derive_field
+
+@[to_additive add_left_cancel_semigroup]
+instance left_cancel_semigroup [∀ i, left_cancel_semigroup $ f i] :
+  left_cancel_semigroup (Π i : I, f i) :=
+by refine_struct { mul := (*) }; tactic.pi_instance_derive_field
+
+@[to_additive add_right_cancel_semigroup]
+instance right_cancel_semigroup [∀ i, right_cancel_semigroup $ f i] :
+  right_cancel_semigroup (Π i : I, f i) :=
+by refine_struct { mul := (*) }; tactic.pi_instance_derive_field
+
+@[to_additive ordered_cancel_add_comm_monoid]
+instance ordered_cancel_comm_monoid [∀ i, ordered_cancel_comm_monoid $ f i] :
+  ordered_cancel_comm_monoid (Π i : I, f i) :=
+by refine_struct { mul := (*), one := (1 : Π i, f i), le := (≤), lt := (<), .. pi.partial_order };
+  tactic.pi_instance_derive_field
+
+@[to_additive ordered_add_comm_group]
+instance ordered_comm_group [∀ i, ordered_comm_group $ f i] :
+  ordered_comm_group (Π i : I, f i) :=
+{ mul_le_mul_left := λ x y hxy c i, mul_le_mul_left' (hxy i) _,
+  ..pi.comm_group,
+  ..pi.partial_order }
+
+variables [decidable_eq I]
+variables [Π i, has_zero (f i)]
+
+/-- The function supported at `i`, with value `x` there. -/
+def single (i : I) (x : f i) : Π i, f i :=
+λ i', if h : i' = i then (by { subst h, exact x }) else 0
+
+@[simp]
+lemma single_eq_same (i : I) (x : f i) : single i x i = x :=
+begin
+  dsimp [single],
+  split_ifs,
+  { refl, },
+  { exfalso, exact h rfl, }
+end
+
+@[simp]
+lemma single_eq_of_ne {i i' : I} (h : i' ≠ i) (x : f i) : single i x i' = 0 :=
+begin
+  dsimp [single],
+  split_ifs with h',
+  { exfalso, exact h h', },
+  { refl, }
+end
+
+end pi
+
+section monoid_hom
+
+variables (f) [Π i, monoid (f i)]
+
+/-- Evaluation of functions into an indexed collection of monoids at a point is a monoid
+homomorphism. -/
+@[to_additive "Evaluation of functions into an indexed collection of additive monoids at a point
+is an additive monoid homomorphism."]
+def monoid_hom.apply (i : I) : (Π i, f i) →* f i :=
+{ to_fun := λ g, g i,
+  map_one' := rfl,
+  map_mul' := λ x y, rfl, }
+
+@[simp, to_additive]
+lemma monoid_hom.apply_apply (i : I) (g : Π i, f i) :
+  (monoid_hom.apply f i) g = g i := rfl
+
+end monoid_hom
+
+section add_monoid_single
+variables [decidable_eq I] (f) [Π i, add_monoid (f i)]
+open pi
+
+/-- The additive monoid homomorphism including a single additive monoid
+into a dependent family of additive monoids, as functions supported at a point. -/
+def add_monoid_hom.single (i : I) : f i →+ Π i, f i :=
+{ to_fun := λ x, single i x,
+  map_zero' :=
+  begin
+    ext i', by_cases h : i' = i,
+    { subst h, simp only [single_eq_same], refl, },
+    { simp only [h, single_eq_of_ne, ne.def, not_false_iff], refl, },
+  end,
+  map_add' := λ x y,
+  begin
+    ext i', by_cases h : i' = i,
+    -- FIXME in the next two `simp only`s,
+    -- it would be really nice to not have to provide the arguments to `add_apply`.
+    { subst h, simp only [single_eq_same, add_apply (single i' x) (single i' y) i'], },
+    { simp only [h, add_zero, single_eq_of_ne,
+        add_apply (single i x) (single i y) i', ne.def, not_false_iff], },
+  end, }
+
+@[simp]
+lemma add_monoid_hom.single_apply {i : I} (x : f i) :
+  (add_monoid_hom.single f i) x = single i x := rfl
+
+end add_monoid_single

src/algebra/group/with_one.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Johan Commelin
 -/
-import algebra.ring
+import algebra.ring.basic
 
 universes u v
 variable {α : Type u}