# Documentation

Mathlib.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 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)
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 => ↑(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 : (i : I) → f i), ↑() f = f 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.

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 : A), ↑() a a =
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.

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,

@[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), ↑() 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.

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.

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) :
@[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) :
= AlgEquiv.piCongrRight fun i => AlgEquiv.trans (e₁ i) (e₂ i)