mathlib3documentation

algebra.algebra.pi

The R-algebra structure on families of R-algebras #

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

The R-algebra structure on Π i : I, A i when each A i is an R-algebra.

Main defintions #

• pi.algebra
• pi.eval_alg_hom
• pi.const_alg_hom
@[protected, instance]
def pi.algebra (I : Type u) {R : Type u_1} (f : I Type v) {r : comm_semiring R} [s : Π (i : I), semiring (f i)] [Π (i : I), (f i)] :
(Π (i : I), f i)
Equations
theorem pi.algebra_map_def (I : Type u) {R : Type u_1} (f : I Type v) {r : comm_semiring R} [s : Π (i : I), semiring (f i)] [Π (i : I), (f i)] (a : R) :
(Π (i : I), f i)) a = λ (i : I), (f i)) a
@[simp]
theorem pi.algebra_map_apply (I : Type u) {R : Type u_1} (f : I Type v) {r : comm_semiring R} [s : Π (i : I), semiring (f i)] [Π (i : I), (f i)] (a : R) (i : I) :
(Π (i : I), f i)) a i = (f i)) a
@[simp]
theorem pi.eval_alg_hom_apply {I : Type u} (R : Type u_1) (f : I Type v) {r : comm_semiring R} [Π (i : I), semiring (f i)] [Π (i : I), (f i)] (i : I) (f_1 : Π (i : I), f i) :
f i) f_1 = f_1 i
def pi.eval_alg_hom {I : Type u} (R : Type u_1) (f : I Type v) {r : comm_semiring R} [Π (i : I), semiring (f i)] [Π (i : I), (f i)] (i : I) :
(Π (i : I), f i) →ₐ[R] f i

function.eval as an alg_hom. The name matches pi.eval_ring_hom, pi.eval_monoid_hom, etc.

Equations
@[simp]
theorem pi.const_alg_hom_apply (R : Type u_1) (A : Type u_2) (B : Type u_3) [semiring B] [ B] (a : B) (ᾰ : A) :
A B) a =
def pi.const_alg_hom (R : Type u_1) (A : Type u_2) (B : Type u_3) [semiring B] [ B] :
B →ₐ[R] A B

function.const as an alg_hom. The name matches pi.const_ring_hom, pi.const_monoid_hom, etc.

Equations
@[simp]
theorem pi.const_ring_hom_eq_algebra_map (R : Type u_1) (A : Type u_2)  :
= (A R)

When R is commutative and permits an algebra_map, pi.const_ring_hom is equal to that map.

@[simp]
theorem pi.const_alg_hom_eq_algebra_of_id (R : Type u_1) (A : Type u_2)  :
R = (A R)
@[protected, instance]
def function.algebra {R : Type u_1} (I : Type u_2) (A : Type u_3) [semiring A] [ A] :
(I A)

A special case of pi.algebra for non-dependent types. Lean struggles to elaborate definitions elsewhere in the library without this,

Equations
• = (λ (ᾰ : I), A)
@[protected]
def alg_hom.comp_left {R : Type u} {A : Type v} {B : Type w} [semiring A] [semiring B] [ A] [ B] (f : A →ₐ[R] B) (I : Type u_1) :
(I A) →ₐ[R] I B

R-algebra homomorphism between the function spaces I → A and I → B, induced by an R-algebra homomorphism f between A and B.

Equations
@[simp]
theorem alg_hom.comp_left_apply {R : Type u} {A : Type v} {B : Type w} [semiring A] [semiring B] [ A] [ B] (f : A →ₐ[R] B) (I : Type u_1) (h : I A) (ᾰ : I) :
(f.comp_left I) h = (f h)
@[simp]
theorem alg_equiv.Pi_congr_right_apply {R : Type u_1} {ι : Type u_2} {A₁ : ι Type u_3} {A₂ : ι Type u_4} [Π (i : ι), semiring (A₁ i)] [Π (i : ι), semiring (A₂ i)] [Π (i : ι), (A₁ i)] [Π (i : ι), (A₂ i)] (e : Π (i : ι), A₁ i ≃ₐ[R] A₂ i) (x : Π (i : ι), A₁ i) (j : ι) :
j = (e j) (x j)
def alg_equiv.Pi_congr_right {R : Type u_1} {ι : Type u_2} {A₁ : ι Type u_3} {A₂ : ι Type u_4} [Π (i : ι), semiring (A₁ i)] [Π (i : ι), semiring (A₂ i)] [Π (i : ι), (A₁ i)] [Π (i : ι), (A₂ i)] (e : Π (i : ι), A₁ i ≃ₐ[R] A₂ i) :
(Π (i : ι), A₁ i) ≃ₐ[R] Π (i : ι), A₂ i

A family of algebra equivalences Π j, (A₁ j ≃ₐ A₂ j) generates a multiplicative equivalence between Π j, A₁ j and Π j, A₂ j.

This is the alg_equiv version of equiv.Pi_congr_right, and the dependent version of alg_equiv.arrow_congr.

Equations
@[simp]
theorem alg_equiv.Pi_congr_right_refl {R : Type u_1} {ι : Type u_2} {A : ι Type u_3} [Π (i : ι), semiring (A i)] [Π (i : ι), (A i)] :
@[simp]
theorem alg_equiv.Pi_congr_right_symm {R : Type u_1} {ι : Type u_2} {A₁ : ι Type u_3} {A₂ : ι Type u_4} [Π (i : ι), semiring (A₁ i)] [Π (i : ι), semiring (A₂ i)] [Π (i : ι), (A₁ i)] [Π (i : ι), (A₂ i)] (e : Π (i : ι), A₁ i ≃ₐ[R] A₂ i) :
= alg_equiv.Pi_congr_right (λ (i : ι), (e i).symm)
@[simp]
theorem alg_equiv.Pi_congr_right_trans {R : Type u_1} {ι : Type u_2} {A₁ : ι Type u_3} {A₂ : ι Type u_4} {A₃ : ι Type u_5} [Π (i : ι), semiring (A₁ i)] [Π (i : ι), semiring (A₂ i)] [Π (i : ι), semiring (A₃ i)] [Π (i : ι), (A₁ i)] [Π (i : ι), (A₂ i)] [Π (i : ι), (A₃ i)] (e₁ : Π (i : ι), A₁ i ≃ₐ[R] A₂ i) (e₂ : Π (i : ι), A₂ i ≃ₐ[R] A₃ i) :
= alg_equiv.Pi_congr_right (λ (i : ι), (e₁ i).trans (e₂ i))