Pi instances for ring #

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

source

instance Pi.distrib {I : Type u} {f : I → Type v} [(i : I) → Distrib (f i)] :

Distrib ((i : I) → f i)

Equations

Pi.distrib = Distrib.mk (_ : ∀ (a b c : (i : I) → f i), a * (b + c) = a * b + a * c) (_ : ∀ (a b c : (i : I) → f i), (a + b) * c = a * c + b * c)

source

instance Pi.hasDistribNeg {I : Type u} {f : I → Type v} [(i : I) → Mul (f i)] [(i : I) → HasDistribNeg (f i)] :

HasDistribNeg ((i : I) → f i)

Equations

Pi.hasDistribNeg = HasDistribNeg.mk (_ : ∀ (x x_1 : (i : I) → f i), -x * x_1 = -(x * x_1)) (_ : ∀ (x x_1 : (i : I) → f i), x * -x_1 = -(x * x_1))

source

instance Pi.nonUnitalNonAssocSemiring {I : Type u} {f : I → Type v} [(i : I) → NonUnitalNonAssocSemiring (f i)] :

NonUnitalNonAssocSemiring ((i : I) → f i)

Equations

One or more equations did not get rendered due to their size.

source

instance Pi.nonUnitalSemiring {I : Type u} {f : I → Type 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 (_ : ∀ (a b c : (i : I) → f i), a * b * c = a * (b * c))

source

instance Pi.nonAssocSemiring {I : Type u} {f : I → Type v} [(i : I) → NonAssocSemiring (f i)] :

NonAssocSemiring ((i : I) → f i)

Equations

One or more equations did not get rendered due to their size.

source

instance Pi.semiring {I : Type u} {f : I → Type v} [(i : I) → Semiring (f i)] :

Semiring ((i : I) → f i)

Equations

One or more equations did not get rendered due to their size.

source

instance Pi.nonUnitalCommSemiring {I : Type u} {f : I → Type v} [(i : I) → NonUnitalCommSemiring (f i)] :

NonUnitalCommSemiring ((i : I) → f i)

Equations

Pi.nonUnitalCommSemiring = let src := Pi.nonUnitalSemiring; let src_1 := Pi.commSemigroup; NonUnitalCommSemiring.mk (_ : ∀ (a b : (i : I) → f i), a * b = b * a)

source

instance Pi.commSemiring {I : Type u} {f : I → Type 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 (_ : ∀ (a b : (i : I) → f i), a * b = b * a)

source

instance Pi.nonUnitalNonAssocRing {I : Type u} {f : I → Type v} [(i : I) → NonUnitalNonAssocRing (f i)] :

NonUnitalNonAssocRing ((i : I) → f i)

Equations

One or more equations did not get rendered due to their size.

source

instance Pi.nonUnitalRing {I : Type u} {f : I → Type 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 (_ : ∀ (a b c : (i : I) → f i), a * b * c = a * (b * c))

source

instance Pi.nonAssocRing {I : Type u} {f : I → Type v} [(i : I) → NonAssocRing (f i)] :

NonAssocRing ((i : I) → f i)

Equations

One or more equations did not get rendered due to their size.

source

instance Pi.ring {I : Type u} {f : I → Type 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 (_ : ∀ (a : (i : I) → f i), -a + a = 0)

source

instance Pi.nonUnitalCommRing {I : Type u} {f : I → Type 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 (_ : ∀ (a b : (i : I) → f i), a * b = b * a)

source

instance Pi.commRing {I : Type u} {f : I → Type 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 (_ : ∀ (a b : (i : I) → f i), a * b = b * a)

source

@[simp]

theorem Pi.nonUnitalRingHom_apply {I : Type u} {f : I → Type 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

source

def Pi.nonUnitalRingHom {I : Type u} {f : I → Type 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

source

theorem Pi.nonUnitalRingHom_injective {I : Type u} {f : I → Type v} {γ : Type w} [Nonempty I] [(i : I) → NonUnitalNonAssocSemiring (f i)] [NonUnitalNonAssocSemiring γ] (g : (i : I) → γ →ₙ+* f i) (hg : ∀ (i : I), Function.Injective ↑(g i)) :

Function.Injective ↑(Pi.nonUnitalRingHom g)

source

@[simp]

theorem Pi.ringHom_apply {I : Type u} {f : I → Type 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

source

def Pi.ringHom {I : Type u} {f : I → Type 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

source

theorem Pi.ringHom_injective {I : Type u} {f : I → Type v} {γ : Type w} [Nonempty I] [(i : I) → NonAssocSemiring (f i)] [NonAssocSemiring γ] (g : (i : I) → γ →+* f i) (hg : ∀ (i : I), Function.Injective ↑(g i)) :

Function.Injective ↑(Pi.ringHom g)

source

@[simp]

theorem Pi.evalNonUnitalRingHom_apply {I : Type u} (f : I → Type v) [(i : I) → NonUnitalNonAssocSemiring (f i)] (i : I) :

∀ (a : (i : I) → f i), ↑(Pi.evalNonUnitalRingHom f i) a = MulHom.toFun (Pi.evalMulHom f i) a

source

def Pi.evalNonUnitalRingHom {I : Type u} (f : I → Type 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

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem Pi.constNonUnitalRingHom_apply (α : Type u_1) (β : Type u_2) [NonUnitalNonAssocSemiring β] (a : β) :

∀ (a : α), ↑(Pi.constNonUnitalRingHom α β) a a = Function.const α a a

source

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

source

@[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

source

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

source

@[simp]

theorem Pi.evalRingHom_apply {I : Type u} (f : I → Type v) [(i : I) → NonAssocSemiring (f i)] (i : I) (g : (i : I) → f i) :

↑(Pi.evalRingHom f i) g = g i

source

def Pi.evalRingHom {I : Type u} (f : I → Type 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

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem Pi.constRingHom_apply (α : Type u_1) (β : Type u_2) [NonAssocSemiring β] (a : β) :

∀ (a : α), ↑(Pi.constRingHom α β) a a = Function.const α a a

source

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

source

@[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

source

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