# 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 definitions #

• Pi.algebra
• Pi.evalAlgHom
• Pi.constAlgHom
instance Pi.algebra (I : Type u) {R : Type u_1} (f : IType v) {r : } [s : (i : I) → Semiring (f i)] [(i : I) → Algebra R (f i)] :
Algebra R ((i : I) → f i)
Equations
theorem Pi.algebraMap_def (I : Type u) {R : Type u_1} (f : IType v) :
∀ {x : } [_s : (i : I) → Semiring (f i)] [inst : (i : I) → Algebra R (f i)] (a : R), (algebraMap R ((i : I) → f i)) a = fun (i : I) => (algebraMap R (f i)) a
@[simp]
theorem Pi.algebraMap_apply (I : Type u) {R : Type u_1} (f : IType v) :
∀ {x : } [_s : (i : I) → Semiring (f i)] [inst : (i : I) → Algebra R (f i)] (a : R) (i : I), (algebraMap R ((i : I) → f i)) a i = (algebraMap R (f i)) a
@[simp]
theorem Pi.evalAlgHom_apply {I : Type u} (R : Type u_1) (f : IType v) :
∀ {x : } [inst : (i : I) → Semiring (f i)] [inst_1 : (i : I) → Algebra R (f i)] (i : I) (f_1 : (i : I) → f i), () f_1 = f_1 i
def Pi.evalAlgHom {I : Type u} (R : Type u_1) (f : IType v) :
{x : } → [inst : (i : I) → Semiring (f i)] → [inst_1 : (i : I) → Algebra R (f i)] → (i : I) → ((i : I) → f i) →ₐ[R] f i

Function.eval as an AlgHom. The name matches Pi.evalRingHom, Pi.evalMonoidHom, etc.

Equations
• = let __src := ; { toFun := fun (f : (i : I) → f i) => f i, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
Instances For
@[simp]
theorem Pi.constAlgHom_apply (R : Type u_1) (A : Type u_2) (B : Type u_3) [] [] [Algebra R B] (a : B) :
∀ (a_1 : A), () a a_1 = Function.const A a a_1
def Pi.constAlgHom (R : Type u_1) (A : Type u_2) (B : Type u_3) [] [] [Algebra R B] :
B →ₐ[R] AB

Function.const as an AlgHom. The name matches Pi.constRingHom, Pi.constMonoidHom, etc.

Equations
• = let __src := ; { toFun := , map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
Instances For
@[simp]
theorem Pi.constRingHom_eq_algebraMap (R : Type u_1) (A : Type u_2) [] :
= algebraMap R (AR)

When R is commutative and permits an algebraMap, Pi.constRingHom is equal to that map.

@[simp]
theorem Pi.constAlgHom_eq_algebra_ofId (R : Type u_1) (A : Type u_2) [] :
= Algebra.ofId R (AR)
instance Function.algebra {R : Type u_1} (I : Type u_2) (A : Type u_3) [] [] [Algebra R A] :
Algebra R (IA)

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

Equations
@[simp]
theorem AlgHom.compLeft_apply {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (I : Type u_2) (h : IA) :
∀ (a : I), (f.compLeft I) h a = (f h) a
def AlgHom.compLeft {R : Type u} {A : Type v} {B : Type w} [] [] [] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (I : Type u_2) :
(IA) →ₐ[R] IB

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

Equations
• f.compLeft I = let __src := f.compLeft I; { toFun := fun (h : IA) => f h, map_one' := , map_mul' := , map_zero' := , map_add' := , commutes' := }
Instances For
@[simp]
theorem AlgEquiv.piCongrRight_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 : ι) → Algebra R (A₁ i)] [(i : ι) → Algebra R (A₂ i)] (e : (i : ι) → A₁ i ≃ₐ[R] A₂ i) (x : (i : ι) → A₁ i) (j : ι) :
x j = (e j) (x j)
def AlgEquiv.piCongrRight {R : Type u_1} {ι : Type u_2} {A₁ : ιType u_3} {A₂ : ιType u_4} [] [(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 ∀ i, (A₁ i ≃ₐ A₂ i) generates a multiplicative equivalence between ∀ i, A₁ i and ∀ i, A₂ i.

This is the AlgEquiv version of Equiv.piCongrRight, and the dependent version of AlgEquiv.arrowCongr.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem AlgEquiv.piCongrRight_refl {R : Type u_1} {ι : Type u_2} {A : ιType u_3} [] [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] :
(AlgEquiv.piCongrRight fun (i : ι) => AlgEquiv.refl) = AlgEquiv.refl
@[simp]
theorem AlgEquiv.piCongrRight_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 : ι) → Algebra R (A₁ i)] [(i : ι) → Algebra R (A₂ i)] (e : (i : ι) → A₁ i ≃ₐ[R] A₂ i) :
.symm = AlgEquiv.piCongrRight fun (i : ι) => (e i).symm
@[simp]
theorem AlgEquiv.piCongrRight_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 : ι) → 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) :
.trans = AlgEquiv.piCongrRight fun (i : ι) => (e₁ i).trans (e₂ i)