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 = { mul := fun (x1 x2 : (i : I) → f i) => x1 * x2, add := fun (x1 x2 : (i : I) → f i) => x1 + x2, left_distrib := ⋯, right_distrib := ⋯ }

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 = { toInvolutiveNeg := Pi.involutiveNeg, neg_mul := ⋯, mul_neg := ⋯ }

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

Equations

• Pi.addMonoidWithOne = { natCast := fun (n : ℕ) (x : I) => ↑n, toAddMonoid := Pi.addMonoid, toOne := Pi.instOne, natCast_zero := ⋯, natCast_succ := ⋯ }

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

Equations

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

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.

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

Equations

• Pi.nonUnitalSemiring = { toNonUnitalNonAssocSemiring := Pi.nonUnitalNonAssocSemiring, mul_assoc := ⋯ }

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.

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.

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

Equations

• Pi.nonUnitalCommSemiring = { toNonUnitalSemiring := Pi.nonUnitalSemiring, mul_comm := ⋯ }

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

Equations

• Pi.commSemiring = { toSemiring := Pi.semiring, mul_comm := ⋯ }

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

Equations

• Pi.nonUnitalNonAssocRing = { toAddCommGroup := Pi.addCommGroup, toMul := Pi.nonUnitalNonAssocSemiring.toMul, left_distrib := ⋯, right_distrib := ⋯, zero_mul := ⋯, mul_zero := ⋯ }

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

Equations

• Pi.nonUnitalRing = { toNonUnitalNonAssocRing := Pi.nonUnitalNonAssocRing, mul_assoc := ⋯ }

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.

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

Equations

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

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

Equations

• Pi.nonUnitalCommRing = { toNonUnitalRing := Pi.nonUnitalRing, mul_comm := ⋯ }

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

Equations

• Pi.commRing = { toRing := Pi.ring, mul_comm := ⋯ }

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

• Pi.nonUnitalRingHom g = { toFun := fun (x : γ) (b : I) => (g b) x, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

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

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)

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

• Pi.ringHom g = { toFun := fun (x : γ) (b : I) => (g b) x, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

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

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)

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 = { toMulHom := Pi.evalMulHom f i, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

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

def Pi.constNonUnitalRingHom (α : Type u_1) (β : Type u_2) [NonUnitalNonAssocSemiring β] : β →ₙ+* α → β

Function.const as a NonUnitalRingHom.

Equations

• Pi.constNonUnitalRingHom α β = { toFun := Function.const α, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

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

• f.compLeft I = { toFun := fun (h : I → α) => ⇑f ∘ h, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[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 : 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 = { toMonoidHom := Pi.evalMonoidHom f i, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Pi.evalRingHom_apply {I : Type u} (f : I → Type 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 : I → Type u_1) [(i : I) → Semiring (f i)] (i : I) : RingHomSurjective (Pi.evalRingHom f i)

def Pi.constRingHom (α : Type u_1) (β : Type u_2) [NonAssocSemiring β] : β →+* α → β

Function.const as a RingHom.

Equations

• Pi.constRingHom α β = { toFun := Function.const α, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

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

• f.compLeft I = { toFun := fun (h : I → α) => ⇑f ∘ h, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

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