Towers of algebras #
In this file we prove basic facts about towers of algebra.
An algebra tower A/S/R is expressed by having instances of algebra A S
,
algebra R S
, algebra R A
and is_scalar_tower R S A
, the later asserting the
compatibility condition (r • s) • a = r • (s • a)
.
An important definition is to_alg_hom R S A
, the canonical R
-algebra homomorphism S →ₐ[R] A
.
The R
-algebra morphism A → End (M)
corresponding to the representation of the algebra A
on the R
-module M
.
This is a stronger version of distrib_mul_action.to_linear_map
, and could also have been
called algebra.to_module_End
.
Equations
- algebra.lsmul R M = {to_fun := distrib_mul_action.to_linear_map R M is_scalar_tower.to_smul_comm_class', map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}
In a tower, the canonical map from the middle element to the top element is an algebra homomorphism over the bottom element.
R ⟶ S induces S-Alg ⥤ R-Alg
R ⟶ S induces S-Alg ⥤ R-Alg
Given a tower A / ↥U / S / R
of algebras, where U
is an S
-subalgebra of A
, reinterpret
U
as an R
-subalgebra of A
.
Equations
- subalgebra.restrict_scalars R U = {carrier := U.carrier, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _}
Produces an R
-algebra map from U.restrict_scalars R
given an S
-algebra map from U
.
This is a special case of alg_hom.restrict_scalars
that can be helpful in elaboration.
Equations
A variant of submodule.span_image
for algebra_map
.