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.nonUnitalNonAssocSemiring {I : Type u} {f : IType v} [(i : I) → NonUnitalNonAssocSemiring (f i)] :
NonUnitalNonAssocSemiring ((i : I) → f i)
Equations
  • Pi.nonUnitalNonAssocSemiring = let __src := Pi.distrib; let __src_1 := Pi.addCommMonoid; let __src_2 := Pi.mulZeroClass; NonUnitalNonAssocSemiring.mk
instance Pi.nonUnitalSemiring {I : Type u} {f : IType v} [(i : I) → NonUnitalSemiring (f i)] :
NonUnitalSemiring ((i : I) → f i)
Equations
  • Pi.nonUnitalSemiring = let __src := Pi.nonUnitalNonAssocSemiring; let __src_1 := Pi.semigroupWithZero; NonUnitalSemiring.mk
instance Pi.nonAssocSemiring {I : Type u} {f : IType v} [(i : I) → NonAssocSemiring (f i)] :
NonAssocSemiring ((i : I) → f i)
Equations
  • Pi.nonAssocSemiring = let __src := Pi.nonUnitalNonAssocSemiring; let __src_1 := Pi.mulZeroOneClass; let __src_2 := Pi.addMonoidWithOne; NonAssocSemiring.mk
instance Pi.semiring {I : Type u} {f : IType v} [(i : I) → Semiring (f i)] :
Semiring ((i : I) → f i)
Equations
  • Pi.semiring = let __src := Pi.nonUnitalSemiring; let __src_1 := Pi.nonAssocSemiring; let __src_2 := Pi.monoidWithZero; Semiring.mk Monoid.npow
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
  • Pi.commSemiring = let __src := Pi.semiring; let __src_1 := Pi.commMonoid; CommSemiring.mk
instance Pi.nonUnitalNonAssocRing {I : Type u} {f : IType v} [(i : I) → NonUnitalNonAssocRing (f i)] :
NonUnitalNonAssocRing ((i : I) → f i)
Equations
  • Pi.nonUnitalNonAssocRing = let __src := Pi.addCommGroup; let __src_1 := Pi.nonUnitalNonAssocSemiring; NonUnitalNonAssocRing.mk
instance Pi.nonUnitalRing {I : Type u} {f : IType v} [(i : I) → NonUnitalRing (f i)] :
NonUnitalRing ((i : I) → f i)
Equations
  • Pi.nonUnitalRing = let __src := Pi.nonUnitalNonAssocRing; let __src_1 := Pi.nonUnitalSemiring; NonUnitalRing.mk
instance Pi.nonAssocRing {I : Type u} {f : IType v} [(i : I) → NonAssocRing (f i)] :
NonAssocRing ((i : I) → f i)
Equations
  • Pi.nonAssocRing = let __src := Pi.nonUnitalNonAssocRing; let __src_1 := Pi.nonAssocSemiring; let __src_2 := Pi.addGroupWithOne; NonAssocRing.mk
instance Pi.ring {I : Type u} {f : IType v} [(i : I) → Ring (f i)] :
Ring ((i : I) → f i)
Equations
  • Pi.ring = let __src := Pi.semiring; let __src_1 := Pi.addCommGroup; let __src_2 := Pi.addGroupWithOne; Ring.mk SubNegMonoid.zsmul
instance Pi.nonUnitalCommRing {I : Type u} {f : IType v} [(i : I) → NonUnitalCommRing (f i)] :
NonUnitalCommRing ((i : I) → f i)
Equations
  • Pi.nonUnitalCommRing = let __src := Pi.nonUnitalRing; let __src_1 := Pi.commSemigroup; NonUnitalCommRing.mk
instance Pi.commRing {I : Type u} {f : IType v} [(i : I) → CommRing (f i)] :
CommRing ((i : I) → f i)
Equations
  • Pi.commRing = let __src := Pi.ring; let __src_1 := Pi.commSemiring; CommRing.mk
@[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
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
  • One or more equations did not get rendered due to their size.
Instances For
    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)) :
    @[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
    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
    • One or more equations did not get rendered due to their size.
    Instances For
      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)) :
      @[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.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.constNonUnitalRingHom_apply (α : Type u_1) (β : Type u_2) [NonUnitalNonAssocSemiring β] (a : β) :
        ∀ (a_1 : α), (Pi.constNonUnitalRingHom α β) a a_1 = Function.const α a a_1
        def Pi.constNonUnitalRingHom (α : Type u_1) (β : Type u_2) [NonUnitalNonAssocSemiring β] :
        β →ₙ+* αβ

        Function.const as a NonUnitalRingHom.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem NonUnitalRingHom.compLeft_apply {α : Type u_1} {β : Type u_2} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) (I : Type u_3) (h : Iα) :
          ∀ (a : I), (NonUnitalRingHom.compLeft f I) h a = (f h) 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
          • One or more equations did not get rendered due to their size.
          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) :
            (Pi.evalRingHom f i) g = g i
            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
              Equations
              • =
              @[simp]
              theorem Pi.constRingHom_apply (α : Type u_1) (β : Type u_2) [NonAssocSemiring β] (a : β) :
              ∀ (a_1 : α), (Pi.constRingHom α β) a a_1 = Function.const α a a_1
              def Pi.constRingHom (α : Type u_1) (β : Type u_2) [NonAssocSemiring β] :
              β →+* αβ

              Function.const as a RingHom.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem RingHom.compLeft_apply {α : Type u_1} {β : Type u_2} [NonAssocSemiring α] [NonAssocSemiring β] (f : α →+* β) (I : Type u_3) (h : Iα) :
                ∀ (a : I), (RingHom.compLeft f I) h a = (f h) 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
                • One or more equations did not get rendered due to their size.
                Instances For