The R-algebra structure on families 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 Pi.algebra (ι : Type u_1) {R : Type u_2} (A : ι → Type u_3) [CommSemiring R] [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] : Algebra R ((i : ι) → A i)

Equations

• Pi.algebra ι A = Algebra.mk (Pi.ringHom fun (i : ι) => algebraMap R (A i)) ⋯ ⋯

theorem Pi.algebraMap_def (ι : Type u_1) {R : Type u_2} (A : ι → Type u_3) [CommSemiring R] [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] (a : R) : (algebraMap R ((i : ι) → A i)) a = fun (i : ι) => (algebraMap R (A i)) a

@[simp]

theorem Pi.algebraMap_apply (ι : Type u_1) {R : Type u_2} (A : ι → Type u_3) [CommSemiring R] [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] (a : R) (i : ι) : (algebraMap R ((i : ι) → A i)) a i = (algebraMap R (A i)) a

def Pi.algHom {ι : Type u_1} (R : Type u_2) (A : ι → Type u_3) [CommSemiring R] [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] {B : Type u_4} [Semiring B] [Algebra R B] (g : (i : ι) → B →ₐ[R] A i) : B →ₐ[R] (i : ι) → A i

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.

Equations

• Pi.algHom R A g = { toRingHom := Pi.ringHom fun (i : ι) => (g i).toRingHom, commutes' := ⋯ }

@[simp]

theorem Pi.algHom_apply {ι : Type u_1} (R : Type u_2) (A : ι → Type u_3) [CommSemiring R] [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] {B : Type u_4} [Semiring B] [Algebra R B] (g : (i : ι) → B →ₐ[R] A i) (x : B) (b : ι) : (algHom R A g) x b = (g b) x

def Pi.evalAlgHom {ι : Type u_1} (R : Type u_2) (A : ι → Type u_3) [CommSemiring R] [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] (i : ι) : ((i : ι) → A i) →ₐ[R] A i

Function.eval as an AlgHom. The name matches Pi.evalRingHom, Pi.evalMonoidHom, etc.

Equations

• Pi.evalAlgHom R A i = { toFun := fun (f : (i : ι) → A i) => f i, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem Pi.evalAlgHom_apply {ι : Type u_1} (R : Type u_2) (A : ι → Type u_3) [CommSemiring R] [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] (i : ι) (f : (i : ι) → A i) : (evalAlgHom R A i) f = f i

@[simp]

theorem Pi.algHom_evalAlgHom {ι : Type u_1} (R : Type u_2) (A : ι → Type u_3) [CommSemiring R] [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] : algHom R A (evalAlgHom R A) = AlgHom.id R ((i : ι) → A i)

theorem Pi.algHom_comp {ι : Type u_1} (R : Type u_2) (A : ι → Type u_3) [CommSemiring R] [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] {B : Type u_4} {C : Type u_5} [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

Pi.algHom commutes with composition.

instance Pi.instAlgebraForall {ι : Type u_1} (A : ι → Type u_3) [(i : ι) → Semiring (A i)] (S : ι → Type u_4) [(i : ι) → CommSemiring (S i)] [(i : ι) → Algebra (S i) (A i)] : Algebra ((i : ι) → S i) ((i : ι) → A i)

Equations

• Pi.instAlgebraForall A S = Algebra.mk (Pi.ringHom fun (x : ι) => (algebraMap (S x) (A x)).comp (Pi.evalRingHom S x)) ⋯ ⋯

def Pi.constAlgHom (R : Type u_2) [CommSemiring R] (A : Type u_5) (B : Type u_6) [Semiring B] [Algebra R B] : B →ₐ[R] A → B

Function.const as an AlgHom. The name matches Pi.constRingHom, Pi.constMonoidHom, etc.

Equations

• Pi.constAlgHom R A B = { toFun := Function.const A, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem Pi.constAlgHom_apply (R : Type u_2) [CommSemiring R] (A : Type u_5) (B : Type u_6) [Semiring B] [Algebra R B] (a : B) (a✝ : A) : (constAlgHom R A B) a a✝ = Function.const A a a✝

@[simp]

theorem Pi.constRingHom_eq_algebraMap (R : Type u_2) [CommSemiring R] (A : Type u_5) : constRingHom A R = algebraMap R (A → R)

When R is commutative and permits an algebraMap, Pi.constRingHom is equal to that map.

@[simp]

theorem Pi.constAlgHom_eq_algebra_ofId (R : Type u_2) [CommSemiring R] (A : Type u_5) : constAlgHom R A R = Algebra.ofId R (A → R)

instance Function.algebra {R : Type u_1} (ι : Type u_2) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] : Algebra R (ι → A)

A special case of Pi.algebra for non-dependent types. Lean struggles to elaborate definitions elsewhere in the library without this.

Equations

• Function.algebra ι A = Pi.algebra ι fun (a : ι) => A

def AlgHom.compLeft {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (ι : Type u_4) : (ι → A) →ₐ[R] ι → B

R-algebra homomorphism between the function spaces ι → A and ι → B, induced by an R-algebra homomorphism f between A and B.

Equations

• f.compLeft ι = { toFun := fun (h : ι → A) => ⇑f ∘ h, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem AlgHom.compLeft_apply {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (ι : Type u_4) (h : ι → A) (a✝ : ι) : (f.compLeft ι) h a✝ = (⇑f ∘ h) a✝

def AlgEquiv.piCongrRight {R : Type u_1} {ι : Type u_2} {A₁ : ι → Type u_3} {A₂ : ι → Type u_4} [CommSemiring R] [(i : ι) → Semiring (A₁ i)] [(i : ι) → Semiring (A₂ i)] [(i : ι) → Algebra R (A₁ i)] [(i : ι) → Algebra R (A₂ i)] (e : (i : ι) → A₁ i ≃ₐ[R] A₂ i) : ((i : ι) → A₁ i) ≃ₐ[R] (i : ι) → A₂ i

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.

Equations

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

@[simp]

theorem AlgEquiv.piCongrRight_apply {R : Type u_1} {ι : Type u_2} {A₁ : ι → Type u_3} {A₂ : ι → Type u_4} [CommSemiring R] [(i : ι) → Semiring (A₁ i)] [(i : ι) → Semiring (A₂ i)] [(i : ι) → Algebra R (A₁ i)] [(i : ι) → Algebra R (A₂ i)] (e : (i : ι) → A₁ i ≃ₐ[R] A₂ i) (x : (i : ι) → A₁ i) (j : ι) : (piCongrRight e) x j = (e j) (x j)

@[simp]

theorem AlgEquiv.piCongrRight_refl {R : Type u_1} {ι : Type u_2} {A₁ : ι → Type u_3} [CommSemiring R] [(i : ι) → Semiring (A₁ i)] [(i : ι) → Algebra R (A₁ i)] : (piCongrRight fun (i : ι) => refl) = refl

@[simp]

theorem AlgEquiv.piCongrRight_symm {R : Type u_1} {ι : Type u_2} {A₁ : ι → Type u_3} {A₂ : ι → Type u_4} [CommSemiring R] [(i : ι) → Semiring (A₁ i)] [(i : ι) → Semiring (A₂ i)] [(i : ι) → Algebra R (A₁ i)] [(i : ι) → Algebra R (A₂ i)] (e : (i : ι) → A₁ i ≃ₐ[R] A₂ i) : (piCongrRight e).symm = piCongrRight fun (i : ι) => (e i).symm

@[simp]

theorem AlgEquiv.piCongrRight_trans {R : Type u_1} {ι : Type u_2} {A₁ : ι → Type u_3} {A₂ : ι → Type u_4} {A₃ : ι → Type u_5} [CommSemiring R] [(i : ι) → Semiring (A₁ i)] [(i : ι) → Semiring (A₂ i)] [(i : ι) → Semiring (A₃ i)] [(i : ι) → Algebra R (A₁ i)] [(i : ι) → Algebra R (A₂ i)] [(i : ι) → Algebra R (A₃ i)] (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)