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 (I : Type u) {R : Type u_1} (f : I → Type v) {r : CommSemiring R} [s : (i : I) → Semiring (f i)] [(i : I) → Algebra R (f i)] : Algebra R ((i : I) → f i)

Equations

• Pi.algebra I f = let __src := Pi.ringHom fun (i : I) => algebraMap R (f i); Algebra.mk __src ⋯ ⋯

theorem Pi.algebraMap_def (I : Type u) {R : Type u_1} (f : I → Type v) : ∀ {x : CommSemiring R} [_s : (i : I) → Semiring (f i)] [inst : (i : I) → Algebra R (f i)] (a : R), (algebraMap R ((i : I) → f i)) a = fun (i : I) => (algebraMap R (f i)) a

@[simp]

theorem Pi.algebraMap_apply (I : Type u) {R : Type u_1} (f : I → Type v) : ∀ {x : CommSemiring R} [_s : (i : I) → Semiring (f i)] [inst : (i : I) → Algebra R (f i)] (a : R) (i : I), (algebraMap R ((i : I) → f i)) a i = (algebraMap R (f i)) a

@[simp]

theorem Pi.evalAlgHom_apply {I : Type u} (R : Type u_1) (f : I → Type v) : ∀ {x : CommSemiring R} [inst : (i : I) → Semiring (f i)] [inst_1 : (i : I) → Algebra R (f i)] (i : I) (f_1 : (i : I) → f i), (Pi.evalAlgHom R f i) f_1 = f_1 i

def Pi.evalAlgHom {I : Type u} (R : Type u_1) (f : I → Type v) : {x : CommSemiring R} → [inst : (i : I) → Semiring (f i)] → [inst_1 : (i : I) → Algebra R (f i)] → (i : I) → ((i : I) → f i) →ₐ[R] f i

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

Equations

• Pi.evalAlgHom R f i = let __src := Pi.evalRingHom f i; { toFun := fun (f : (i : I) → f i) => f i, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem Pi.constAlgHom_apply (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [Semiring B] [Algebra R B] (a : B) : ∀ (a_1 : A), (Pi.constAlgHom R A B) a a_1 = Function.const A a a_1

def Pi.constAlgHom (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [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 = let __src := Pi.constRingHom A B; { toFun := Function.const A, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem Pi.constRingHom_eq_algebraMap (R : Type u_1) (A : Type u_2) [CommSemiring R] : Pi.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_1) (A : Type u_2) [CommSemiring R] : Pi.constAlgHom R A R = Algebra.ofId R (A → R)

instance Function.algebra {R : Type u_1} (I : Type u_2) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] : Algebra R (I → 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 I A = Pi.algebra I fun (a : I) => A

@[simp]

theorem AlgHom.compLeft_apply {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (I : Type u_2) (h : I → A) : ∀ (a : I), (f.compLeft I) h a = (⇑f ∘ h) a

def AlgHom.compLeft {R : Type u} {A : Type v} {B : Type w} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (I : Type u_2) : (I → A) →ₐ[R] I → B

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

Equations

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

@[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 : ι) : (AlgEquiv.piCongrRight e) x j = (e j) (x j)

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_refl {R : Type u_1} {ι : Type u_2} {A : ι → Type u_3} [CommSemiring R] [(i : ι) → Semiring (A i)] [(i : ι) → Algebra R (A i)] : (AlgEquiv.piCongrRight fun (i : ι) => AlgEquiv.refl) = AlgEquiv.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) : (AlgEquiv.piCongrRight e).symm = AlgEquiv.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) : (AlgEquiv.piCongrRight e₁).trans (AlgEquiv.piCongrRight e₂) = AlgEquiv.piCongrRight fun (i : ι) => (e₁ i).trans (e₂ i)