Pi instances for ring #
This file defines instances for ring, semiring and related structures on Pi Types
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 ⋯ ⋯
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 ⋯ ⋯
instance
Pi.addMonoidWithOne
{I : Type u}
{f : I → Type v}
[(i : I) → AddMonoidWithOne (f i)]
:
AddMonoidWithOne ((i : I) → f i)
Equations
- Pi.addMonoidWithOne = AddMonoidWithOne.mk ⋯ ⋯
instance
Pi.addGroupWithOne
{I : Type u}
{f : I → Type v}
[(i : I) → AddGroupWithOne (f i)]
:
AddGroupWithOne ((i : I) → f i)
Equations
- Pi.addGroupWithOne = let __spread.0 := Pi.addGroup; let __spread.1 := Pi.addMonoidWithOne; AddGroupWithOne.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
instance
Pi.nonUnitalNonAssocSemiring
{I : Type u}
{f : I → Type 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 : 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 ⋯
instance
Pi.nonAssocSemiring
{I : Type u}
{f : I → Type 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 : I → Type 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 : 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 ⋯
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 ⋯
instance
Pi.nonUnitalNonAssocRing
{I : Type u}
{f : I → Type 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 : 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 ⋯
instance
Pi.nonAssocRing
{I : Type u}
{f : I → Type 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.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 ⋯
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 ⋯
@[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
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
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))
:
@[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
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
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))
:
@[simp]
theorem
Pi.evalNonUnitalRingHom_apply
{I : Type u}
(f : I → Type v)
[(i : I) → NonUnitalNonAssocSemiring (f i)]
(i : I)
(g : (i : I) → f i)
:
(Pi.evalNonUnitalRingHom f i) g = g i
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
- Pi.evalNonUnitalRingHom f i = let __src := Pi.evalMulHom f i; let __src_1 := Pi.evalAddMonoidHom f i; { toMulHom := __src, map_zero' := ⋯, map_add' := ⋯ }
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 : I → Type 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 : 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
- Pi.evalRingHom f i = let __src := Pi.evalMonoidHom f i; let __src_1 := Pi.evalAddMonoidHom f i; { toMonoidHom := __src, map_zero' := ⋯, map_add' := ⋯ }
Instances For
instance
instRingHomSurjectiveForAllSemiringEvalRingHomToNonAssocSemiring
{I : Type u}
(f : I → Type u_1)
[(i : I) → Semiring (f i)]
(i : I)
:
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
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.