Mathlib.Algebra.Algebra.Pi

Pi.algebra instance

: Algebra R (Π i, A i)

Full source

instance algebra : Algebra R (Π i, A i) where
  algebraMap := Pi.ringHom fun i ↦ algebraMap R (A i)
  commutes' := fun a f ↦ by ext; simp [Algebra.commutes]
  smul_def' := fun a f ↦ by ext; simp [Algebra.smul_def]

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

Informal description

For any commutative semiring $R$ and any family of $R$-algebras $(A_i)_{i \in I}$, the product type $\prod_{i \in I} A_i$ inherits an $R$-algebra structure with pointwise operations. The algebra map $R \to \prod_{i \in I} A_i$ is given by $a \mapsto (i \mapsto \text{algebraMap}_R^{A_i}(a))$.

Pi.algebraMap_def theorem

(a : R) : algebraMap R (Π i, A i) a = fun i ↦ algebraMap R (A i) a

Full source

theorem algebraMap_def (a : R) : algebraMap R (Π i, A i) a = fun i ↦ algebraMap R (A i) a :=
  rfl

Definition of Algebra Map on Product of $R$-Algebras

Informal description

For any commutative semiring $R$ and any family of $R$-algebras $(A_i)_{i \in I}$, the algebra map from $R$ to the product algebra $\prod_{i \in I} A_i$ is given by $a \mapsto (i \mapsto \text{algebraMap}_R^{A_i}(a))$ for any $a \in R$.

Pi.algebraMap_apply theorem

(a : R) (i : ι) : algebraMap R (Π i, A i) a i = algebraMap R (A i) a

Full source

@[simp]
theorem algebraMap_apply (a : R) (i : ι) : algebraMap R (Π i, A i) a i = algebraMap R (A i) a :=
  rfl

Componentwise Equality of Algebra Map on Product of $R$-Algebras

Informal description

For any commutative semiring $R$ and any family of $R$-algebras $(A_i)_{i \in I}$, the algebra map $\text{algebraMap}_R^{\prod_{i \in I} A_i}$ satisfies that for any element $a \in R$ and any index $i \in I$, the $i$-th component of $\text{algebraMap}_R^{\prod_{i \in I} A_i}(a)$ equals $\text{algebraMap}_R^{A_i}(a)$. In other words, $(\text{algebraMap}_R^{\prod_{i \in I} A_i}(a))_i = \text{algebraMap}_R^{A_i}(a)$ for all $i \in I$.

Pi.algHom definition

{B : Type*} [Semiring B] [Algebra R B] (g : ∀ i, B →ₐ[R] A i) : B →ₐ[R] Π i, A i

Full source

/-- A family of algebra homomorphisms `g i : B →ₐ[R] A i` defines a ring homomorphism
`Pi.algHom g : B →ₐ[R] Π i, A i` given by `Pi.algHom g x i = g i x`. -/
@[simps!]
def algHom {B : Type*} [Semiring B] [Algebra R B] (g : ∀ i, B →ₐ[R] A i) : B →ₐ[R] Π i, A i where
  __ := Pi.ringHom fun i ↦ (g i).toRingHom
  commutes' r := by ext; simp

Product of $R$-algebra homomorphisms

Informal description

Given a commutative semiring $R$, a semiring $B$ with an $R$-algebra structure, and a family of $R$-algebras $(A_i)_{i \in I}$, any family of $R$-algebra homomorphisms $(g_i \colon B \to A_i)_{i \in I}$ defines an $R$-algebra homomorphism $\text{Pi.algHom}\, g \colon B \to \prod_{i \in I} A_i$ given by $(\text{Pi.algHom}\, g)(x)_i = g_i(x)$ for each $x \in B$ and $i \in I$.

Pi.evalAlgHom definition

(i : ι) : (Π i, A i) →ₐ[R] A i

Full source

/-- `Function.eval` as an `AlgHom`. The name matches `Pi.evalRingHom`, `Pi.evalMonoidHom`,
etc. -/
@[simps]
def evalAlgHom (i : ι) : (Π i, A i) →ₐ[R] A i :=
  { Pi.evalRingHom A i with
    toFun := fun f ↦ f i
    commutes' := fun _ ↦ rfl }

Evaluation $R$-algebra homomorphism for product of $R$-algebras

Informal description

For a commutative semiring $R$ and a family of $R$-algebras $(A_i)_{i \in I}$, the evaluation map at index $i$ is an $R$-algebra homomorphism from the product algebra $\prod_{i \in I} A_i$ to $A_i$. Specifically, it maps a function $f$ in the product to its value $f(i)$ at index $i$, preserving both the ring structure and the $R$-algebra structure.

Pi.algHom_evalAlgHom theorem

: algHom R A (evalAlgHom R A) = AlgHom.id R (Π i, A i)

Full source

@[simp]
theorem algHom_evalAlgHom : algHom R A (evalAlgHom R A) = AlgHom.id R (Π i, A i) := rfl

Identity Property of Product Algebra Homomorphism via Evaluation

Informal description

For a commutative semiring $R$ and a family of $R$-algebras $(A_i)_{i \in I}$, the composition of the product algebra homomorphism $\text{algHom}_{R,A}$ with the evaluation homomorphisms $\text{evalAlgHom}_{R,A}$ equals the identity algebra homomorphism on the product algebra $\prod_{i \in I} A_i$. That is, $\text{algHom}_{R,A}(\text{evalAlgHom}_{R,A}) = \text{id}_{\prod_{i \in I} A_i}$.

Pi.algHom_comp theorem

 {B C : Type*} [Semiring B] [Algebra R B] [Semiring C] [Algebra R C] (g : ∀ i, C →ₐ[R] A i) (h : B →ₐ[R] C) :
  (algHom R A g).comp h = algHom R A (fun i ↦ (g i).comp h)

Full source

/-- `Pi.algHom` commutes with composition. -/
theorem algHom_comp {B C : Type*} [Semiring B] [Algebra R B] [Semiring C] [Algebra R C]
    (g : ∀ i, C →ₐ[R] A i) (h : B →ₐ[R] C) :
    (algHom R A g).comp h = algHom R A (fun i ↦ (g i).comp h) := rfl

Composition Property of Product Algebra Homomorphisms

Informal description

Let $R$ be a commutative semiring, and let $(A_i)_{i \in I}$ be a family of $R$-algebras. For any $R$-algebras $B$ and $C$, given a family of $R$-algebra homomorphisms $(g_i \colon C \to A_i)_{i \in I}$ and an $R$-algebra homomorphism $h \colon B \to C$, the composition of the product homomorphism $\text{Pi.algHom}\, g$ with $h$ equals the product homomorphism formed by composing each $g_i$ with $h$. That is, \[ (\text{Pi.algHom}\, g) \circ h = \text{Pi.algHom}\, (g_i \circ h). \]

Pi.instAlgebraForall instance

[∀ i, Algebra (S i) (A i)] : Algebra (Π i, S i) (Π i, A i)

Full source

instance [∀ i, Algebra (S i) (A i)] : Algebra (Π i, S i) (Π i, A i) where
  algebraMap := Pi.ringHom fun _ ↦ (algebraMap _ _).comp (Pi.evalRingHom S _)
  commutes' _ _ := funext fun _ ↦ Algebra.commutes _ _
  smul_def' _ _ := funext fun _ ↦ Algebra.smul_def _ _

Pointwise Algebra Structure on Product of Algebras

Informal description

For any family of $R$-algebras $(A_i)_{i \in I}$ where each $A_i$ is an algebra over a corresponding ring $(S_i)_{i \in I}$, the product type $\prod_{i \in I} A_i$ inherits an algebra structure over the product ring $\prod_{i \in I} S_i$ with pointwise operations. Specifically: - The algebra operations (addition, multiplication, and scalar multiplication) are defined componentwise - The algebra map from $\prod_{i \in I} S_i$ to $\prod_{i \in I} A_i$ is given by applying each component's algebra map pointwise - The multiplicative identity is the function that returns the multiplicative identity of each $A_i$

Pi.constAlgHom definition

: B →ₐ[R] A → B

Full source

/-- `Function.const` as an `AlgHom`. The name matches `Pi.constRingHom`, `Pi.constMonoidHom`,
etc. -/
@[simps]
def constAlgHom : B →ₐ[R] A → B :=
  { Pi.constRingHom A B with
    toFun := Function.const _
    commutes' := fun _ ↦ rfl }

Constant function as an $R$-algebra homomorphism

Informal description

The constant function that maps every element of type $A$ to a fixed element of type $B$ forms an $R$-algebra homomorphism from $B$ to the function space $A \to B$, where $B$ is an $R$-algebra. This homomorphism preserves the $R$-algebra structure, meaning it commutes with the algebra map from $R$.

Pi.constRingHom_eq_algebraMap theorem

: constRingHom A R = algebraMap R (A → R)

Full source

/-- When `R` is commutative and permits an `algebraMap`, `Pi.constRingHom` is equal to that
map. -/
@[simp]
theorem constRingHom_eq_algebraMap : constRingHom A R = algebraMap R (A → R) :=
  rfl

Equality of Constant Ring Homomorphism and Algebra Map for Function Space

Informal description

For a commutative semiring $R$ and a type $A$, the constant ring homomorphism $\text{constRingHom}_A^R : R \to (A \to R)$ coincides with the algebra map $\text{algebraMap}_R^{A \to R}$ when $R$ is viewed as an $R$-algebra.

Pi.constAlgHom_eq_algebra_ofId theorem

: constAlgHom R A R = Algebra.ofId R (A → R)

Full source

@[simp]
theorem constAlgHom_eq_algebra_ofId : constAlgHom R A R = Algebra.ofId R (A → R) :=
  rfl

Equality of Constant Algebra Homomorphism and Canonical Embedding for Function Space over $R$

Informal description

For a commutative semiring $R$ and a type $A$, the constant $R$-algebra homomorphism from $R$ to the function space $A \to R$ is equal to the canonical algebra map that embeds $R$ into $A \to R$ as constant functions.

Function.algebra instance

{R : Type*} (ι : Type*) (A : Type*) [CommSemiring R] [Semiring A] [Algebra R A] : Algebra R (ι → A)

Full source

/-- A special case of `Pi.algebra` for non-dependent types. Lean struggles to elaborate
definitions elsewhere in the library without this. -/
instance Function.algebra {R : Type*} (ι : Type*) (A : Type*) [CommSemiring R] [Semiring A]
    [Algebra R A] : Algebra R (ι → A) :=
  Pi.algebra _ _

$R$-Algebra Structure on Function Types

Informal description

For any commutative semiring $R$, any type $\iota$, and any $R$-algebra $A$, the function type $\iota \to A$ inherits an $R$-algebra structure with pointwise operations. The algebra map $R \to (\iota \to A)$ is given by $a \mapsto (i \mapsto \text{algebraMap}_R^A(a))$.

AlgHom.compLeft definition

(f : A →ₐ[R] B) (ι : Type*) : (ι → A) →ₐ[R] ι → B

Full source

/-- `R`-algebra homomorphism between the function spaces `ι → A` and `ι → B`, induced by an
`R`-algebra homomorphism `f` between `A` and `B`. -/
@[simps]
protected def compLeft (f : A →ₐ[R] B) (ι : Type*) : (ι → A) →ₐ[R] ι → B :=
  { f.toRingHom.compLeft ι with
    toFun := fun h ↦ f ∘ h
    commutes' := fun c ↦ by
      ext
      exact f.commutes' c }

Post-composition $R$-algebra homomorphism on function spaces

Informal description

Given an $R$-algebra homomorphism $f \colon A \to B$ and a type $\iota$, the function `AlgHom.compLeft` constructs an $R$-algebra homomorphism from the function space $\iota \to A$ to $\iota \to B$ by post-composing with $f$. Specifically, it maps any function $h \colon \iota \to A$ to the composition $f \circ h \colon \iota \to B$.

AlgEquiv.piCongrRight definition

(e : ∀ i, A₁ i ≃ₐ[R] A₂ i) : (Π i, A₁ i) ≃ₐ[R] Π i, A₂ i

Full source

/-- A family of algebra equivalences `∀ i, (A₁ i ≃ₐ A₂ i)` generates a
multiplicative equivalence between `Π i, A₁ i` and `Π i, A₂ i`.

This is the `AlgEquiv` version of `Equiv.piCongrRight`, and the dependent version of
`AlgEquiv.arrowCongr`.
-/
@[simps apply]
def piCongrRight (e : ∀ i, A₁ i ≃ₐ[R] A₂ i) : (Π i, A₁ i) ≃ₐ[R] Π i, A₂ i :=
  { @RingEquiv.piCongrRight ι A₁ A₂ _ _ fun i ↦ (e i).toRingEquiv with
    toFun := fun x j ↦ e j (x j)
    invFun := fun x j ↦ (e j).symm (x j)
    commutes' := fun r ↦ by
      ext i
      simp }

Component-wise $R$-algebra isomorphism of product algebras

Informal description

Given a commutative semiring $R$ and two families of $R$-algebras $(A_1_i)_{i \in I}$ and $(A_2_i)_{i \in I}$, along with a family of $R$-algebra isomorphisms $(e_i : A_1_i \simeq_{R} A_2_i)_{i \in I}$, there exists an $R$-algebra isomorphism between the product algebras $\prod_{i \in I} A_1_i$ and $\prod_{i \in I} A_2_i$. This isomorphism maps a tuple $(x_i)_{i \in I}$ to $(e_i(x_i))_{i \in I}$, and its inverse maps $(y_i)_{i \in I}$ to $(e_i^{-1}(y_i))_{i \in I}$. The isomorphism preserves both the ring structure and the scalar multiplication by elements of $R$ component-wise.

AlgEquiv.piCongrRight_refl theorem

: (piCongrRight fun i ↦ (AlgEquiv.refl : A₁ i ≃ₐ[R] A₁ i)) = AlgEquiv.refl

Full source

@[simp]
theorem piCongrRight_refl :
    (piCongrRight fun i ↦ (AlgEquiv.refl : A₁ i ≃ₐ[R] A₁ i)) = AlgEquiv.refl :=
  rfl

Identity Component-wise Isomorphism Yields Identity on Product Algebra

Informal description

Given a commutative semiring $R$ and a family of $R$-algebras $(A_i)_{i \in I}$, the component-wise $R$-algebra isomorphism construction using identity isomorphisms on each $A_i$ yields the identity isomorphism on the product algebra $\prod_{i \in I} A_i$. In other words, the isomorphism $\prod_{i \in I} A_i \simeq_{R} \prod_{i \in I} A_i$ obtained by applying the identity isomorphism $A_i \simeq_{R} A_i$ to each component is equal to the identity isomorphism on $\prod_{i \in I} A_i$.

AlgEquiv.piCongrRight_symm theorem

(e : ∀ i, A₁ i ≃ₐ[R] A₂ i) : (piCongrRight e).symm = piCongrRight fun i ↦ (e i).symm

Full source

@[simp]
theorem piCongrRight_symm (e : ∀ i, A₁ i ≃ₐ[R] A₂ i) :
    (piCongrRight e).symm = piCongrRight fun i ↦ (e i).symm :=
  rfl

Inverse of Component-wise $R$-Algebra Isomorphism Equals Component-wise Inverses

Informal description

Given a commutative semiring $R$ and two families of $R$-algebras $(A_1_i)_{i \in I}$ and $(A_2_i)_{i \in I}$, along with a family of $R$-algebra isomorphisms $(e_i : A_1_i \simeq_{R} A_2_i)_{i \in I}$, the inverse of the component-wise $R$-algebra isomorphism $\prod_{i \in I} A_1_i \simeq_{R} \prod_{i \in I} A_2_i$ is equal to the component-wise $R$-algebra isomorphism obtained by taking the inverse of each $e_i$. In other words, for the isomorphism $\text{piCongrRight}\, e : \prod_{i} A_1_i \simeq_{R} \prod_{i} A_2_i$ defined by $(x_i)_i \mapsto (e_i(x_i))_i$, we have: $$(\text{piCongrRight}\, e)^{-1} = \text{piCongrRight}\, (\lambda i, e_i^{-1})$$

AlgEquiv.piCongrRight_trans theorem

 (e₁ : ∀ i, A₁ i ≃ₐ[R] A₂ i) (e₂ : ∀ i, A₂ i ≃ₐ[R] A₃ i) :
  (piCongrRight e₁).trans (piCongrRight e₂) = piCongrRight fun i ↦ (e₁ i).trans (e₂ i)

Full source

@[simp]
theorem piCongrRight_trans (e₁ : ∀ i, A₁ i ≃ₐ[R] A₂ i) (e₂ : ∀ i, A₂ i ≃ₐ[R] A₃ i) :
    (piCongrRight e₁).trans (piCongrRight e₂) = piCongrRight fun i ↦ (e₁ i).trans (e₂ i) :=
  rfl

Composition of Product $R$-Algebra Isomorphisms Equals Product of Compositions

Informal description

Let $R$ be a commutative semiring and let $(A_1_i)_{i \in I}$, $(A_2_i)_{i \in I}$, $(A_3_i)_{i \in I}$ be families of $R$-algebras. Given families of $R$-algebra isomorphisms $(e_1_i : A_1_i \simeq_{alg[R]} A_2_i)_{i \in I}$ and $(e_2_i : A_2_i \simeq_{alg[R]} A_3_i)_{i \in I}$, the composition of the product isomorphisms $\prod_{i \in I} e_1_i$ and $\prod_{i \in I} e_2_i$ is equal to the product isomorphism $\prod_{i \in I} (e_1_i \circ e_2_i)$. In other words, the following diagram commutes: $$(\prod_{i \in I} A_1_i) \xrightarrow{\prod e_1_i} (\prod_{i \in I} A_2_i) \xrightarrow{\prod e_2_i} (\prod_{i \in I} A_3_i)$$ is equal to: $$(\prod_{i \in I} A_1_i) \xrightarrow{\prod (e_1_i \circ e_2_i)} (\prod_{i \in I} A_3_i)$$

Main definitions