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
• AlgEquiv.prodUnique and AlgEquiv.uniqueProd

@[instance_reducible]

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 = { toSMul := Prod.instSMul, algebraMap := (algebraMap R A).prod (algebraMap R B), commutes' := ⋯, smul_def' := ⋯ }

@[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 = { toRingHom := RingHom.fst A B, 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 = { toRingHom := RingHom.snd A B, commutes' := ⋯ }

@[simp]

theorem AlgHom.fst_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] (a : A × B) : (fst R A B) a = a.1

@[simp]

theorem AlgHom.snd_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] (a : A × B) : (snd R A B) a = a.2

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 Function.prod of two morphisms is a morphism.

Equations

• f.prod g = { toRingHom := f.prod g.toRingHom, 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) : (f.prod g) x = (f x, g x)

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) : ⇑(f.prod g) = Function.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) : (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} [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) : (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} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] : (fst R A B).prod (snd R A B) = AlgHom.id R (A × B)

theorem AlgHom.prod_comp {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] {C' : Type u_5} [Semiring C'] [Algebra R C'] (f : A →ₐ[R] B) (g : B →ₐ[R] C) (g' : B →ₐ[R] C') : (g.prod g').comp f = (g.comp f).prod (g'.comp f)

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.

@[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) : prodEquiv.symm f = ((fst R B C).comp f, (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} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (f : (A →ₐ[R] B) × (A →ₐ[R] C)) : prodEquiv f = f.1.prod f.2

def AlgHom.prodMap {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] {D : Type u_5} [Semiring D] [Algebra R D] (f : A →ₐ[R] B) (g : C →ₐ[R] D) : A × C →ₐ[R] B × D

Prod.map of two algebra homomorphisms.

Equations

• f.prodMap g = { toRingHom := f.prodMap g.toRingHom, commutes' := ⋯ }

def AlgEquiv.prodCongr {R : Type u_1} [CommSemiring R] {S : Type u_5} {T : Type u_6} {A : Type u_7} {B : Type u_8} [Semiring A] [Semiring B] [Semiring S] [Semiring T] [Algebra R S] [Algebra R T] [Algebra R A] [Algebra R B] (l : S ≃ₐ[R] A) (r : T ≃ₐ[R] B) : (S × T) ≃ₐ[R] A × B

Product of algebra isomorphisms.

Equations

• l.prodCongr r = AlgEquiv.ofRingEquiv ⋯

@[simp]

theorem AlgEquiv.prodCongr_apply {R : Type u_1} [CommSemiring R] {S : Type u_5} {T : Type u_6} {A : Type u_7} {B : Type u_8} [Semiring A] [Semiring B] [Semiring S] [Semiring T] [Algebra R S] [Algebra R T] [Algebra R A] [Algebra R B] (l : S ≃ₐ[R] A) (r : T ≃ₐ[R] B) (x : S × T) : (l.prodCongr r) x = ((↑l).prodCongr ↑r) x

@[simp]

theorem AlgEquiv.prodCongr_symm_apply {R : Type u_1} [CommSemiring R] {S : Type u_5} {T : Type u_6} {A : Type u_7} {B : Type u_8} [Semiring A] [Semiring B] [Semiring S] [Semiring T] [Algebra R S] [Algebra R T] [Algebra R A] [Algebra R B] (l : S ≃ₐ[R] A) (r : T ≃ₐ[R] B) (x : A × B) : (l.prodCongr r).symm x = ((↑l).prodCongr ↑r).symm x

def AlgEquiv.prodUnique {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Unique B] : (A × B) ≃ₐ[R] A

Multiplying by the trivial algebra from the right does not change the structure. This is the AlgEquiv version of LinearEquiv.prodUnique and RingEquiv.prodZeroRing.symm.

Equations

• AlgEquiv.prodUnique = { toFun := Prod.fst, invFun := fun (x : A) => (x, 0), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem AlgEquiv.prodUnique_symm_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] [Unique B] (x : A) : prodUnique.symm x = (x, 0)

@[simp]

theorem AlgEquiv.prodUnique_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] [Unique B] (self : A × B) : prodUnique self = self.1

def AlgEquiv.uniqueProd {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] [Unique B] : (B × A) ≃ₐ[R] A

Multiplying by the trivial algebra from the left does not change the structure. This is the AlgEquiv version of LinearEquiv.uniqueProd and RingEquiv.zeroRingProd.symm.

Equations

• AlgEquiv.uniqueProd = { toFun := Prod.snd, invFun := fun (x : A) => (0, x), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem AlgEquiv.uniqueProd_symm_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] [Unique B] (x : A) : uniqueProd.symm x = (0, x)

@[simp]

theorem AlgEquiv.uniqueProd_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] [Unique B] (self : B × A) : uniqueProd self = self.2