mathlib documentation

algebra.algebra.pi

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

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

Main defintions #

@[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), algebra R (f i)] :
algebra R (Π (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), algebra R (f i)] (a : R) :
(algebra_map R (Π (i : I), f i)) a = λ (i : I), (algebra_map R (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), algebra R (f i)] (a : R) (i : I) :
(algebra_map R (Π (i : I), f i)) a i = (algebra_map R (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), algebra R (f i)] (i : I) (f_1 : Π (i : I), f i) :
(pi.eval_alg_hom R 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), algebra R (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) [comm_semiring R] [semiring B] [algebra R B] (a : B) (ᾰ : A) :
(pi.const_alg_hom R A B) a = function.const A a
def pi.const_alg_hom (R : Type u_1) (A : Type u_2) (B : Type u_3) [comm_semiring R] [semiring B] [algebra R 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]

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) [comm_semiring R] :
@[protected, instance]
def function.algebra {R : Type u_1} (I : Type u_2) (A : Type u_3) [comm_semiring R] [semiring A] [algebra R A] :
algebra R (I A)

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

Equations
@[protected]
def alg_hom.comp_left {R : Type u} {A : Type v} {B : Type w} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R 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} [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R 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} [comm_semiring R] [Π (i : ι), semiring (A₁ i)] [Π (i : ι), semiring (A₂ i)] [Π (i : ι), algebra R (A₁ i)] [Π (i : ι), algebra R (A₂ i)] (e : Π (i : ι), A₁ i ≃ₐ[R] A₂ i) (x : Π (i : ι), A₁ i) (j : ι) :
(alg_equiv.Pi_congr_right e) x 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} [comm_semiring R] [Π (i : ι), semiring (A₁ i)] [Π (i : ι), semiring (A₂ i)] [Π (i : ι), algebra R (A₁ i)] [Π (i : ι), algebra R (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} [comm_semiring R] [Π (i : ι), semiring (A i)] [Π (i : ι), algebra R (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} [comm_semiring R] [Π (i : ι), semiring (A₁ i)] [Π (i : ι), semiring (A₂ i)] [Π (i : ι), algebra R (A₁ i)] [Π (i : ι), algebra R (A₂ i)] (e : Π (i : ι), A₁ i ≃ₐ[R] A₂ i) :
@[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} [comm_semiring R] [Π (i : ι), semiring (A₁ i)] [Π (i : ι), semiring (A₂ i)] [Π (i : ι), semiring (A₃ i)] [Π (i : ι), algebra R (A₁ i)] [Π (i : ι), algebra R (A₂ i)] [Π (i : ι), algebra R (A₃ i)] (e₁ : Π (i : ι), A₁ i ≃ₐ[R] A₂ i) (e₂ : Π (i : ι), A₂ i ≃ₐ[R] A₃ i) :