mathlib documentation

algebra.algebra.subalgebra.tower

Subalgebras in towers of algebras #

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 #

theorem algebra.lmul_algebra_map (R : Type u) {A : Type w} [comm_semiring R] [semiring A] [algebra R A] (x : R) :
@[protected, instance]
def is_scalar_tower.subalgebra (R : Type u) (S : Type v) (A : Type w) [comm_semiring R] [comm_semiring S] [semiring A] [algebra R S] [algebra S A] (S₀ : subalgebra R S) :
@[protected, instance]
def is_scalar_tower.subalgebra' (R : Type u) (S : Type v) (A : Type w) [comm_semiring R] [comm_semiring S] [semiring A] [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A] (S₀ : subalgebra R S) :
def subalgebra.restrict_scalars (R : Type u) {S : Type v} {A : Type w} [comm_semiring R] [comm_semiring S] [semiring A] [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A] (U : subalgebra S 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} [comm_semiring R] [comm_semiring S] [semiring A] [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A] {U : subalgebra S A} :
@[simp]
theorem subalgebra.mem_restrict_scalars (R : Type u) {S : Type v} {A : Type w} [comm_semiring R] [comm_semiring S] [semiring A] [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A] {U : subalgebra S A} {x : A} :
@[simp]
def subalgebra.of_restrict_scalars (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [comm_semiring R] [comm_semiring S] [semiring A] [semiring B] [algebra R S] [algebra S A] [algebra R A] [algebra S B] [algebra R B] [is_scalar_tower R S A] [is_scalar_tower R S B] (U : subalgebra S 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