The R-algebra structure on families of R-algebras #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
The R-algebra structure on Π i : I, A i when each A i is an R-algebra.
Main defintions #
@[protected, instance]
def
pi.algebra
(I : Type u)
{R : Type u_1}
(f : I → Type v)
{r : comm_semiring R}
[s : Π (i : I), semiring (f i)]
[Π (i : I), algebra R (f i)] :
Equations
- pi.algebra I f = {to_has_smul := pi.has_smul (λ (i : I), smul_zero_class.to_has_smul), to_ring_hom := {to_fun := (pi.ring_hom (λ (i : I), algebra_map R (f i))).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
theorem
pi.algebra_map_def
(I : Type u)
{R : Type u_1}
(f : I → Type v)
{r : comm_semiring R}
[s : Π (i : I), semiring (f i)]
[Π (i : I), algebra R (f i)]
(a : R) :
⇑(algebra_map R (Π (i : I), f i)) a = λ (i : I), ⇑(algebra_map R (f i)) a
@[simp]
theorem
pi.algebra_map_apply
(I : Type u)
{R : Type u_1}
(f : I → Type v)
{r : comm_semiring R}
[s : Π (i : I), semiring (f i)]
[Π (i : I), algebra R (f i)]
(a : R)
(i : I) :
⇑(algebra_map R (Π (i : I), f i)) a i = ⇑(algebra_map R (f i)) a
@[simp]
theorem
pi.eval_alg_hom_apply
{I : Type u}
(R : Type u_1)
(f : I → Type v)
{r : comm_semiring R}
[Π (i : I), semiring (f i)]
[Π (i : I), algebra R (f i)]
(i : I)
(f_1 : Π (i : I), f i) :
⇑(pi.eval_alg_hom R f i) f_1 = f_1 i
def
pi.eval_alg_hom
{I : Type u}
(R : Type u_1)
(f : I → Type v)
{r : comm_semiring R}
[Π (i : I), semiring (f i)]
[Π (i : I), algebra R (f i)]
(i : I) :
function.eval as an alg_hom. The name matches pi.eval_ring_hom, pi.eval_monoid_hom,
etc.
@[simp]
theorem
pi.const_alg_hom_apply
(R : Type u_1)
(A : Type u_2)
(B : Type u_3)
[comm_semiring R]
[semiring B]
[algebra R B]
(a : B)
(ᾰ : A) :
⇑(pi.const_alg_hom R A B) a ᾰ = function.const A a ᾰ
def
pi.const_alg_hom
(R : Type u_1)
(A : Type u_2)
(B : Type u_3)
[comm_semiring R]
[semiring B]
[algebra R B] :
function.const as an alg_hom. The name matches pi.const_ring_hom, pi.const_monoid_hom,
etc.
Equations
- pi.const_alg_hom R A B = {to_fun := function.const A, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}
@[simp]
theorem
pi.const_ring_hom_eq_algebra_map
(R : Type u_1)
(A : Type u_2)
[comm_semiring R] :
pi.const_ring_hom A R = algebra_map R (A → R)
When R is commutative and permits an algebra_map, pi.const_ring_hom is equal to that
map.
@[simp]
theorem
pi.const_alg_hom_eq_algebra_of_id
(R : Type u_1)
(A : Type u_2)
[comm_semiring R] :
pi.const_alg_hom R A R = algebra.of_id R (A → R)
@[protected, instance]
def
function.algebra
{R : Type u_1}
(I : Type u_2)
(A : Type u_3)
[comm_semiring R]
[semiring 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 I A = pi.algebra I (λ (ᾰ : I), A)
@[protected]
def
alg_hom.comp_left
{R : Type u}
{A : Type v}
{B : Type w}
[comm_semiring R]
[semiring A]
[semiring B]
[algebra R A]
[algebra R B]
(f : A →ₐ[R] B)
(I : Type u_1) :
R-algebra homomorphism between the function spaces I → A and I → B, induced by an
R-algebra homomorphism f between A and B.
@[simp]
theorem
alg_equiv.Pi_congr_right_apply
{R : Type u_1}
{ι : Type u_2}
{A₁ : ι → Type u_3}
{A₂ : ι → Type u_4}
[comm_semiring 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 : ι) :
⇑(alg_equiv.Pi_congr_right e) x j = ⇑(e j) (x j)
def
alg_equiv.Pi_congr_right
{R : Type u_1}
{ι : Type u_2}
{A₁ : ι → Type u_3}
{A₂ : ι → Type u_4}
[comm_semiring 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) :
A family of algebra equivalences Π j, (A₁ j ≃ₐ A₂ j) generates a
multiplicative equivalence between Π j, A₁ j and Π j, A₂ j.
This is the alg_equiv version of equiv.Pi_congr_right, and the dependent version of
alg_equiv.arrow_congr.
@[simp]
theorem
alg_equiv.Pi_congr_right_refl
{R : Type u_1}
{ι : Type u_2}
{A : ι → Type u_3}
[comm_semiring R]
[Π (i : ι), semiring (A i)]
[Π (i : ι), algebra R (A i)] :
alg_equiv.Pi_congr_right (λ (i : ι), alg_equiv.refl) = alg_equiv.refl
@[simp]
theorem
alg_equiv.Pi_congr_right_symm
{R : Type u_1}
{ι : Type u_2}
{A₁ : ι → Type u_3}
{A₂ : ι → Type u_4}
[comm_semiring 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) :
(alg_equiv.Pi_congr_right e).symm = alg_equiv.Pi_congr_right (λ (i : ι), (e i).symm)
@[simp]
theorem
alg_equiv.Pi_congr_right_trans
{R : Type u_1}
{ι : Type u_2}
{A₁ : ι → Type u_3}
{A₂ : ι → Type u_4}
{A₃ : ι → Type u_5}
[comm_semiring 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) :
(alg_equiv.Pi_congr_right e₁).trans (alg_equiv.Pi_congr_right e₂) = alg_equiv.Pi_congr_right (λ (i : ι), (e₁ i).trans (e₂ i))