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 #

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)

source

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 => ↑(algebraMap R (f i)) a

source

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

source

@[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 : (i : I) → f i), ↑(Pi.evalAlgHom R f i) f = f i

source

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.

Instances For

source

@[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 : A), ↑(Pi.constAlgHom R A B) a a = Function.const A a a

source

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.

Instances For

source

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

source

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

source

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,

source

@[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), ↑(AlgHom.compLeft f I) h a = (↑f ∘ h) a

source

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.

Instances For

source

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

source

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.

Instances For

source

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

source

@[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.symm (AlgEquiv.piCongrRight e) = AlgEquiv.piCongrRight fun i => AlgEquiv.symm (e i)

source

@[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.trans (AlgEquiv.piCongrRight e₁) (AlgEquiv.piCongrRight e₂) = AlgEquiv.piCongrRight fun i => AlgEquiv.trans (e₁ i) (e₂ i)