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

• Pi.algebra
• Pi.evalAlgHom
• Pi.constAlgHom

instance Prod.algebra (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] : Algebra R (A × B)

Equations

• Prod.algebra R A B = let __src := Prod.instModule; let __src_1 := RingHom.prod (algebraMap R A) (algebraMap R B); Algebra.mk __src_1 ⋯ ⋯

@[simp]

theorem Prod.algebraMap_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (r : R) : (algebraMap R (A × B)) r = ((algebraMap R A) r, (algebraMap R B) r)

def AlgHom.fst (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] : A × B →ₐ[R] A

First projection as AlgHom.

Equations

• AlgHom.fst R A B = let __src := RingHom.fst A B; { toRingHom := __src, commutes' := ⋯ }

def AlgHom.snd (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] : A × B →ₐ[R] B

Second projection as AlgHom.

Equations

• AlgHom.snd R A B = let __src := RingHom.snd A B; { toRingHom := __src, commutes' := ⋯ }

@[simp]

theorem AlgHom.prod_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (f : A →ₐ[R] B) (g : A →ₐ[R] C) (x : A) : (AlgHom.prod f 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} [CommSemiring 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

• AlgHom.prod f g = let __src := RingHom.prod f.toRingHom g.toRingHom; { toRingHom := __src, commutes' := ⋯ }

theorem AlgHom.coe_prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (f : A →ₐ[R] B) (g : A →ₐ[R] C) : ⇑(AlgHom.prod f 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} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (f : A →ₐ[R] B) (g : A →ₐ[R] C) : AlgHom.comp (AlgHom.fst R B C) (AlgHom.prod f g) = f

@[simp]

theorem AlgHom.snd_prod {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (f : A →ₐ[R] B) (g : A →ₐ[R] C) : AlgHom.comp (AlgHom.snd R B C) (AlgHom.prod f g) = g

@[simp]

theorem AlgHom.prod_fst_snd {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] : AlgHom.prod (AlgHom.fst R A B) (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} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (f : A →ₐ[R] B × C) : AlgHom.prodEquiv.symm f = (AlgHom.comp (AlgHom.fst R B C) f, AlgHom.comp (AlgHom.snd R B C) f)

@[simp]

theorem AlgHom.prodEquiv_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (f : (A →ₐ[R] B) × (A →ₐ[R] C)) : AlgHom.prodEquiv f = AlgHom.prod f.1 f.2

def AlgHom.prodEquiv {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [CommSemiring 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

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