mathlib3 documentation

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

source
@[protected, instance]
def pi.distrib {I : Type u} {f : I → Type v} [Π (i : I), distrib (f i)] :
distrib (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.non_unital_non_assoc_semiring {I : Type u} {f : I → Type v} [Π (i : I), non_unital_non_assoc_semiring (f i)] :
non_unital_non_assoc_semiring (Π (i : I), f i)
Equations
source
@[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
source
@[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
source
@[protected, instance]
def pi.semiring {I : Type u} {f : I → Type v} [Π (i : I), semiring (f i)] :
semiring (Π (i : I), f i)
Equations
source
@[protected, instance]
def pi.non_unital_comm_semiring {I : Type u} {f : I → Type v} [Π (i : I), non_unital_comm_semiring (f i)] :
non_unital_comm_semiring (Π (i : I), f i)
Equations
source
@[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
source
@[protected, instance]
def pi.non_unital_non_assoc_ring {I : Type u} {f : I → Type v} [Π (i : I), non_unital_non_assoc_ring (f i)] :
non_unital_non_assoc_ring (Π (i : I), f i)
Equations
source
@[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
source
@[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
source
@[protected, instance]
def pi.ring {I : Type u} {f : I → Type v} [Π (i : I), ring (f i)] :
ring (Π (i : I), f i)
Equations
source
@[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
source
@[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
source
@[simp]
theorem pi.non_unital_ring_hom_to_fun {I : Type u} {f : I → Type v} {γ : Type w} [Π (i : I), non_unital_non_assoc_semiring (f i)] [non_unital_non_assoc_semiring γ] (g : Π (i : I), γ →ₙ+* f i) (x : γ) (b : I) :
⇑(pi.non_unital_ring_hom g) x b = ⇑(g b) x
source
@[protected]
def pi.non_unital_ring_hom {I : Type u} {f : I → Type v} {γ : Type w} [Π (i : I), non_unital_non_assoc_semiring (f i)] [non_unital_non_assoc_semiring γ] (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
source
theorem pi.non_unital_ring_hom_injective {I : Type u} {f : I → Type v} {γ : Type w} [nonempty I] [Π (i : I), non_unital_non_assoc_semiring (f i)] [non_unital_non_assoc_semiring γ] (g : Π (i : I), γ →ₙ+* f i) (hg : ∀ (i : I), function.injective ⇑(g i)) :
function.injective ⇑(pi.non_unital_ring_hom g)
source
@[protected]
def pi.ring_hom {I : Type u} {f : I → Type v} {γ : Type w} [Π (i : I), non_assoc_semiring (f i)] [non_assoc_semiring γ] (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
source
@[simp]
theorem pi.ring_hom_apply {I : Type u} {f : I → Type v} {γ : Type w} [Π (i : I), non_assoc_semiring (f i)] [non_assoc_semiring γ] (g : Π (i : I), γ →+* f i) (x : γ) (b : I) :
⇑(pi.ring_hom g) x b = ⇑(g b) x
source
theorem pi.ring_hom_injective {I : Type u} {f : I → Type v} {γ : Type w} [nonempty I] [Π (i : I), non_assoc_semiring (f i)] [non_assoc_semiring γ] (g : Π (i : I), γ →+* f i) (hg : ∀ (i : I), function.injective ⇑(g i)) :
function.injective ⇑(pi.ring_hom g)
source
def pi.eval_non_unital_ring_hom {I : Type u} (f : I → Type v) [Π (i : I), non_unital_non_assoc_semiring (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 non_unital_ring_hom.

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

function.const as a non_unital_ring_hom.

Equations
source
@[simp]
theorem pi.const_non_unital_ring_hom_to_fun (α : Type u_1) (β : Type u_2) [non_unital_non_assoc_semiring β] (a : β) (ᾰ : α) :
⇑(pi.const_non_unital_ring_hom α β) a ᾰ = function.const α a ᾰ
source
@[protected]
def non_unital_ring_hom.comp_left {α : Type u_1} {β : Type u_2} [non_unital_non_assoc_semiring α] [non_unital_non_assoc_semiring β] (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
source
@[simp]
theorem non_unital_ring_hom.comp_left_to_fun {α : Type u_1} {β : Type u_2} [non_unital_non_assoc_semiring α] [non_unital_non_assoc_semiring β] (f : α →ₙ+* β) (I : Type u_3) (h : I → α) (ᾰ : I) :
⇑(f.comp_left I) h ᾰ = (⇑f ∘ h) ᾰ
source
@[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) :
⇑(pi.eval_ring_hom f i) ᾰ = (pi.eval_monoid_hom f i).to_fun ᾰ
source
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
source
@[simp]
theorem pi.const_ring_hom_apply (α : Type u_1) (β : Type u_2) [non_assoc_semiring β] (a : β) (ᾰ : α) :
⇑(pi.const_ring_hom α β) a ᾰ = function.const α a ᾰ
source
def pi.const_ring_hom (α : Type u_1) (β : Type u_2) [non_assoc_semiring β] :
β →+* α → β

function.const as a ring_hom.

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