# mathlib3documentation

ring_theory.algebra_tower

# Towers of algebras #

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

We set up the basic theory of algebra towers. 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).

In field_theory/tower.lean we use this to prove the tower law for finite extensions, that if R and S are both fields, then [A:R] = [A:S] [S:A].

In this file we prepare the main lemma: if {bi | i ∈ I} is an R-basis of S and {cj | j ∈ J} is a S-basis of A, then {bi cj | i ∈ I, j ∈ J} is an R-basis of A. This statement does not require the base rings to be a field, so we also generalize the lemma to rings in this file.

def is_scalar_tower.invertible.algebra_tower (R : Type u) (S : Type v) (A : Type w) [semiring A] [ S] [ A] [ A] [ A] (r : R) [invertible ( S) r)] :

Suppose that R -> S -> A is a tower of algebras. If an element r : R is invertible in S, then it is invertible in A.

Equations
def is_scalar_tower.invertible_algebra_coe_nat (R : Type u) (A : Type w) [semiring A] [ A] (n : ) [inv : invertible n] :

A natural number that is invertible when coerced to R is also invertible when coerced to any R-algebra.

Equations
@[simp]
theorem basis.algebra_map_coeffs_repr_apply_support_val {R : Type u} (A : Type w) {ι : Type u_1} {M : Type u_2} [semiring A] [ A] [ M] [ M] [ M] (b : R M) (h : function.bijective A)) (ᾰ : M) :
( h).repr) ᾰ).support.val = multiset.filter (λ (a : ι), ¬ h).symm.symm) (((b.repr) ᾰ) a) = 0) ((b.repr) ᾰ).support.val
noncomputable def basis.algebra_map_coeffs {R : Type u} (A : Type w) {ι : Type u_1} {M : Type u_2} [semiring A] [ A] [ M] [ M] [ M] (b : R M) (h : function.bijective A)) :
A M

If R and A have a bijective algebra_map R A and act identically on M, then a basis for M as R-module is also a basis for M as R'-module.

Equations
@[simp]
theorem basis.algebra_map_coeffs_repr_apply_to_fun {R : Type u} (A : Type w) {ι : Type u_1} {M : Type u_2} [semiring A] [ A] [ M] [ M] [ M] (b : R M) (h : function.bijective A)) (ᾰ : M) (ᾰ_1 : ι) :
( h).repr) ᾰ) ᾰ_1 = A) (((b.repr) ᾰ) ᾰ_1)
@[simp]
theorem basis.algebra_map_coeffs_repr_symm_apply {R : Type u} (A : Type w) {ι : Type u_1} {M : Type u_2} [semiring A] [ A] [ M] [ M] [ M] (b : R M) (h : function.bijective A)) (ᾰ : ι →₀ A) :
h).repr.symm) = M R b)
theorem basis.algebra_map_coeffs_apply {R : Type u} (A : Type w) {ι : Type u_1} {M : Type u_2} [semiring A] [ A] [ M] [ M] [ M] (b : R M) (h : function.bijective A)) (i : ι) :
h) i = b i
@[simp]
theorem basis.coe_algebra_map_coeffs {R : Type u} (A : Type w) {ι : Type u_1} {M : Type u_2} [semiring A] [ A] [ M] [ M] [ M] (b : R M) (h : function.bijective A)) :
h) = b
theorem linear_independent_smul {R : Type u} {S : Type v} {A : Type w} [semiring S] [ S] [ A] [ A] [ A] {ι : Type v₁} {b : ι S} {ι' : Type w₁} {c : ι' A} (hb : b) (hc : c) :
(λ (p : ι × ι'), b p.fst c p.snd)
noncomputable def basis.smul {R : Type u} {S : Type v} {A : Type w} [semiring S] [ S] [ A] [ A] [ A] {ι : Type v₁} {ι' : Type w₁} (b : R S) (c : basis ι' S A) :
basis × ι') R A

basis.smul (b : basis ι R S) (c : basis ι S A) is the R-basis on A where the (i, j)th basis vector is b i • c j.

Equations
@[simp]
theorem basis.smul_repr {R : Type u} {S : Type v} {A : Type w} [semiring S] [ S] [ A] [ A] [ A] {ι : Type v₁} {ι' : Type w₁} (b : R S) (c : basis ι' S A) (x : A) (ij : ι × ι') :
(((b.smul c).repr) x) ij = ((b.repr) (((c.repr) x) ij.snd)) ij.fst
theorem basis.smul_repr_mk {R : Type u} {S : Type v} {A : Type w} [semiring S] [ S] [ A] [ A] [ A] {ι : Type v₁} {ι' : Type w₁} (b : R S) (c : basis ι' S A) (x : A) (i : ι) (j : ι') :
(((b.smul c).repr) x) (i, j) = ((b.repr) (((c.repr) x) j)) i
@[simp]
theorem basis.smul_apply {R : Type u} {S : Type v} {A : Type w} [semiring S] [ S] [ A] [ A] [ A] {ι : Type v₁} {ι' : Type w₁} (b : R S) (c : basis ι' S A) (ij : ι × ι') :
(b.smul c) ij = b ij.fst c ij.snd
theorem basis.algebra_map_injective {R : Type u} {S : Type v} [comm_ring R] [ring S] [ S] {ι : Type u_1} [nontrivial S] (b : R S) :
def alg_hom.restrict_domain {A : Type w} (B : Type u₁) {C : Type u_1} {D : Type u_2} [ C] [ D] (f : C →ₐ[A] D) [ B] [ C] [ C] :

Restrict the domain of an alg_hom.

Equations
def alg_hom.extend_scalars {A : Type w} (B : Type u₁) {C : Type u_1} {D : Type u_2} [ C] [ D] (f : C →ₐ[A] D) [ B] [ C] [ C] :

Extend the scalars of an alg_hom.

Equations
def alg_hom_equiv_sigma {A : Type w} {B : Type u₁} {C : Type u_1} {D : Type u_2} [ C] [ D] [ B] [ C] [ C] :
(C →ₐ[A] D) Σ (f : B →ₐ[A] D), C →ₐ[B] D

alg_homs from the top of a tower are equivalent to a pair of alg_homs.

Equations