mathlib3 documentation

algebra.algebra.prod

The R-algebra structure on products 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 #

source
@[protected, instance]
def prod.algebra (R : Type u_1) (A : Type u_2) (B : Type u_3) [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] :
algebra R (A × B)
Equations
source
@[simp]
theorem prod.algebra_map_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] (r : R) :
⇑(algebra_map R (A × B)) r = (⇑(algebra_map R A) r, ⇑(algebra_map R B) r)
source
def alg_hom.fst (R : Type u_1) (A : Type u_2) (B : Type u_3) [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] :
A × B →ₐ[R] A

First projection as alg_hom.

Equations
source
def alg_hom.snd (R : Type u_1) (A : Type u_2) (B : Type u_3) [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] :
A × B →ₐ[R] B

Second projection as alg_hom.

Equations
source
def alg_hom.prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] [semiring C] [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
source
@[simp]
theorem alg_hom.prod_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] [semiring C] [algebra R C] (f : A →ₐ[R] B) (g : A →ₐ[R] C) (ᾰ : A) :
⇑(f.prod g) ᾰ = (f.to_ring_hom.prod g.to_ring_hom).to_fun ᾰ
source
theorem alg_hom.coe_prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] [semiring C] [algebra R C] (f : A →ₐ[R] B) (g : A →ₐ[R] C) :
⇑(f.prod g) = pi.prod ⇑f ⇑g
source
@[simp]
theorem alg_hom.fst_prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] [semiring C] [algebra R C] (f : A →ₐ[R] B) (g : A →ₐ[R] C) :
(alg_hom.fst R B C).comp (f.prod g) = f
source
@[simp]
theorem alg_hom.snd_prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] [semiring C] [algebra R C] (f : A →ₐ[R] B) (g : A →ₐ[R] C) :
(alg_hom.snd R B C).comp (f.prod g) = g
source
@[simp]
theorem alg_hom.prod_fst_snd {R : Type u_1} {A : Type u_2} {B : Type u_3} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] :
(alg_hom.fst R A B).prod (alg_hom.snd R A B) = 1
source
@[simp]
theorem alg_hom.prod_equiv_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] [semiring C] [algebra R C] (f : (A →ₐ[R] B) × (A →ₐ[R] C)) :
⇑alg_hom.prod_equiv f = f.fst.prod f.snd
source
@[simp]
theorem alg_hom.prod_equiv_symm_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] [semiring C] [algebra R C] (f : A →ₐ[R] B × C) :
⇑(alg_hom.prod_equiv.symm) f = ((alg_hom.fst R B C).comp f, (alg_hom.snd R B C).comp f)
source
def alg_hom.prod_equiv {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B] [semiring C] [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