feat(ring_theory/prod): ring homs to/from R × S (#2836)

* move some instances from `algebra/pi_instances`;
* add `prod.comm_semiring`;
* define `ring_hom.fst`, `ring_hom.snd`, `ring_hom.prod`, and
  `ring_hom.prod_map`.

Author: urkud

src/algebra/group/prod.lean

@@ -156,15 +156,15 @@ protected def prod (f : M →* N) (g : M →* P) : M →* N × P :=
 @[simp, to_additive prod_apply]
 lemma prod_apply (f : M →* N) (g : M →* P) (x) : f.prod g x = (f x, g x) := rfl
 
-@[to_additive fst_comp_prod]
+@[simp, to_additive fst_comp_prod]
 lemma fst_comp_prod (f : M →* N) (g : M →* P) : (fst N P).comp (f.prod g) = f :=
 ext $ λ x, rfl
 
-@[to_additive snd_comp_prod]
+@[simp, to_additive snd_comp_prod]
 lemma snd_comp_prod (f : M →* N) (g : M →* P) : (snd N P).comp (f.prod g) = g :=
 ext $ λ x, rfl
 
-@[to_additive prod_unique]
+@[simp, to_additive prod_unique]
 lemma prod_unique (f : M →* N × P) :
   ((fst N P).comp f).prod ((snd N P).comp f) = f :=
 ext $ λ x, by simp only [prod_apply, coe_fst, coe_snd, comp_apply, prod.mk.eta]
@@ -183,9 +183,8 @@ def prod_map : M × N →* M' × N' := (f.comp (fst M N)).prod (g.comp (snd M N)
 @[to_additive prod_map_def]
 lemma prod_map_def : prod_map f g = (f.comp (fst M N)).prod (g.comp (snd M N)) := rfl
 
--- TODO : use `rfl` once we redefine `prod.map` in stdlib
 @[simp, to_additive coe_prod_map]
-lemma coe_prod_map : ⇑(prod_map f g) = prod.map f g := funext $ λ ⟨x, y⟩, rfl
+lemma coe_prod_map : ⇑(prod_map f g) = prod.map f g := rfl
 
 @[to_additive prod_comp_prod_map]
 lemma prod_comp_prod_map (f : P →* M) (g : P →* N) (f' : M →* M') (g' : N →* N') :

src/algebra/pi_instances.lean

@@ -2,11 +2,14 @@
 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
-
-Pi instances for algebraic structures.
 -/
 import algebra.module
 import ring_theory.subring
+import ring_theory.prod
+
+/-!
+# Pi instances for algebraic structures
+-/
 
 namespace pi
 universes u v w
@@ -339,32 +342,15 @@ lemma snd_prod [comm_monoid α] [comm_monoid β] {t : finset γ} {f : γ → α
   (t.prod f).2 = t.prod (λc, (f c).2) :=
 (monoid_hom.snd α β).map_prod f t
 
-instance [semiring α] [semiring β] : semiring (α × β) :=
-{ zero_mul := λ a, mk.inj_iff.mpr ⟨zero_mul _, zero_mul _⟩,
-  mul_zero := λ a, mk.inj_iff.mpr ⟨mul_zero _, mul_zero _⟩,
-  left_distrib := λ a b c, mk.inj_iff.mpr ⟨left_distrib _ _ _, left_distrib _ _ _⟩,
-  right_distrib := λ a b c, mk.inj_iff.mpr ⟨right_distrib _ _ _, right_distrib _ _ _⟩,
-  ..prod.add_comm_monoid, ..prod.monoid }
-
-instance [ring α] [ring β] : ring (α × β) :=
-{ ..prod.add_comm_group, ..prod.semiring }
-
-instance [comm_ring α] [comm_ring β] : comm_ring (α × β) :=
-{ ..prod.ring, ..prod.comm_monoid }
-
-instance [nonzero_comm_ring α] [comm_ring β] : nonzero_comm_ring (α × β) :=
-{ zero_ne_one := mt (congr_arg prod.fst) zero_ne_one,
-  ..prod.comm_ring }
-
 instance fst.is_semiring_hom [semiring α] [semiring β] : is_semiring_hom (prod.fst : α × β → α) :=
-by refine_struct {..}; simp
+(ring_hom.fst α β).is_semiring_hom
 instance snd.is_semiring_hom [semiring α] [semiring β] : is_semiring_hom (prod.snd : α × β → β) :=
-by refine_struct {..}; simp
+(ring_hom.snd α β).is_semiring_hom
 
 instance fst.is_ring_hom [ring α] [ring β] : is_ring_hom (prod.fst : α × β → α) :=
-by refine_struct {..}; simp
+(ring_hom.fst α β).is_ring_hom
 instance snd.is_ring_hom [ring α] [ring β] : is_ring_hom (prod.snd : α × β → β) :=
-by refine_struct {..}; simp
+(ring_hom.snd α β).is_ring_hom
 
 /-- Left injection function for the inner product
 From a vector space (and also group and module) perspective the product is the same as the sum of

src/ring_theory/prod.lean

@@ -0,0 +1,111 @@
+/-
+Copyright (c) 2020 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Chris Hughes, Mario Carneiro, Yury Kudryashov
+-/
+import algebra.group.prod
+import algebra.ring
+
+/-!
+# Semiring, ring etc structures on `R × S`
+
+In this file we define two-binop (`semiring`, `ring` etc) structures on `R × S`. We also prove
+trivial `simp` lemmas, and define the following operations on `ring_hom`s:
+
+* `fst R S : R × S →+* R`, `snd R S : R × S →+* R`: projections `prod.fst` and `prod.snd`
+  as `ring_hom`s;
+* `f.prod g : `R →+* S × T`: sends `x` to `(f x, g x)`;
+* `f.prod_map g : `R × S → R' × S'`: `prod.map f g` as a `ring_hom`,
+  sends `(x, y)` to `(f x, g y)`.
+-/
+
+variables {R : Type*} {R' : Type*} {S : Type*} {S' : Type*} {T : Type*} {T' : Type*}
+
+namespace prod
+
+/-- Product of two semirings is a semiring. -/
+instance [semiring R] [semiring S] : semiring (R × S) :=
+{ zero_mul := λ a, mk.inj_iff.mpr ⟨zero_mul _, zero_mul _⟩,
+  mul_zero := λ a, mk.inj_iff.mpr ⟨mul_zero _, mul_zero _⟩,
+  left_distrib := λ a b c, mk.inj_iff.mpr ⟨left_distrib _ _ _, left_distrib _ _ _⟩,
+  right_distrib := λ a b c, mk.inj_iff.mpr ⟨right_distrib _ _ _, right_distrib _ _ _⟩,
+  .. prod.add_comm_monoid, .. prod.monoid }
+
+/-- Product of two commutative semirings is a commutative semiring. -/
+instance [comm_semiring R] [comm_semiring S] : comm_semiring (R × S) :=
+{ .. prod.semiring, .. prod.comm_monoid }
+
+/-- Product of two rings is a ring. -/
+instance [ring R] [ring S] : ring (R × S) :=
+{ .. prod.add_comm_group, .. prod.semiring }
+
+/-- Product of two commutative rings is a commutative ring. -/
+instance [comm_ring R] [comm_ring S] : comm_ring (R × S) :=
+{ .. prod.ring, .. prod.comm_monoid }
+
+/-- Product of two commutative rings is a nonzero commutative ring provided that the first
+ring is a nonzero ring. -/
+instance [nonzero_comm_ring R] [comm_ring S] : nonzero_comm_ring (R × S) :=
+{ zero_ne_one := mt (congr_arg prod.fst) zero_ne_one,
+  .. prod.comm_ring }
+
+end prod
+
+namespace ring_hom
+
+variables (R S) [semiring R] [semiring S]
+
+/-- Given semirings `R`, `S`, the natural projection homomorphism from `R × S` to `R`.-/
+def fst : R × S →+* R := { to_fun := prod.fst, .. monoid_hom.fst R S, .. add_monoid_hom.fst R S }
+
+/-- Given semirings `R`, `S`, the natural projection homomorphism from `R × S` to `S`.-/
+def snd : R × S →+* S := { to_fun := prod.snd, .. monoid_hom.snd R S, .. add_monoid_hom.snd R S }
+
+variables {R S}
+
+@[simp] lemma coe_fst : ⇑(fst R S) = prod.fst := rfl
+@[simp] lemma coe_snd : ⇑(snd R S) = prod.snd := rfl
+
+section prod
+
+variables [semiring T] (f : R →+* S) (g : R →+* T)
+
+/-- Combine two ring homomorphisms `f : R →+* S`, `g : R →+* T` into `f.prod g : R →+* S × T`
+given by `(f.prod g) x = (f x, g x)` -/
+protected def prod (f : R →+* S) (g : R →+* T) : R →+* S × T :=
+{ to_fun := λ x, (f x, g x),
+  .. monoid_hom.prod (f : R →* S) (g : R →* T), .. add_monoid_hom.prod (f : R →+ S) (g : R →+ T) }
+
+@[simp] lemma prod_apply (x) : f.prod g x = (f x, g x) := rfl
+
+@[simp] lemma fst_comp_prod : (fst S T).comp (f.prod g) = f :=
+ext $ λ x, rfl
+
+@[simp] lemma snd_comp_prod : (snd S T).comp (f.prod g) = g :=
+ext $ λ x, rfl
+
+lemma prod_unique (f : R →+* S × T) :
+  ((fst S T).comp f).prod ((snd S T).comp f) = f :=
+ext $ λ x, by simp only [prod_apply, coe_fst, coe_snd, comp_apply, prod.mk.eta]
+
+end prod
+
+section prod_map
+
+variables [semiring R'] [semiring S'] [semiring T] (f : R →+* R') (g : S →+* S')
+
+/-- `prod.map` as a `ring_hom`. -/
+def prod_map : R × S →* R' × S' := (f.comp (fst R S)).prod (g.comp (snd R S))
+
+lemma prod_map_def : prod_map f g = (f.comp (fst R S)).prod (g.comp (snd R S)) := rfl
+
+@[simp]
+lemma coe_prod_map : ⇑(prod_map f g) = prod.map f g := rfl
+
+lemma prod_comp_prod_map (f : T →* R) (g : T →* S) (f' : R →* R') (g' : S →* S') :
+  (f'.prod_map g').comp (f.prod g) = (f'.comp f).prod (g'.comp g) :=
+rfl
+
+end prod_map
+
+end ring_hom