Documentation

Mathlib.Algebra.Ring.Pi

Pi instances for ring #

This file defines instances for ring, semiring and related structures on Pi Types

instance Pi.distrib {I : Type u} {f : IType v} [(i : I) → Distrib (f i)] :
Distrib ((i : I) → f i)
Equations
    instance Pi.hasDistribNeg {I : Type u} {f : IType v} [(i : I) → Mul (f i)] [(i : I) → HasDistribNeg (f i)] :
    HasDistribNeg ((i : I) → f i)
    Equations
      instance Pi.addMonoidWithOne {I : Type u} {f : IType v} [(i : I) → AddMonoidWithOne (f i)] :
      AddMonoidWithOne ((i : I) → f i)
      Equations
        instance Pi.addGroupWithOne {I : Type u} {f : IType v} [(i : I) → AddGroupWithOne (f i)] :
        AddGroupWithOne ((i : I) → f i)
        Equations
          instance Pi.nonUnitalNonAssocSemiring {I : Type u} {f : IType v} [(i : I) → NonUnitalNonAssocSemiring (f i)] :
          NonUnitalNonAssocSemiring ((i : I) → f i)
          Equations
            instance Pi.nonUnitalSemiring {I : Type u} {f : IType v} [(i : I) → NonUnitalSemiring (f i)] :
            NonUnitalSemiring ((i : I) → f i)
            Equations
              instance Pi.nonAssocSemiring {I : Type u} {f : IType v} [(i : I) → NonAssocSemiring (f i)] :
              NonAssocSemiring ((i : I) → f i)
              Equations
                instance Pi.semiring {I : Type u} {f : IType v} [(i : I) → Semiring (f i)] :
                Semiring ((i : I) → f i)
                Equations
                  instance Pi.nonUnitalCommSemiring {I : Type u} {f : IType v} [(i : I) → NonUnitalCommSemiring (f i)] :
                  NonUnitalCommSemiring ((i : I) → f i)
                  Equations
                    instance Pi.commSemiring {I : Type u} {f : IType v} [(i : I) → CommSemiring (f i)] :
                    CommSemiring ((i : I) → f i)
                    Equations
                      instance Pi.nonUnitalNonAssocRing {I : Type u} {f : IType v} [(i : I) → NonUnitalNonAssocRing (f i)] :
                      NonUnitalNonAssocRing ((i : I) → f i)
                      Equations
                        instance Pi.nonUnitalRing {I : Type u} {f : IType v} [(i : I) → NonUnitalRing (f i)] :
                        NonUnitalRing ((i : I) → f i)
                        Equations
                          instance Pi.nonAssocRing {I : Type u} {f : IType v} [(i : I) → NonAssocRing (f i)] :
                          NonAssocRing ((i : I) → f i)
                          Equations
                            instance Pi.ring {I : Type u} {f : IType v} [(i : I) → Ring (f i)] :
                            Ring ((i : I) → f i)
                            Equations
                              instance Pi.nonUnitalCommRing {I : Type u} {f : IType v} [(i : I) → NonUnitalCommRing (f i)] :
                              NonUnitalCommRing ((i : I) → f i)
                              Equations
                                instance Pi.commRing {I : Type u} {f : IType v} [(i : I) → CommRing (f i)] :
                                CommRing ((i : I) → f i)
                                Equations
                                  def Pi.nonUnitalRingHom {I : Type u} {f : IType v} {γ : Type w} [(i : I) → NonUnitalNonAssocSemiring (f i)] [NonUnitalNonAssocSemiring γ] (g : (i : I) → γ →ₙ+* f i) :
                                  γ →ₙ+* (i : I) → f i

                                  A family of non-unital ring homomorphisms f a : γ →ₙ+* β a defines a non-unital ring homomorphism Pi.nonUnitalRingHom f : γ →+* Π a, β a given by Pi.nonUnitalRingHom f x b = f b x.

                                  Equations
                                    Instances For
                                      @[simp]
                                      theorem Pi.nonUnitalRingHom_apply {I : Type u} {f : IType v} {γ : Type w} [(i : I) → NonUnitalNonAssocSemiring (f i)] [NonUnitalNonAssocSemiring γ] (g : (i : I) → γ →ₙ+* f i) (x : γ) (b : I) :
                                      (Pi.nonUnitalRingHom g) x b = (g b) x
                                      theorem Pi.nonUnitalRingHom_injective {I : Type u} {f : IType v} {γ : Type w} [Nonempty I] [(i : I) → NonUnitalNonAssocSemiring (f i)] [NonUnitalNonAssocSemiring γ] (g : (i : I) → γ →ₙ+* f i) (hg : ∀ (i : I), Function.Injective (g i)) :
                                      def Pi.ringHom {I : Type u} {f : IType v} {γ : Type w} [(i : I) → NonAssocSemiring (f i)] [NonAssocSemiring γ] (g : (i : I) → γ →+* f i) :
                                      γ →+* (i : I) → f i

                                      A family of ring homomorphisms f a : γ →+* β a defines a ring homomorphism Pi.ringHom f : γ →+* Π a, β a given by Pi.ringHom f x b = f b x.

                                      Equations
                                        Instances For
                                          @[simp]
                                          theorem Pi.ringHom_apply {I : Type u} {f : IType v} {γ : Type w} [(i : I) → NonAssocSemiring (f i)] [NonAssocSemiring γ] (g : (i : I) → γ →+* f i) (x : γ) (b : I) :
                                          (Pi.ringHom g) x b = (g b) x
                                          theorem Pi.ringHom_injective {I : Type u} {f : IType v} {γ : Type w} [Nonempty I] [(i : I) → NonAssocSemiring (f i)] [NonAssocSemiring γ] (g : (i : I) → γ →+* f i) (hg : ∀ (i : I), Function.Injective (g i)) :
                                          def Pi.evalNonUnitalRingHom {I : Type u} (f : IType v) [(i : I) → NonUnitalNonAssocSemiring (f i)] (i : I) :
                                          ((i : I) → f i) →ₙ+* f i

                                          Evaluation of functions into an indexed collection of non-unital rings at a point is a non-unital ring homomorphism. This is Function.eval as a NonUnitalRingHom.

                                          Equations
                                            Instances For
                                              @[simp]
                                              theorem Pi.evalNonUnitalRingHom_apply {I : Type u} (f : IType v) [(i : I) → NonUnitalNonAssocSemiring (f i)] (i : I) (g : (i : I) → f i) :
                                              def Pi.constNonUnitalRingHom (α : Type u_1) (β : Type u_2) [NonUnitalNonAssocSemiring β] :
                                              β →ₙ+* αβ

                                              Function.const as a NonUnitalRingHom.

                                              Equations
                                                Instances For
                                                  @[simp]
                                                  theorem Pi.constNonUnitalRingHom_apply (α : Type u_1) (β : Type u_2) [NonUnitalNonAssocSemiring β] (a : β) (a✝ : α) :
                                                  (constNonUnitalRingHom α β) a a✝ = Function.const α a a✝
                                                  def NonUnitalRingHom.compLeft {α : Type u_1} {β : Type u_2} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) (I : Type u_3) :
                                                  (Iα) →ₙ+* Iβ

                                                  Non-unital ring homomorphism between the function spaces I → α and I → β, induced by a non-unital ring homomorphism f between α and β.

                                                  Equations
                                                    Instances For
                                                      @[simp]
                                                      theorem NonUnitalRingHom.compLeft_apply {α : Type u_1} {β : Type u_2} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) (I : Type u_3) (h : Iα) (a✝ : I) :
                                                      (f.compLeft I) h a✝ = (f h) a✝
                                                      def Pi.evalRingHom {I : Type u} (f : IType v) [(i : I) → NonAssocSemiring (f i)] (i : I) :
                                                      ((i : I) → f i) →+* f i

                                                      Evaluation of functions into an indexed collection of rings at a point is a ring homomorphism. This is Function.eval as a RingHom.

                                                      Equations
                                                        Instances For
                                                          @[simp]
                                                          theorem Pi.evalRingHom_apply {I : Type u} (f : IType v) [(i : I) → NonAssocSemiring (f i)] (i : I) (g : (i : I) → f i) :
                                                          (evalRingHom f i) g = g i
                                                          instance instRingHomSurjectiveForallEvalRingHom {I : Type u} (f : IType u_1) [(i : I) → Semiring (f i)] (i : I) :
                                                          def Pi.constRingHom (α : Type u_1) (β : Type u_2) [NonAssocSemiring β] :
                                                          β →+* αβ

                                                          Function.const as a RingHom.

                                                          Equations
                                                            Instances For
                                                              @[simp]
                                                              theorem Pi.constRingHom_apply (α : Type u_1) (β : Type u_2) [NonAssocSemiring β] (a : β) (a✝ : α) :
                                                              (constRingHom α β) a a✝ = Function.const α a a✝
                                                              def RingHom.compLeft {α : Type u_1} {β : Type u_2} [NonAssocSemiring α] [NonAssocSemiring β] (f : α →+* β) (I : Type u_3) :
                                                              (Iα) →+* Iβ

                                                              Ring homomorphism between the function spaces I → α and I → β, induced by a ring homomorphism f between α and β.

                                                              Equations
                                                                Instances For
                                                                  @[simp]
                                                                  theorem RingHom.compLeft_apply {α : Type u_1} {β : Type u_2} [NonAssocSemiring α] [NonAssocSemiring β] (f : α →+* β) (I : Type u_3) (h : Iα) (a✝ : I) :
                                                                  (f.compLeft I) h a✝ = (f h) a✝