algebra.ring.pi

# Pi instances for ring #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[protected, instance]
def pi.distrib {I : Type u} {f : I Type v} [Π (i : I), distrib (f i)] :
distrib (Π (i : I), f i)
Equations
@[protected, instance]
def pi.non_unital_non_assoc_semiring {I : Type u} {f : I Type v} [Π (i : I), ] :
Equations
@[protected, instance]
def pi.non_unital_semiring {I : Type u} {f : I Type v} [Π (i : I), non_unital_semiring (f i)] :
non_unital_semiring (Π (i : I), f i)
Equations
@[protected, instance]
def pi.non_assoc_semiring {I : Type u} {f : I Type v} [Π (i : I), non_assoc_semiring (f i)] :
non_assoc_semiring (Π (i : I), f i)
Equations
@[protected, instance]
def pi.semiring {I : Type u} {f : I Type v} [Π (i : I), semiring (f i)] :
semiring (Π (i : I), f i)
Equations
@[protected, instance]
def pi.non_unital_comm_semiring {I : Type u} {f : I Type v} [Π (i : I), ] :
Equations
@[protected, instance]
def pi.comm_semiring {I : Type u} {f : I Type v} [Π (i : I), comm_semiring (f i)] :
comm_semiring (Π (i : I), f i)
Equations
@[protected, instance]
def pi.non_unital_non_assoc_ring {I : Type u} {f : I Type v} [Π (i : I), ] :
Equations
@[protected, instance]
def pi.non_unital_ring {I : Type u} {f : I Type v} [Π (i : I), non_unital_ring (f i)] :
non_unital_ring (Π (i : I), f i)
Equations
@[protected, instance]
def pi.non_assoc_ring {I : Type u} {f : I Type v} [Π (i : I), non_assoc_ring (f i)] :
non_assoc_ring (Π (i : I), f i)
Equations
@[protected, instance]
def pi.ring {I : Type u} {f : I Type v} [Π (i : I), ring (f i)] :
ring (Π (i : I), f i)
Equations
@[protected, instance]
def pi.non_unital_comm_ring {I : Type u} {f : I Type v} [Π (i : I), non_unital_comm_ring (f i)] :
non_unital_comm_ring (Π (i : I), f i)
Equations
@[protected, instance]
def pi.comm_ring {I : Type u} {f : I Type v} [Π (i : I), comm_ring (f i)] :
comm_ring (Π (i : I), f i)
Equations
@[simp]
theorem pi.non_unital_ring_hom_to_fun {I : Type u} {f : I Type v} {γ : Type w} [Π (i : I), ] (g : Π (i : I), γ →ₙ+* f i) (x : γ) (b : I) :
b = (g b) x
@[protected]
def pi.non_unital_ring_hom {I : Type u} {f : I Type v} {γ : Type w} [Π (i : I), ] (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.non_unital_ring_hom f : γ →+* Π a, β a given by pi.non_unital_ring_hom f x b = f b x.

Equations
theorem pi.non_unital_ring_hom_injective {I : Type u} {f : I Type v} {γ : Type w} [nonempty I] [Π (i : I), ] (g : Π (i : I), γ →ₙ+* f i) (hg : (i : I), function.injective (g i)) :
@[protected]
def pi.ring_hom {I : Type u} {f : I Type v} {γ : Type w} [Π (i : I), non_assoc_semiring (f i)] (g : Π (i : I), γ →+* f i) :
γ →+* Π (i : I), f i

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

Equations
@[simp]
theorem pi.ring_hom_apply {I : Type u} {f : I Type v} {γ : Type w} [Π (i : I), non_assoc_semiring (f i)] (g : Π (i : I), γ →+* f i) (x : γ) (b : I) :
(pi.ring_hom g) x b = (g b) x
theorem pi.ring_hom_injective {I : Type u} {f : I Type v} {γ : Type w} [nonempty I] [Π (i : I), non_assoc_semiring (f i)] (g : Π (i : I), γ →+* f i) (hg : (i : I), function.injective (g i)) :
def pi.eval_non_unital_ring_hom {I : Type u} (f : I Type v) [Π (i : 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 non_unital_ring_hom.

Equations
@[simp]
theorem pi.eval_non_unital_ring_hom_to_fun {I : Type u} (f : I Type v) [Π (i : I), ] (i : I) (ᾰ : Π (i : I), f i) :
= i).to_fun
def pi.const_non_unital_ring_hom (α : Type u_1) (β : Type u_2)  :
β →ₙ+* α β

function.const as a non_unital_ring_hom.

Equations
@[simp]
theorem pi.const_non_unital_ring_hom_to_fun (α : Type u_1) (β : Type u_2) (a : β) (ᾰ : α) :
=
@[protected]
def non_unital_ring_hom.comp_left {α : Type u_1} {β : Type u_2} (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
@[simp]
theorem non_unital_ring_hom.comp_left_to_fun {α : Type u_1} {β : Type u_2} (f : α →ₙ+* β) (I : Type u_3) (h : I α) (ᾰ : I) :
(f.comp_left I) h = (f h)
@[simp]
theorem pi.eval_ring_hom_apply {I : Type u} (f : I Type v) [Π (i : I), non_assoc_semiring (f i)] (i : I) (ᾰ : Π (i : I), f i) :
i) = i).to_fun
def pi.eval_ring_hom {I : Type u} (f : I Type v) [Π (i : I), non_assoc_semiring (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 ring_hom.

Equations
@[simp]
theorem pi.const_ring_hom_apply (α : Type u_1) (β : Type u_2) (a : β) (ᾰ : α) :
β) a =
def pi.const_ring_hom (α : Type u_1) (β : Type u_2)  :
β →+* α β

function.const as a ring_hom.

Equations
@[protected]
def ring_hom.comp_left {α : Type u_1} {β : Type u_2} (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
@[simp]
theorem ring_hom.comp_left_apply {α : Type u_1} {β : Type u_2} (f : α →+* β) (I : Type u_3) (h : I α) (ᾰ : I) :
(f.comp_left I) h = (f h)