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

The R-algebra structure on (i : I) → A i when each A i is an R-algebra.

## Main definitions #

• Prod.algebra
• AlgHom.fst
• AlgHom.snd
• AlgHom.prod
instance Prod.algebra (R : Type u_1) (A : Type u_2) (B : Type u_3) [] [] [Algebra R A] [] [Algebra R B] :
Algebra R (A × B)
Equations
@[simp]
theorem Prod.algebraMap_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [Algebra R A] [] [Algebra R B] (r : R) :
(algebraMap R (A × B)) r = (() r, () r)
def AlgHom.fst (R : Type u_1) (A : Type u_2) (B : Type u_3) [] [] [Algebra R A] [] [Algebra R B] :
A × B →ₐ[R] A

First projection as AlgHom.

Equations
• AlgHom.fst R A B = let __src := ; { toRingHom := __src, commutes' := }
Instances For
def AlgHom.snd (R : Type u_1) (A : Type u_2) (B : Type u_3) [] [] [Algebra R A] [] [Algebra R B] :
A × B →ₐ[R] B

Second projection as AlgHom.

Equations
• AlgHom.snd R A B = let __src := ; { toRingHom := __src, commutes' := }
Instances For
@[simp]
theorem AlgHom.prod_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [] [] [Algebra R A] [] [Algebra R B] [] [Algebra R C] (f : A →ₐ[R] B) (g : A →ₐ[R] C) (x : A) :
(f.prod g) x = (f x, g x)
def AlgHom.prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [] [] [Algebra R A] [] [Algebra R B] [] [Algebra R C] (f : A →ₐ[R] B) (g : A →ₐ[R] C) :
A →ₐ[R] B × C

The Pi.prod of two morphisms is a morphism.

Equations
• f.prod g = let __src := f.prod g.toRingHom; { toRingHom := __src, commutes' := }
Instances For
theorem AlgHom.coe_prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [] [] [Algebra R A] [] [Algebra R B] [] [Algebra R C] (f : A →ₐ[R] B) (g : A →ₐ[R] C) :
(f.prod g) = Pi.prod f g
@[simp]
theorem AlgHom.fst_prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [] [] [Algebra R A] [] [Algebra R B] [] [Algebra R C] (f : A →ₐ[R] B) (g : A →ₐ[R] C) :
(AlgHom.fst R B C).comp (f.prod g) = f
@[simp]
theorem AlgHom.snd_prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [] [] [Algebra R A] [] [Algebra R B] [] [Algebra R C] (f : A →ₐ[R] B) (g : A →ₐ[R] C) :
(AlgHom.snd R B C).comp (f.prod g) = g
@[simp]
theorem AlgHom.prod_fst_snd {R : Type u_1} {A : Type u_2} {B : Type u_3} [] [] [Algebra R A] [] [Algebra R B] :
(AlgHom.fst R A B).prod (AlgHom.snd R A B) = 1
@[simp]
theorem AlgHom.prodEquiv_symm_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [] [] [Algebra R A] [] [Algebra R B] [] [Algebra R C] (f : A →ₐ[R] B × C) :
AlgHom.prodEquiv.symm f = ((AlgHom.fst R B C).comp f, (AlgHom.snd R B C).comp f)
@[simp]
theorem AlgHom.prodEquiv_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [] [] [Algebra R A] [] [Algebra R B] [] [Algebra R C] (f : (A →ₐ[R] B) × (A →ₐ[R] C)) :
AlgHom.prodEquiv f = f.1.prod f.2
def AlgHom.prodEquiv {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [] [] [Algebra R A] [] [Algebra R B] [] [Algebra R C] :
(A →ₐ[R] B) × (A →ₐ[R] C) (A →ₐ[R] B × C)

Taking the product of two maps with the same domain is equivalent to taking the product of their codomains.

Equations
• One or more equations did not get rendered due to their size.
Instances For