Documentation

Mathlib.Algebra.Ring.Prod

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 RingHoms and similarly for NonUnitalRingHoms:

instance Prod.instDistrib {R : Type u_1} {S : Type u_3} [Distrib R] [Distrib S] :
Distrib (R × S)

Product of two distributive types is distributive.

Equations

    Product of two NonAssocSemirings is a NonAssocSemiring.

    Equations
      instance Prod.instSemiring {R : Type u_1} {S : Type u_3} [Semiring R] [Semiring S] :
      Semiring (R × S)

      Product of two semirings is a semiring.

      Equations
        instance Prod.instCommSemiring {R : Type u_1} {S : Type u_3} [CommSemiring R] [CommSemiring S] :

        Product of two commutative semirings is a commutative semiring.

        Equations
          instance Prod.instNonUnitalRing {R : Type u_1} {S : Type u_3} [NonUnitalRing R] [NonUnitalRing S] :
          Equations
            instance Prod.instNonAssocRing {R : Type u_1} {S : Type u_3} [NonAssocRing R] [NonAssocRing S] :
            Equations
              instance Prod.instRing {R : Type u_1} {S : Type u_3} [Ring R] [Ring S] :
              Ring (R × S)

              Product of two rings is a ring.

              Equations
                instance Prod.instCommRing {R : Type u_1} {S : Type u_3} [CommRing R] [CommRing S] :
                CommRing (R × S)

                Product of two commutative rings is a commutative ring.

                Equations

                  Given non-unital semirings R, S, the natural projection homomorphism from R × S to R.

                  Equations
                    Instances For

                      Given non-unital semirings R, S, the natural projection homomorphism from R × S to S.

                      Equations
                        Instances For

                          Combine two non-unital 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)

                          Equations
                            Instances For
                              @[simp]
                              theorem NonUnitalRingHom.prod_apply {R : Type u_1} {S : Type u_3} {T : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring T] (f : R →ₙ+* S) (g : R →ₙ+* T) (x : R) :
                              (f.prod g) x = (f x, g x)
                              @[simp]
                              theorem NonUnitalRingHom.fst_comp_prod {R : Type u_1} {S : Type u_3} {T : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring T] (f : R →ₙ+* S) (g : R →ₙ+* T) :
                              (fst S T).comp (f.prod g) = f
                              @[simp]
                              theorem NonUnitalRingHom.snd_comp_prod {R : Type u_1} {S : Type u_3} {T : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring T] (f : R →ₙ+* S) (g : R →ₙ+* T) :
                              (snd S T).comp (f.prod g) = g

                              Prod.map as a NonUnitalRingHom.

                              Equations
                                Instances For
                                  theorem NonUnitalRingHom.prodMap_def {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring R'] [NonUnitalNonAssocSemiring S'] (f : R →ₙ+* R') (g : S →ₙ+* S') :
                                  f.prodMap g = (f.comp (fst R S)).prod (g.comp (snd R S))
                                  @[simp]
                                  theorem NonUnitalRingHom.coe_prodMap {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring R'] [NonUnitalNonAssocSemiring S'] (f : R →ₙ+* R') (g : S →ₙ+* S') :
                                  (f.prodMap g) = Prod.map f g
                                  theorem NonUnitalRingHom.prod_comp_prodMap {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} {T : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring R'] [NonUnitalNonAssocSemiring S'] [NonUnitalNonAssocSemiring T] (f : T →ₙ+* R) (g : T →ₙ+* S) (f' : R →ₙ+* R') (g' : S →ₙ+* S') :
                                  (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)
                                  def RingHom.fst (R : Type u_1) (S : Type u_3) [NonAssocSemiring R] [NonAssocSemiring S] :
                                  R × S →+* R

                                  Given semirings R, S, the natural projection homomorphism from R × S to R.

                                  Equations
                                    Instances For
                                      def RingHom.snd (R : Type u_1) (S : Type u_3) [NonAssocSemiring R] [NonAssocSemiring S] :
                                      R × S →+* S

                                      Given semirings R, S, the natural projection homomorphism from R × S to S.

                                      Equations
                                        Instances For
                                          @[simp]
                                          theorem RingHom.coe_fst {R : Type u_1} {S : Type u_3} [NonAssocSemiring R] [NonAssocSemiring S] :
                                          (fst R S) = Prod.fst
                                          @[simp]
                                          theorem RingHom.coe_snd {R : Type u_1} {S : Type u_3} [NonAssocSemiring R] [NonAssocSemiring S] :
                                          (snd R S) = Prod.snd
                                          def RingHom.prod {R : Type u_1} {S : Type u_3} {T : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring T] (f : R →+* S) (g : R →+* T) :
                                          R →+* S × 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)

                                          Equations
                                            Instances For
                                              @[simp]
                                              theorem RingHom.prod_apply {R : Type u_1} {S : Type u_3} {T : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring T] (f : R →+* S) (g : R →+* T) (x : R) :
                                              (f.prod g) x = (f x, g x)
                                              @[simp]
                                              theorem RingHom.fst_comp_prod {R : Type u_1} {S : Type u_3} {T : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring T] (f : R →+* S) (g : R →+* T) :
                                              (fst S T).comp (f.prod g) = f
                                              @[simp]
                                              theorem RingHom.snd_comp_prod {R : Type u_1} {S : Type u_3} {T : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring T] (f : R →+* S) (g : R →+* T) :
                                              (snd S T).comp (f.prod g) = g
                                              theorem RingHom.prod_unique {R : Type u_1} {S : Type u_3} {T : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring T] (f : R →+* S × T) :
                                              ((fst S T).comp f).prod ((snd S T).comp f) = f
                                              def RingHom.prodMap {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] (f : R →+* R') (g : S →+* S') :
                                              R × S →+* R' × S'

                                              Prod.map as a RingHom.

                                              Equations
                                                Instances For
                                                  theorem RingHom.prodMap_def {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] (f : R →+* R') (g : S →+* S') :
                                                  f.prodMap g = (f.comp (fst R S)).prod (g.comp (snd R S))
                                                  @[simp]
                                                  theorem RingHom.coe_prodMap {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] (f : R →+* R') (g : S →+* S') :
                                                  (f.prodMap g) = Prod.map f g
                                                  theorem RingHom.prod_comp_prodMap {R : Type u_1} {R' : Type u_2} {S : Type u_3} {S' : Type u_4} {T : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] [NonAssocSemiring T] (f : T →+* R) (g : T →+* S) (f' : R →+* R') (g' : S →+* S') :
                                                  (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)
                                                  def RingEquiv.prodComm {R : Type u_1} {S : Type u_3} [NonAssocSemiring R] [NonAssocSemiring S] :
                                                  R × S ≃+* S × R

                                                  Swapping components as an equivalence of (semi)rings.

                                                  Equations
                                                    Instances For
                                                      def RingEquiv.prodProdProdComm (R : Type u_1) (R' : Type u_2) (S : Type u_3) (S' : Type u_4) [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] :
                                                      (R × R') × S × S' ≃+* (R × S) × R' × S'

                                                      Four-way commutativity of Prod. The name matches mul_mul_mul_comm.

                                                      Equations
                                                        Instances For
                                                          @[simp]
                                                          theorem RingEquiv.prodProdProdComm_apply (R : Type u_1) (R' : Type u_2) (S : Type u_3) (S' : Type u_4) [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] (rrss : (R × R') × S × S') :
                                                          (prodProdProdComm R R' S S') rrss = ((rrss.1.1, rrss.2.1), rrss.1.2, rrss.2.2)
                                                          @[simp]
                                                          theorem RingEquiv.prodProdProdComm_symm (R : Type u_1) (R' : Type u_2) (S : Type u_3) (S' : Type u_4) [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] :
                                                          (prodProdProdComm R R' S S').symm = prodProdProdComm R S R' S'
                                                          @[simp]
                                                          @[simp]
                                                          @[simp]
                                                          theorem RingEquiv.prodProdProdComm_toEquiv (R : Type u_1) (R' : Type u_2) (S : Type u_3) (S' : Type u_4) [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] :
                                                          (prodProdProdComm R R' S S') = Equiv.prodProdProdComm R R' S S'

                                                          A ring R is isomorphic to R × S when S is the zero ring

                                                          Equations
                                                            Instances For
                                                              @[simp]
                                                              theorem RingEquiv.prodZeroRing_apply (R : Type u_1) (S : Type u_3) [NonAssocSemiring R] [NonAssocSemiring S] [Subsingleton S] (x : R) :
                                                              (prodZeroRing R S) x = (x, 0)
                                                              @[simp]
                                                              theorem RingEquiv.prodZeroRing_symm_apply (R : Type u_1) (S : Type u_3) [NonAssocSemiring R] [NonAssocSemiring S] [Subsingleton S] (self : R × S) :
                                                              (prodZeroRing R S).symm self = self.1

                                                              A ring R is isomorphic to S × R when S is the zero ring

                                                              Equations
                                                                Instances For
                                                                  @[simp]
                                                                  theorem RingEquiv.zeroRingProd_symm_apply (R : Type u_1) (S : Type u_3) [NonAssocSemiring R] [NonAssocSemiring S] [Subsingleton S] (self : S × R) :
                                                                  (zeroRingProd R S).symm self = self.2
                                                                  @[simp]
                                                                  theorem RingEquiv.zeroRingProd_apply (R : Type u_1) (S : Type u_3) [NonAssocSemiring R] [NonAssocSemiring S] [Subsingleton S] (x : R) :
                                                                  (zeroRingProd R S) x = (0, x)

                                                                  The product of two nontrivial rings is not a domain