Towers of algebras

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 IsScalarTower R S A, the later asserting the compatibility condition (r • s) • a = r • (s • a).

In Mathlib/FieldTheory/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 an 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.

@[instance_reducible]

def IsScalarTower.Invertible.algebraTower (R : Type u_1) (S : Type u_2) (A : Type u_3) [CommSemiring R] [CommSemiring S] [Semiring A] [Algebra R S] [Algebra S A] [Algebra R A] [IsScalarTower R S A] (r : R) [Invertible ((algebraMap R S) r)] : Invertible ((algebraMap R A) 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.

@[instance_reducible]

def IsScalarTower.invertibleAlgebraCoeNat (R : Type u_1) (A : Type u_3) [CommSemiring R] [Semiring A] [Algebra R A] (n : ℕ) [inv : Invertible ↑n] : Invertible ↑n

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

noncomputable def Module.Basis.algebraMapCoeffs {R : Type u_1} (A : Type u_3) {ι : Type u_5} {M : Type u_6} [CommSemiring R] [Semiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] [IsScalarTower R A M] (b : Basis ι R M) (h : Function.Bijective ⇑(algebraMap R A)) : Basis ι A M

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

theorem Module.Basis.algebraMapCoeffs_repr_apply_apply {R : Type u_1} (A : Type u_3) {ι : Type u_5} {M : Type u_6} [CommSemiring R] [Semiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] [IsScalarTower R A M] (b : Basis ι R M) (h : Function.Bijective ⇑(algebraMap R A)) (x : M) (a✝ : ι) : ((algebraMapCoeffs A b h).repr x) a✝ = (algebraMap R A) ((b.repr x) a✝)

@[simp]

theorem Module.Basis.algebraMapCoeffs_repr {R : Type u_1} (A : Type u_3) {ι : Type u_5} {M : Type u_6} [CommSemiring R] [Semiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] [IsScalarTower R A M] (b : Basis ι R M) (h : Function.Bijective ⇑(algebraMap R A)) (m : M) : (algebraMapCoeffs A b h).repr m = Finsupp.mapRange ⇑(algebraMap R A) ⋯ (b.repr m)

theorem Module.Basis.algebraMapCoeffs_apply {R : Type u_1} (A : Type u_3) {ι : Type u_5} {M : Type u_6} [CommSemiring R] [Semiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] [IsScalarTower R A M] (b : Basis ι R M) (h : Function.Bijective ⇑(algebraMap R A)) (i : ι) : (algebraMapCoeffs A b h) i = b i

@[simp]

theorem Module.Basis.coe_algebraMapCoeffs {R : Type u_1} (A : Type u_3) {ι : Type u_5} {M : Type u_6} [CommSemiring R] [Semiring A] [AddCommMonoid M] [Algebra R A] [Module A M] [Module R M] [IsScalarTower R A M] (b : Basis ι R M) (h : Function.Bijective ⇑(algebraMap R A)) : ⇑(algebraMapCoeffs A b h) = ⇑b

theorem linearIndependent_smul {R : Type u_1} {S : Type u_2} {A : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid A] [Module R S] [Module S A] [Module R A] [IsScalarTower R S A] {ι : Type u_5} {b : ι → S} {ι' : Type u_6} {c : ι' → A} (hb : LinearIndependent R b) (hc : LinearIndependent S c) : LinearIndependent R fun (p : ι × ι') => b p.1 • c p.2

theorem Module.Basis.isScalarTower_of_nonempty (R : Type u_1) {S : Type u_2} {A : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid A] [Module R S] [Module S A] [Module R A] [IsScalarTower R S A] {ι : Type u_5} [Nonempty ι] (b : Basis ι S A) : IsScalarTower R S S

theorem Module.Basis.isScalarTower_finsupp (R : Type u_1) {S : Type u_2} {A : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid A] [Module R S] [Module S A] [Module R A] [IsScalarTower R S A] {ι : Type u_5} (b : Basis ι S A) : IsScalarTower R S (ι →₀ S)

noncomputable def Module.Basis.smulTower {R : Type u_1} {S : Type u_2} {A : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid A] [Module R S] [Module S A] [Module R A] [IsScalarTower R S A] {ι : Type u_5} {ι' : Type u_6} (b : Basis ι R S) (c : Basis ι' S A) : Basis (ι × ι') R A

Basis.smulTower (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.

@[simp]

theorem Module.Basis.smulTower_repr {R : Type u_1} {S : Type u_2} {A : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid A] [Module R S] [Module S A] [Module R A] [IsScalarTower R S A] {ι : Type u_5} {ι' : Type u_6} (b : Basis ι R S) (c : Basis ι' S A) (x : A) (ij : ι × ι') : ((b.smulTower c).repr x) ij = (b.repr ((c.repr x) ij.2)) ij.1

theorem Module.Basis.smulTower_repr_mk {R : Type u_1} {S : Type u_2} {A : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid A] [Module R S] [Module S A] [Module R A] [IsScalarTower R S A] {ι : Type u_5} {ι' : Type u_6} (b : Basis ι R S) (c : Basis ι' S A) (x : A) (i : ι) (j : ι') : ((b.smulTower c).repr x) (i, j) = (b.repr ((c.repr x) j)) i

@[simp]

theorem Module.Basis.smulTower_apply {R : Type u_1} {S : Type u_2} {A : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid A] [Module R S] [Module S A] [Module R A] [IsScalarTower R S A] {ι : Type u_5} {ι' : Type u_6} (b : Basis ι R S) (c : Basis ι' S A) (ij : ι × ι') : (b.smulTower c) ij = b ij.1 • c ij.2

noncomputable def Module.Basis.smulTower' {R : Type u_1} {S : Type u_2} {A : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid A] [Module R S] [Module S A] [Module R A] [IsScalarTower R S A] {ι : Type u_5} {ι' : Type u_6} (b : Basis ι R S) (c : Basis ι' S A) : Basis (ι' × ι) R A

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

theorem Module.Basis.smulTower'_repr {R : Type u_1} {S : Type u_2} {A : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid A] [Module R S] [Module S A] [Module R A] [IsScalarTower R S A] {ι : Type u_5} {ι' : Type u_6} (b : Basis ι R S) (c : Basis ι' S A) (x : A) (ij : ι' × ι) : ((b.smulTower' c).repr x) ij = (b.repr ((c.repr x) ij.1)) ij.2

theorem Module.Basis.smulTower'_repr_mk {R : Type u_1} {S : Type u_2} {A : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid A] [Module R S] [Module S A] [Module R A] [IsScalarTower R S A] {ι : Type u_5} {ι' : Type u_6} (b : Basis ι R S) (c : Basis ι' S A) (x : A) (i : ι') (j : ι) : ((b.smulTower' c).repr x) (i, j) = (b.repr ((c.repr x) i)) j

theorem Module.Basis.smulTower'_apply {R : Type u_1} {S : Type u_2} {A : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid A] [Module R S] [Module S A] [Module R A] [IsScalarTower R S A] {ι : Type u_5} {ι' : Type u_6} (b : Basis ι R S) (c : Basis ι' S A) (ij : ι' × ι) : (b.smulTower' c) ij = b ij.2 • c ij.1

theorem Module.Basis.algebraMap_injective {R : Type u_1} {S : Type u_2} [CommRing R] [IsDomain R] [Ring S] [Nontrivial S] [Algebra R S] {ι : Type u_5} (b : Basis ι R S) : Function.Injective ⇑(algebraMap R S)

def AlgHom.domRestrict {A : Type u_3} (B : Type u_4) {C : Type u_5} {D : Type u_6} [CommSemiring A] [CommSemiring C] [CommSemiring D] [Algebra A C] [Algebra A D] [CommSemiring B] [Algebra A B] [Algebra B C] [IsScalarTower A B C] (f : C →ₐ[A] D) : B →ₐ[A] D

Restrict the domain of an AlgHom.

@[deprecated AlgHom.domRestrict (since := "2026-07-19")]

def AlgHom.restrictDomain {A : Type u_3} (B : Type u_4) {C : Type u_5} {D : Type u_6} [CommSemiring A] [CommSemiring C] [CommSemiring D] [Algebra A C] [Algebra A D] [CommSemiring B] [Algebra A B] [Algebra B C] [IsScalarTower A B C] (f : C →ₐ[A] D) : B →ₐ[A] D

Alias of AlgHom.domRestrict.

---

Restrict the domain of an AlgHom.

def AlgHom.extendScalars {A : Type u_3} (B : Type u_4) {C : Type u_5} {D : Type u_6} [CommSemiring A] [CommSemiring C] [CommSemiring D] [Algebra A C] [Algebra A D] [CommSemiring B] [Algebra A B] [Algebra B C] [IsScalarTower A B C] (f : C →ₐ[A] D) : C →ₐ[B] D

Extend the scalars of an AlgHom.

def algHomEquivSigma {A : Type u_3} {B : Type u_4} {C : Type u_5} {D : Type u_6} [CommSemiring A] [CommSemiring C] [CommSemiring D] [Algebra A C] [Algebra A D] [CommSemiring B] [Algebra A B] [Algebra B C] [IsScalarTower A B C] : (C →ₐ[A] D) ≃ (f : B →ₐ[A] D) × (C →ₐ[B] D)

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