# mathlib3documentation

algebra.algebra.subalgebra.tower

# Subalgebras in towers of algebras #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we prove facts about subalgebras in 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).

## Main results #

• is_scalar_tower.subalgebra: if A/S/R is a tower and S₀ is a subalgebra between S and R, then A/S/S₀ is a tower
• is_scalar_tower.subalgebra': if A/S/R is a tower and S₀ is a subalgebra between S and R, then A/S₀/R is a tower
• subalgebra.restrict_scalars: turn an S-subalgebra of A into an R-subalgebra of A, given that A/S/R is a tower
theorem algebra.lmul_algebra_map (R : Type u) {A : Type w} [semiring A] [ A] (x : R) :
A) ( A) x) = A) x
@[protected, instance]
def is_scalar_tower.subalgebra (R : Type u) (S : Type v) (A : Type w) [semiring A] [ S] [ A] (S₀ : S) :
S A
@[protected, instance]
def is_scalar_tower.subalgebra' (R : Type u) (S : Type v) (A : Type w) [semiring A] [ S] [ A] [ A] [ A] (S₀ : S) :
S₀ A
def subalgebra.restrict_scalars (R : Type u) {S : Type v} {A : Type w} [semiring A] [ S] [ A] [ A] [ A] (U : A) :
A

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
@[simp]
theorem subalgebra.coe_restrict_scalars (R : Type u) {S : Type v} {A : Type w} [semiring A] [ S] [ A] [ A] [ A] {U : A} :
@[simp]
theorem subalgebra.restrict_scalars_top (R : Type u) {S : Type v} {A : Type w} [semiring A] [ S] [ A] [ A] [ A] :
@[simp]
theorem subalgebra.restrict_scalars_to_submodule (R : Type u) {S : Type v} {A : Type w} [semiring A] [ S] [ A] [ A] [ A] {U : A} :
@[simp]
theorem subalgebra.mem_restrict_scalars (R : Type u) {S : Type v} {A : Type w} [semiring A] [ S] [ A] [ A] [ A] {U : A} {x : A} :
x U
theorem subalgebra.restrict_scalars_injective (R : Type u) {S : Type v} {A : Type w} [semiring A] [ S] [ A] [ A] [ A] :
@[simp]
def subalgebra.of_restrict_scalars (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [semiring A] [semiring B] [ S] [ A] [ A] [ B] [ B] [ A] [ B] (U : A) (f : U →ₐ[S] B) :

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
theorem is_scalar_tower.adjoin_range_to_alg_hom (R : Type u) (S : Type v) (A : Type w) [ S] [ A] [ A] [ A] (t : set A) :