doc-next-gen

Mathlib.RingTheory.AlgebraTower

Module docstring

{"# 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 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. "}

IsScalarTower.Invertible.algebraTower definition
(r : R) [Invertible (algebraMap R S r)] : Invertible (algebraMap R A r)
Full source 
/-- 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`. -/
def Invertible.algebraTower (r : R) [Invertible (algebraMap R S r)] :
    Invertible (algebraMap R A r) :=
  Invertible.copy (Invertible.map (algebraMap S A) (algebraMap R S r)) (algebraMap R A r)
    (IsScalarTower.algebraMap_apply R S A r)
Invertibility in a tower of algebras
Informal description
Given a tower of algebras \( R \to S \to A \), if an element \( r \in R \) is invertible in \( S \) (i.e., the image of \( r \) under the algebra map \( R \to S \) is invertible), then \( r \) is also invertible in \( A \).
IsScalarTower.invertibleAlgebraCoeNat definition
(n : ℕ) [inv : Invertible (n : R)] : Invertible (n : A)
Full source 
/-- A natural number that is invertible when coerced to `R` is also invertible
when coerced to any `R`-algebra. -/
def invertibleAlgebraCoeNat (n : ℕ) [inv : Invertible (n : R)] : Invertible (n : A) :=
  haveI : Invertible (algebraMap ℕ R n) := inv
  Invertible.algebraTower ℕ R A n
Invertibility of natural numbers in algebra towers
Informal description
For any natural number \( n \) that is invertible in a ring \( R \), the image of \( n \) in any \( R \)-algebra \( A \) is also invertible.
Basis.algebraMapCoeffs definition
: Basis ι A M
Full source 
/-- 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. -/
@[simps! repr_apply_support_val repr_apply_toFun]
noncomputable def Basis.algebraMapCoeffs : Basis ι A M :=
  b.mapCoeffs (RingEquiv.ofBijective _ h) fun c x => by simp
Basis transformation under bijective algebra map
Informal description
Given a basis $b$ for a module $M$ over a ring $R$ and a bijective algebra map from $R$ to another ring $A$ that acts identically on $M$, the basis $b$ can be transformed into a basis for $M$ as an $A$-module. The transformation preserves the basis vectors while changing the coefficient ring from $R$ to $A$.
Basis.algebraMapCoeffs_apply theorem
(i : ι) : b.algebraMapCoeffs A h i = b i
Full source 
theorem Basis.algebraMapCoeffs_apply (i : ι) : b.algebraMapCoeffs A h i = b i :=
  b.mapCoeffs_apply _ _ _
Basis Vectors Remain Unchanged Under Algebra Coefficient Mapping
Informal description
For any basis $b$ of a module $M$ over a ring $R$ indexed by a type $\iota$, any $R$-algebra $A$, and any index $i \in \iota$, the $i$-th basis vector of the transformed basis $b.\text{algebraMapCoeffs}\,A\,h$ equals the original $i$-th basis vector $b(i)$. In other words, $(b.\text{algebraMapCoeffs}\,A\,h)(i) = b(i)$.
linearIndependent_smul theorem
{ι : Type*} {b : ι → S} {ι' : Type*} {c : ι' → A} (hb : LinearIndependent R b) (hc : LinearIndependent S c) : LinearIndependent R fun p : ι × ι' ↦ b p.1 • c p.2
Full source 
theorem linearIndependent_smul {ι : Type*} {b : ι → S} {ι' : Type*} {c : ι' → A}
    (hb : LinearIndependent R b) (hc : LinearIndependent S c) :
    LinearIndependent R fun p : ι × ι' ↦ b p.1 • c p.2 := by
  rw [← linearIndependent_equiv' (.prodComm ..) (g := fun p : ι' × ι ↦ b p.2 • c p.1) rfl,
    LinearIndependent, linearCombination_smul]
  simpa using Function.Injective.comp hc
    ((mapRange_injective _ (map_zero _) hb).comp <| Equiv.injective _)
Linear Independence of Tensor Products in Algebra Towers
Informal description
Let $R$, $S$, and $A$ be rings forming an algebra tower (with $R \to S \to A$ algebra maps). Given an $R$-linearly independent family $\{b_i\}_{i \in \iota}$ in $S$ and an $S$-linearly independent family $\{c_j\}_{j \in \iota'}$ in $A$, the family $\{b_i \cdot c_j\}_{(i,j) \in \iota \times \iota'}$ is $R$-linearly independent in $A$.
Basis.isScalarTower_of_nonempty theorem
{ι} [Nonempty ι] (b : Basis ι S A) : IsScalarTower R S S
Full source 
theorem Basis.isScalarTower_of_nonempty {ι} [Nonempty ι] (b : Basis ι S A) : IsScalarTower R S S :=
  (b.repr.symm.comp <| lsingle <| Classical.arbitrary ι).isScalarTower_of_injective R
    (b.repr.symm.injective.comp <| single_injective _)
Scalar Tower Condition for Nonempty Basis in Algebra Tower
Informal description
Let $R$, $S$, and $A$ be rings forming an algebra tower (with $R \to S \to A$ algebra maps), and let $\iota$ be a nonempty index type. Given a basis $b$ of $A$ over $S$ indexed by $\iota$, the scalar multiplication operations satisfy the tower condition: for any $r \in R$, $s \in S$, and $a \in A$, we have $(r \cdot s) \cdot a = r \cdot (s \cdot a)$ when viewing $S$ as both an $R$-algebra and an $S$-algebra.
Basis.isScalarTower_finsupp theorem
{ι} (b : Basis ι S A) : IsScalarTower R S (ι →₀ S)
Full source 
theorem Basis.isScalarTower_finsupp {ι} (b : Basis ι S A) : IsScalarTower R S (ι →₀ S) :=
  b.repr.symm.isScalarTower_of_injective R b.repr.symm.injective
Compatibility of Scalar Multiplication in Finitely Supported Functions over Basis
Informal description
Let $R$ be a ring, $S$ an $R$-algebra, and $A$ an $S$-algebra. Given a basis $b$ of $A$ over $S$ indexed by $\iota$, the finitely supported functions $\iota \to_{\text{f}} S$ form an $S$-module where the scalar multiplication by $R$ is compatible with the algebra structure, i.e., for any $r \in R$, $s \in S$, and $f \in \iota \to_{\text{f}} S$, we have $(r \cdot s) \cdot f = r \cdot (s \cdot f)$.
Basis.smulTower definition
: Basis (ι × ι') R A
Full source 
/-- `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`. -/
noncomputable
def Basis.smulTower : Basis (ι × ι') R A :=
  haveI := c.isScalarTower_finsupp R
  .ofRepr
    (c.repr.restrictScalars R ≪≫ₗ
      (Finsupp.lcongr (Equiv.refl _) b.repr ≪≫ₗ
        ((finsuppProdLEquiv R).symm ≪≫ₗ
          Finsupp.lcongr (Equiv.prodComm ι' ι) (LinearEquiv.refl _ _))))
Tower basis construction via scalar multiplication
Informal description
Given an $R$-basis $b$ of $S$ indexed by $\iota$ and an $S$-basis $c$ of $A$ indexed by $\iota'$, the function `Basis.smulTower b c` constructs an $R$-basis of $A$ indexed by $\iota \times \iota'$, where the basis vector corresponding to $(i, j)$ is $b_i \cdot c_j$. This basis is obtained by composing the representation isomorphisms of $c$ and $b$ with appropriate linear equivalences to ensure the resulting structure is indeed an $R$-basis of $A$.
Basis.smulTower_repr theorem
(x ij) : (b.smulTower c).repr x ij = b.repr (c.repr x ij.2) ij.1
Full source 
@[simp]
theorem Basis.smulTower_repr (x ij) :
    (b.smulTower c).repr x ij = b.repr (c.repr x ij.2) ij.1 := by
  simp [smulTower]
Coefficient Formula for Tower Basis Representation
Informal description
Let $R$ be a ring, $S$ an $R$-algebra, and $A$ an $S$-algebra. Given an $R$-basis $b$ of $S$ indexed by $\iota$ and an $S$-basis $c$ of $A$ indexed by $\iota'$, the representation of an element $x \in A$ in the $R$-basis $b \cdot c$ of $A$ (indexed by $\iota \times \iota'$) satisfies the following: for any $(i,j) \in \iota \times \iota'$, the coefficient of $(i,j)$ in the representation of $x$ is equal to the coefficient of $i$ in the representation of the coefficient of $j$ in the representation of $x$ with respect to $c$. In symbols: $$(b \cdot c).\text{repr}(x)_{(i,j)} = b.\text{repr}\big(c.\text{repr}(x)_j\big)_i$$
Basis.smulTower_repr_mk theorem
(x i j) : (b.smulTower c).repr x (i, j) = b.repr (c.repr x j) i
Full source 
theorem Basis.smulTower_repr_mk (x i j) : (b.smulTower c).repr x (i, j) = b.repr (c.repr x j) i :=
  b.smulTower_repr c x (i, j)
Coefficient Formula for Tower Basis Representation with Explicit Indices
Informal description
Let $R$ be a ring, $S$ an $R$-algebra, and $A$ an $S$-algebra. Given an $R$-basis $\{b_i\}_{i \in \iota}$ of $S$ and an $S$-basis $\{c_j\}_{j \in \iota'}$ of $A$, the representation of an element $x \in A$ in the $R$-basis $\{b_i c_j\}_{(i,j) \in \iota \times \iota'}$ of $A$ satisfies: $$(b \cdot c).\text{repr}(x)_{(i,j)} = b.\text{repr}\big(c.\text{repr}(x)_j\big)_i$$ for all $i \in \iota$ and $j \in \iota'$.
Basis.smulTower_apply theorem
(ij) : (b.smulTower c) ij = b ij.1 • c ij.2
Full source 
@[simp]
theorem Basis.smulTower_apply (ij) : (b.smulTower c) ij = b ij.1 • c ij.2 := by
  classical
  obtain ⟨i, j⟩ := ij
  rw [Basis.apply_eq_iff]
  ext ⟨i', j'⟩
  rw [Basis.smulTower_repr, LinearEquiv.map_smul, Basis.repr_self, Finsupp.smul_apply,
    Finsupp.single_apply]
  dsimp only
  split_ifs with hi
  · simp [hi, Finsupp.single_apply]
  · simp [hi]
Tower Basis Vector Formula: $(b \cdot c)_{(i,j)} = b_i \cdot c_j$
Informal description
Given an $R$-basis $b$ of $S$ indexed by $\iota$ and an $S$-basis $c$ of $A$ indexed by $\iota'$, the basis vector of the tower basis $b \cdot c$ at index $(i,j) \in \iota \times \iota'$ is given by the scalar multiplication $b_i \cdot c_j$. In symbols: $$(b \cdot c)_{(i,j)} = b_i \cdot c_j$$
Basis.smulTower' definition
: Basis (ι' × ι) R A
Full source 
/-- `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`. -/
noncomputable def Basis.smulTower' : Basis (ι' × ι) R A :=
  (b.smulTower c).reindex (.prodComm ..)
Tower basis construction via scalar multiplication with swapped indices
Informal description
Given an $R$-basis $b$ of $S$ indexed by $\iota$ and an $S$-basis $c$ of $A$ indexed by $\iota'$, the function `Basis.smulTower' b c` constructs an $R$-basis of $A$ indexed by $\iota' \times \iota$, where the basis vector corresponding to $(j, i)$ is $b_i \cdot c_j$. This basis is obtained by reindexing the basis `Basis.smulTower b c` (which uses $\iota \times \iota'$ indexing) via the product commutativity equivalence that swaps the components of each pair.
Basis.smulTower'_repr theorem
(x ij) : (b.smulTower' c).repr x ij = b.repr (c.repr x ij.1) ij.2
Full source 
theorem Basis.smulTower'_repr (x ij) :
    (b.smulTower' c).repr x ij = b.repr (c.repr x ij.1) ij.2 := by
  rw [smulTower', repr_reindex_apply, smulTower_repr]; rfl
Coefficient Formula for Swapped Tower Basis Representation
Informal description
Let $R$ be a ring, $S$ an $R$-algebra, and $A$ an $S$-algebra. Given an $R$-basis $\{b_i\}_{i \in \iota}$ of $S$ and an $S$-basis $\{c_j\}_{j \in \iota'}$ of $A$, the representation of an element $x \in A$ in the $R$-basis $\{b_j c_i\}_{(j,i) \in \iota' \times \iota}$ of $A$ satisfies the following: for any $(j,i) \in \iota' \times \iota$, the coefficient of $(j,i)$ in the representation of $x$ is equal to the coefficient of $i$ in the representation of the coefficient of $j$ in the representation of $x$ with respect to $\{c_j\}_{j \in \iota'}$. In symbols: $$(b \cdot c).\text{repr}(x)_{(j,i)} = b.\text{repr}\big(c.\text{repr}(x)_j\big)_i$$
Basis.smulTower'_repr_mk theorem
(x i j) : (b.smulTower' c).repr x (i, j) = b.repr (c.repr x i) j
Full source 
theorem Basis.smulTower'_repr_mk (x i j) : (b.smulTower' c).repr x (i, j) = b.repr (c.repr x i) j :=
  b.smulTower'_repr c x (i, j)
Coefficient Formula for Swapped Tower Basis Representation with Explicit Indices
Informal description
Let $R$ be a ring, $S$ an $R$-algebra, and $A$ an $S$-algebra. Given an $R$-basis $\{b_i\}_{i \in \iota}$ of $S$ and an $S$-basis $\{c_j\}_{j \in \iota'}$ of $A$, for any element $x \in A$ and indices $i \in \iota'$, $j \in \iota$, the coefficient of $(i,j)$ in the representation of $x$ with respect to the $R$-basis $\{c_i b_j\}_{(i,j) \in \iota' \times \iota}$ of $A$ is equal to the coefficient of $j$ in the representation of the coefficient of $i$ in the representation of $x$ with respect to $\{c_j\}_{j \in \iota'}$. In symbols: $$(b \cdot c).\text{repr}(x)_{(i,j)} = b.\text{repr}\big(c.\text{repr}(x)_i\big)_j$$
Basis.smulTower'_apply theorem
(ij) : b.smulTower' c ij = b ij.2 • c ij.1
Full source 
theorem Basis.smulTower'_apply (ij) : b.smulTower' c ij = b ij.2 • c ij.1 := by
  rw [smulTower', reindex_apply, smulTower_apply]; rfl
Tower Basis Vector Formula: $(b \cdot c)_{(j,i)} = b_i \cdot c_j$
Informal description
Given an $R$-basis $\{b_i\}_{i \in \iota}$ of $S$ and an $S$-basis $\{c_j\}_{j \in \iota'}$ of $A$, the basis vector of the tower basis $b \cdot c$ at index $(j,i) \in \iota' \times \iota$ is given by the scalar multiplication $b_i \cdot c_j$. In symbols: $$(b \cdot c)_{(j,i)} = b_i \cdot c_j$$
Basis.algebraMap_injective theorem
{ι : Type*} [NoZeroDivisors R] [Nontrivial S] (b : @Basis ι R S _ _ Algebra.toModule) : Function.Injective (algebraMap R S)
Full source 
theorem Basis.algebraMap_injective {ι : Type*} [NoZeroDivisors R] [Nontrivial S]
    (b : @Basis ι R S _ _ Algebra.toModule) : Function.Injective (algebraMap R S) :=
  have : NoZeroSMulDivisors R S := b.noZeroSMulDivisors
  FaithfulSMul.algebraMap_injective R S
Injectivity of Algebra Map for Basis over NoZeroDivisors Ring
Informal description
Let $R$ be a ring with no zero divisors, $S$ a nontrivial $R$-algebra, and $\{b_i\}_{i \in \iota}$ an $R$-basis of $S$. Then the algebra map from $R$ to $S$ is injective.
AlgHom.restrictDomain definition
: B →ₐ[A] D
Full source 
/-- Restrict the domain of an `AlgHom`. -/
def AlgHom.restrictDomain : B →ₐ[A] D :=
  f.comp (IsScalarTower.toAlgHom A B C)
Restriction of an algebra homomorphism to a subalgebra
Informal description
Given an algebra homomorphism $f \colon C \to D$ over $A$, the restriction of $f$ to a subalgebra $B$ of $C$ is an algebra homomorphism from $B$ to $D$ over $A$. More precisely, if $A$, $B$, $C$, and $D$ are algebras such that $B$ is a subalgebra of $C$ over $A$, then the restriction of $f$ to $B$ is defined by composing $f$ with the canonical inclusion map $B \hookrightarrow C$.
AlgHom.extendScalars definition
: @AlgHom B C D _ _ _ _ (f.restrictDomain B).toRingHom.toAlgebra
Full source 
/-- Extend the scalars of an `AlgHom`. -/
def AlgHom.extendScalars : @AlgHom B C D _ _ _ _ (f.restrictDomain B).toRingHom.toAlgebra where
  toFun := f.toFun
  map_one' := by simp only [toRingHom_eq_coe, RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe,
    map_one]
  map_mul' := by simp only [toRingHom_eq_coe, RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe,
    MonoidHom.toOneHom_coe, map_mul, MonoidHom.coe_coe, RingHom.coe_coe, forall_const]
  map_zero' := by simp only [toRingHom_eq_coe, RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe,
    MonoidHom.toOneHom_coe, MonoidHom.coe_coe, map_zero]
  map_add' := by simp only [toRingHom_eq_coe, RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe,
    MonoidHom.toOneHom_coe, MonoidHom.coe_coe, map_add, RingHom.coe_coe, forall_const]
  commutes' := fun _ ↦ rfl
  __ := (f.restrictDomain B).toRingHom.toAlgebra
Extension of scalars of an algebra homomorphism
Informal description
Given an algebra homomorphism $f \colon C \to D$ over $A$, the extension of scalars of $f$ is an algebra homomorphism from $C$ to $D$ over $B$, where $B$ is a subalgebra of $C$ over $A$. More precisely, if $A$, $B$, $C$, and $D$ are algebras such that $B$ is a subalgebra of $C$ over $A$, then the extension of scalars of $f$ is defined by using the restriction of $f$ to $B$ and extending it to an algebra homomorphism over $B$.
algHomEquivSigma definition
: (C →ₐ[A] D) ≃ Σ f : B →ₐ[A] D, @AlgHom B C D _ _ _ _ f.toRingHom.toAlgebra
Full source 
/-- `AlgHom`s from the top of a tower are equivalent to a pair of `AlgHom`s. -/
def algHomEquivSigma :
    (C →ₐ[A] D) ≃ Σf : B →ₐ[A] D, @AlgHom B C D _ _ _ _ f.toRingHom.toAlgebra where
  toFun f := ⟨f.restrictDomain B, f.extendScalars B⟩
  invFun fg :=
    let _ := fg.1.toRingHom.toAlgebra
    fg.2.restrictScalars A
  left_inv f := by
    dsimp only
    ext
    rfl
  right_inv := by
    rintro ⟨⟨⟨⟨⟨f, _⟩, _⟩, _⟩, _⟩, ⟨⟨⟨⟨g, _⟩, _⟩, _⟩, hg⟩⟩
    obtain rfl : f = fun x => g (algebraMap B C x) := by
      ext x
      exact (hg x).symm
    rfl
Equivalence of Algebra Homomorphisms in a Tower
Informal description
The equivalence `algHomEquivSigma` establishes a bijection between algebra homomorphisms from `C` to `D` over `A` and pairs consisting of an algebra homomorphism from `B` to `D` over `A` and an algebra homomorphism from `C` to `D` over `B`. More precisely, given algebras `A`, `B`, `C`, and `D` where `B` is a subalgebra of `C` over `A`, the equivalence maps an algebra homomorphism `f : C →ₐ[A] D` to the pair `(f.restrictDomain B, f.extendScalars B)`, and conversely, it maps a pair `(f, g)` to the restriction of `g` to `A`. This equivalence captures the idea that algebra homomorphisms from the top of a tower (`C`) can be decomposed into homomorphisms at each level of the tower (`B` and `C` over `B`).