Documentation

Mathlib.Algebra.Algebra.Prod

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 #

source
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
source
@[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)
source
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
Instances For
    source
    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
    Instances For
      source
      @[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) :
      (AlgHom.fst R A B) a = a.1
      source
      @[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) :
      (AlgHom.snd R A B) a = a.2
      source
      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
      • f.prod g = { toRingHom := f.prod g.toRingHom, commutes' := ⋯ }
      Instances For
        source
        @[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)
        source
        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) = Pi.prod ⇑f ⇑g
        source
        @[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.fst R B C).comp (f.prod g) = f
        source
        @[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.snd R B C).comp (f.prod g) = g
        source
        @[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.fst R A B).prod (AlgHom.snd R A B) = AlgHom.id R (A × B)
        source
        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)
        source
        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.
        Instances For
          source
          @[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 = f.1.prod f.2
          source
          @[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.fst R B C).comp f, (AlgHom.snd R B C).comp f)
          source
          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' := ⋯ }
          Instances For