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)

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.

@[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.

@[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)

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.

@[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.

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.

@[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_3} {ι : Type u_4} {A₁ : ι → Type u_5} {A₂ : ι → Type u_6} [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.

@[simp]

theorem AlgEquiv.piCongrRight_apply {R : Type u_3} {ι : Type u_4} {A₁ : ι → Type u_5} {A₂ : ι → Type u_6} [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_3} {ι : Type u_4} {A₁ : ι → Type u_5} [CommSemiring R] [(i : ι) → Semiring (A₁ i)] [(i : ι) → Algebra R (A₁ i)] : (piCongrRight fun (i : ι) => refl) = refl

@[simp]

theorem AlgEquiv.piCongrRight_symm {R : Type u_3} {ι : Type u_4} {A₁ : ι → Type u_5} {A₂ : ι → Type u_6} [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_3} {ι : Type u_4} {A₁ : ι → Type u_5} {A₂ : ι → Type u_6} {A₃ : ι → Type u_7} [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)

def AlgEquiv.piMulOpposite (R : Type u_3) {ι : Type u_4} (A₁ : ι → Type u_5) [CommSemiring R] [(i : ι) → Semiring (A₁ i)] [(i : ι) → Algebra R (A₁ i)] : ((i : ι) → A₁ i)ᵐᵒᵖ ≃ₐ[R] (i : ι) → (A₁ i)ᵐᵒᵖ

The opposite of a direct product is isomorphic to the direct product of the opposites as algebras.

def AlgEquiv.piCongrLeft' (R : Type u_3) {ι : Type u_4} (A₁ : ι → Type u_5) [CommSemiring R] [(i : ι) → Semiring (A₁ i)] [(i : ι) → Algebra R (A₁ i)] {ι' : Type u_8} (e : ι ≃ ι') : ((i : ι) → A₁ i) ≃ₐ[R] (i : ι') → A₁ (e.symm i)

Transport dependent functions through an equivalence of the base space.

This is Equiv.piCongrLeft' as an AlgEquiv.

@[simp]

theorem AlgEquiv.piCongrLeft'_apply {R : Type u_3} {ι : Type u_4} {A₁ : ι → Type u_5} [CommSemiring R] [(i : ι) → Semiring (A₁ i)] [(i : ι) → Algebra R (A₁ i)] {ι' : Type u_8} (e : ι ≃ ι') (x : (i : ι) → A₁ i) : (piCongrLeft' R A₁ e) x = (Equiv.piCongrLeft' A₁ e) x

@[simp]

theorem AlgEquiv.piCongrLeft'_symm_apply {R : Type u_3} {ι : Type u_4} {A₁ : ι → Type u_5} [CommSemiring R] [(i : ι) → Semiring (A₁ i)] [(i : ι) → Algebra R (A₁ i)] {ι' : Type u_8} (e : ι ≃ ι') (x : (i : ι') → A₁ (e.symm i)) : (piCongrLeft' R A₁ e).symm x = (Equiv.piCongrLeft' A₁ e).symm x

def AlgEquiv.piCongrLeft (R : Type u_3) {ι : Type u_4} (A₁ : ι → Type u_5) [CommSemiring R] [(i : ι) → Semiring (A₁ i)] [(i : ι) → Algebra R (A₁ i)] {ι' : Type u_8} (e : ι' ≃ ι) : ((i : ι') → A₁ (e i)) ≃ₐ[R] (i : ι) → A₁ i

Transport dependent functions through an equivalence of the base space, expressed as "simplification".

This is Equiv.piCongrLeft as an AlgEquiv.

@[simp]

theorem AlgEquiv.piCongrLeft_apply {R : Type u_3} {ι : Type u_4} {A₁ : ι → Type u_5} [CommSemiring R] [(i : ι) → Semiring (A₁ i)] [(i : ι) → Algebra R (A₁ i)] {ι' : Type u_8} (e : ι' ≃ ι) (x : (i : ι') → A₁ (e i)) : (piCongrLeft R A₁ e) x = (Equiv.piCongrLeft A₁ e) x

@[simp]

theorem AlgEquiv.piCongrLeft_symm_apply {R : Type u_3} {ι : Type u_4} {A₁ : ι → Type u_5} [CommSemiring R] [(i : ι) → Semiring (A₁ i)] [(i : ι) → Algebra R (A₁ i)] {ι' : Type u_8} (e : ι' ≃ ι) (x : (i : ι) → A₁ i) : (piCongrLeft R A₁ e).symm x = (Equiv.piCongrLeft A₁ e).symm x

def AlgEquiv.funUnique (R : Type u_3) (ι : Type u_4) [CommSemiring R] (S : Type u_8) [Semiring S] [Algebra R S] [Unique ι] : (ι → S) ≃ₐ[R] S

If ι has a unique element, then ι → S is isomorphic to S as an R-algebra.

@[simp]

theorem AlgEquiv.funUnique_apply {R : Type u_3} {ι : Type u_4} [CommSemiring R] (S : Type u_8) [Semiring S] [Algebra R S] [Unique ι] (x : ι → S) : (funUnique R ι S) x = (Equiv.funUnique ι S) x

@[simp]

theorem AlgEquiv.funUnique_symm_apply {R : Type u_3} {ι : Type u_4} [CommSemiring R] (S : Type u_8) [Semiring S] [Algebra R S] [Unique ι] (x : S) : (funUnique R ι S).symm x = (Equiv.funUnique ι S).symm x

def AlgEquiv.sumArrowEquivProdArrow (α : Type u_1) (β : Type u_2) (R : Type u_3) [CommSemiring R] (S : Type u_8) [Semiring S] [Algebra R S] : (α ⊕ β → S) ≃ₐ[R] (α → S) × (β → S)

Equiv.sumArrowEquivProdArrow as an algebra equivalence.

@[simp]

theorem AlgEquiv.sumArrowEquivProdArrow_apply {α : Type u_1} {β : Type u_2} {R : Type u_3} [CommSemiring R] (S : Type u_8) [Semiring S] [Algebra R S] (x : α ⊕ β → S) : (sumArrowEquivProdArrow α β R S) x = (Equiv.sumArrowEquivProdArrow α β S) x

@[simp]

theorem AlgEquiv.sumArrowEquivProdArrow_symm_apply_inr {α : Type u_1} {β : Type u_2} {R : Type u_3} [CommSemiring R] (S : Type u_8) [Semiring S] [Algebra R S] (x : (α → S) × (β → S)) : (sumArrowEquivProdArrow α β R S).symm x = (Equiv.sumArrowEquivProdArrow α β S).symm x