Mathlib.Algebra.Algebra.Prod

Prod.algebra instance

: Algebra R (A × B)

Full source

instance algebra : Algebra R (A × B) where
  algebraMap := RingHom.prod (algebraMap R A) (algebraMap R B)
  commutes' := by
    rintro r ⟨a, b⟩
    dsimp
    rw [commutes r a, commutes r b]
  smul_def' := by
    rintro r ⟨a, b⟩
    dsimp
    rw [Algebra.smul_def r a, Algebra.smul_def r b]

$R$-Algebra Structure on Product of $R$-Algebras

Informal description

For any commutative semiring $R$ and $R$-algebras $A$ and $B$, the product $A \times B$ is also an $R$-algebra with componentwise operations and algebra structure map given by $r \mapsto (r \cdot 1_A, r \cdot 1_B)$.

Prod.algebraMap_apply theorem

(r : R) : algebraMap R (A × B) r = (algebraMap R A r, algebraMap R B r)

Full source

@[simp]
theorem algebraMap_apply (r : R) : algebraMap R (A × B) r = (algebraMap R A r, algebraMap R B r) :=
  rfl

Componentwise Algebra Structure Map on Product Algebra

Informal description

For any commutative semiring $R$ and $R$-algebras $A$ and $B$, the algebra structure map on the product algebra $A \times B$ satisfies \[ \text{algebraMap}_R^{A \times B}(r) = (\text{algebraMap}_R^A(r), \text{algebraMap}_R^B(r)) \] for all $r \in R$, where $\text{algebraMap}_R^A$ and $\text{algebraMap}_R^B$ are the algebra structure maps of $A$ and $B$ respectively.

AlgHom.fst definition

: A × B →ₐ[R] A

Full source

/-- First projection as `AlgHom`. -/
def fst : A × BA × B →ₐ[R] A :=
  { RingHom.fst A B with commutes' := fun _r => rfl }

First projection $R$-algebra homomorphism

Informal description

The first projection map from the product $R$-algebra $A \times B$ to $A$, which is an $R$-algebra homomorphism. For any element $(a, b) \in A \times B$, it maps to $a \in A$, and it commutes with the algebra structure map, i.e., for any $r \in R$, the projection of the scalar multiplication $r \cdot (1_A, 1_B)$ is equal to $r \cdot 1_A$.

AlgHom.snd definition

: A × B →ₐ[R] B

Full source

/-- Second projection as `AlgHom`. -/
def snd : A × BA × B →ₐ[R] B :=
  { RingHom.snd A B with commutes' := fun _r => rfl }

Second projection algebra homomorphism

Informal description

The second projection as an algebra homomorphism from the product algebra $A \times B$ to $B$, where $A$ and $B$ are $R$-algebras. This homomorphism maps each pair $(a, b)$ to its second component $b$ and preserves the $R$-algebra structure.

AlgHom.fst_apply theorem

(a) : fst R A B a = a.1

Full source

@[simp]
theorem fst_apply (a) : fst R A B a = a.1 := rfl

First projection of product algebra equals first component

Informal description

For any element $a = (a_1, a_2)$ in the product $R$-algebra $A \times B$, the first projection algebra homomorphism $\text{fst}_{R,A,B}$ satisfies $\text{fst}_{R,A,B}(a) = a_1$.

AlgHom.snd_apply theorem

(a) : snd R A B a = a.2

Full source

@[simp]
theorem snd_apply (a) : snd R A B a = a.2 := rfl

Second projection homomorphism evaluation: $\text{snd}(a) = a_2$

Informal description

For any element $a = (a_1, a_2)$ in the product $R$-algebra $A \times B$, the second projection algebra homomorphism $\text{snd} \colon A \times B \to B$ satisfies $\text{snd}(a) = a_2$.

AlgHom.prod definition

(f : A →ₐ[R] B) (g : A →ₐ[R] C) : A →ₐ[R] B × C

Full source

/-- The `Pi.prod` of two morphisms is a morphism. -/
@[simps!]
def prod (f : A →ₐ[R] B) (g : A →ₐ[R] C) : A →ₐ[R] B × C :=
  { f.toRingHom.prod g.toRingHom with
    commutes' := fun r => by
      simp only [toRingHom_eq_coe, RingHom.toFun_eq_coe, RingHom.prod_apply, coe_toRingHom,
        commutes, Prod.algebraMap_apply] }

Product of $R$-algebra homomorphisms

Informal description

Given two $R$-algebra homomorphisms $f \colon A \to B$ and $g \colon A \to C$, the function $f \times g \colon A \to B \times C$ defined by $(f \times g)(x) = (f(x), g(x))$ is also an $R$-algebra homomorphism.

AlgHom.coe_prod theorem

(f : A →ₐ[R] B) (g : A →ₐ[R] C) : ⇑(f.prod g) = Pi.prod f g

Full source

theorem coe_prod (f : A →ₐ[R] B) (g : A →ₐ[R] C) : ⇑(f.prod g) = Pi.prod f g :=
  rfl

Underlying Function of Product Homomorphism Equals Component-wise Product

Informal description

For any two $R$-algebra homomorphisms $f \colon A \to B$ and $g \colon A \to C$, the underlying function of the product homomorphism $f \times g \colon A \to B \times C$ is equal to the component-wise product of the functions $f$ and $g$, i.e., $(f \times g)(a) = (f(a), g(a))$ for all $a \in A$.

AlgHom.fst_prod theorem

(f : A →ₐ[R] B) (g : A →ₐ[R] C) : (fst R B C).comp (prod f g) = f

Full source

@[simp]
theorem fst_prod (f : A →ₐ[R] B) (g : A →ₐ[R] C) : (fst R B C).comp (prod f g) = f := by ext; rfl

First projection of product homomorphism equals original homomorphism

Informal description

For any $R$-algebra homomorphisms $f \colon A \to B$ and $g \colon A \to C$, the composition of the first projection homomorphism $\mathrm{fst} \colon B \times C \to B$ with the product homomorphism $f \times g \colon A \to B \times C$ equals $f$, i.e., $\mathrm{fst} \circ (f \times g) = f$.

AlgHom.snd_prod theorem

(f : A →ₐ[R] B) (g : A →ₐ[R] C) : (snd R B C).comp (prod f g) = g

Full source

@[simp]
theorem snd_prod (f : A →ₐ[R] B) (g : A →ₐ[R] C) : (snd R B C).comp (prod f g) = g := by ext; rfl

Second projection of product homomorphism equals second factor

Informal description

For any $R$-algebra homomorphisms $f \colon A \to B$ and $g \colon A \to C$, the composition of the second projection homomorphism $\mathrm{snd} \colon B \times C \to C$ with the product homomorphism $f \times g \colon A \to B \times C$ equals $g$. In other words, $\mathrm{snd} \circ (f \times g) = g$.

AlgHom.prod_fst_snd theorem

: prod (fst R A B) (snd R A B) = AlgHom.id R _

Full source

@[simp]
theorem prod_fst_snd : prod (fst R A B) (snd R A B) = AlgHom.id R _ := rfl

Product of Projections is Identity on Product Algebra

Informal description

The product of the first and second projection $R$-algebra homomorphisms from $A \times B$ to $A$ and $A \times B$ to $B$ respectively is equal to the identity $R$-algebra homomorphism on $A \times B$. In other words, for any element $(a, b) \in A \times B$, we have $(\pi_1(a, b), \pi_2(a, b)) = (a, b)$, where $\pi_1$ and $\pi_2$ are the first and second projection maps.

AlgHom.prod_comp theorem

 {C' : Type*} [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)

Full source

theorem prod_comp {C' : Type*} [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) := rfl

Composition of Product of $R$-Algebra Homomorphisms

Informal description

Let $R$ be a commutative semiring, and let $A$, $B$, $C$, and $C'$ be $R$-algebras. Given $R$-algebra homomorphisms $f \colon A \to B$, $g \colon B \to C$, and $g' \colon B \to C'$, the composition of the product homomorphism $g \times g'$ with $f$ is equal to the product of the compositions $g \circ f$ and $g' \circ f$, i.e., $$(g \times g') \circ f = (g \circ f) \times (g' \circ f).$$

AlgHom.prodEquiv definition

: (A →ₐ[R] B) × (A →ₐ[R] C) ≃ (A →ₐ[R] B × C)

Full source

/-- Taking the product of two maps with the same domain is equivalent to taking the product of
their codomains. -/
@[simps]
def prodEquiv : (A →ₐ[R] B) × (A →ₐ[R] C)(A →ₐ[R] B) × (A →ₐ[R] C) ≃ (A →ₐ[R] B × C) where
  toFun f := f.1.prod f.2
  invFun f := ((fst _ _ _).comp f, (snd _ _ _).comp f)
  left_inv f := by ext <;> rfl
  right_inv f := by ext <;> rfl

Equivalence between product of $R$-algebra homomorphisms and homomorphisms to product algebra

Informal description

The equivalence between the product of $R$-algebra homomorphisms $(A \toₐ[R] B) \times (A \toₐ[R] C)$ and the $R$-algebra homomorphisms from $A$ to the product $R$-algebra $B \times C$. Explicitly, this equivalence is given by: - The forward map takes a pair of homomorphisms $(f, g)$ to their product homomorphism $f \times g$ defined by $(f \times g)(x) = (f(x), g(x))$. - The inverse map takes a homomorphism $h \colon A \to B \times C$ to the pair of homomorphisms $(\pi_1 \circ h, \pi_2 \circ h)$, where $\pi_1$ and $\pi_2$ are the first and second projection maps from $B \times C$ to $B$ and $C$ respectively. This equivalence is bijective, meaning that composing the forward and inverse maps in either order yields the identity.

AlgHom.prodMap definition

{D : Type*} [Semiring D] [Algebra R D] (f : A →ₐ[R] B) (g : C →ₐ[R] D) : A × C →ₐ[R] B × D

Full source

/-- `Prod.map` of two algebra homomorphisms. -/
def prodMap {D : Type*} [Semiring D] [Algebra R D] (f : A →ₐ[R] B) (g : C →ₐ[R] D) :
    A × CA × C →ₐ[R] B × D :=
  { toRingHom := f.toRingHom.prodMap g.toRingHom
    commutes' := fun r => by simp [commutes] }

Product map of $R$-algebra homomorphisms

Informal description

Given $R$-algebra homomorphisms $f \colon A \to B$ and $g \colon C \to D$, the function $\text{prodMap}$ is the $R$-algebra homomorphism from $A \times C$ to $B \times D$ defined by mapping $(x, y)$ to $(f(x), g(y))$. This preserves both the ring structure and the $R$-algebra structure.

Main definitions