Towers of algebras and their equivalences

An AlgebraTower is a preorder-indexed family of commutative semirings with ring homomorphisms between comparable levels. Self-maps are identities, and the maps compose along chains of indices. Each map induces an algebra structure on its target, and composition gives compatible scalar actions across three levels.

AlgebraTower.ofNatStep constructs a natural-number-indexed tower by composing chosen homomorphisms between adjacent levels. These homomorphisms need not be injective.

An AlgebraTowerEquiv consists of ring equivalences at each level that commute with the tower maps.

class AlgebraTower {ι : Type u_1} [Preorder ι] (AT : ι → Type u_2) [(i : ι) → CommSemiring (AT i)] : Type (max u_1 u_2)

A preorder-indexed family of commutative semirings with compatible ring homomorphisms.

The map from a level to itself is the identity. For i ≤ j ≤ k, the map from i to k is the composite of the maps from i to j and from j to k.

• algebraMap (i j : ι) (h : i ≤ j) : AT i →+* AT j

  Ring homomorphisms from AT i to AT j for all i ≤ j.

• algebraMap_self' (i : ι) : AlgebraTower.algebraMap i i ⋯ = RingHom.id (AT i)

  The ring homomorphism from level i to itself is the identity.

• commutes' (i j : ι) (h : i ≤ j) (r : AT i) (x : AT j) : (AlgebraTower.algebraMap i j h) r * x = x * (AlgebraTower.algebraMap i j h) r

  Every image element commutes with every element of the target semiring.

• coherence' (i j k : ι) (h1 : i ≤ j) (h2 : j ≤ k) : AlgebraTower.algebraMap i k ⋯ = (AlgebraTower.algebraMap j k h2).comp (AlgebraTower.algebraMap i j h1)

  The map from i to k is the composite of the maps from i to j and j to k.

@[instance_reducible]

def AlgebraTower.ofNatStep {A : ℕ → Type u_1} [(k : ℕ) → CommSemiring (A k)] (step : (k : ℕ) → A k →+* A (k + 1)) : AlgebraTower A

Construct a tower by composing chosen ring homomorphisms between adjacent levels.

The map from a level to itself is the identity. The map from i to j + 1, for i ≤ j, is step j composed with the map from i to j. No injectivity assumption is required.

theorem AlgebraTower.ofNatStep_algebraMap_succ_right {A : ℕ → Type u_1} [(k : ℕ) → CommSemiring (A k)] (step : (k : ℕ) → A k →+* A (k + 1)) {i j : ℕ} (h : i ≤ j) : AlgebraTower.algebraMap i (j + 1) ⋯ = (step j).comp (AlgebraTower.algebraMap i j h)

Extending a constructed tower map by one level composes it with the chosen next map.

@[simp]

theorem AlgebraTower.ofNatStep_algebraMap_succ {A : ℕ → Type u_1} [(k : ℕ) → CommSemiring (A k)] (step : (k : ℕ) → A k →+* A (k + 1)) (i : ℕ) (h : i ≤ i + 1) : AlgebraTower.algebraMap i (i + 1) h = step i

The map between adjacent levels is the homomorphism supplied to the constructor.

@[simp]

theorem AlgebraTower.algebraMap_self {ι : Type u_1} [Preorder ι] {A : ι → Type u_2} [(i : ι) → CommSemiring (A i)] [AlgebraTower A] (i : ι) (h : i ≤ i) : AlgebraTower.algebraMap i i h = RingHom.id (A i)

The tower map from level i to itself is the identity for every proof of i ≤ i.

theorem AlgebraTower.algebraMap_self_apply {ι : Type u_1} [Preorder ι] {A : ι → Type u_2} [(i : ι) → CommSemiring (A i)] [AlgebraTower A] (i : ι) (h : i ≤ i) (x : A i) : (AlgebraTower.algebraMap i i h) x = x

The tower map from level i to itself fixes every element of that level.

@[reducible, inline]

abbrev AlgebraTower.toAlgebra {ι : Type u_1} [Preorder ι] {A : ι → Type u_2} [(i : ι) → CommSemiring (A i)] [AlgebraTower A] {i j : ι} (h : i ≤ j) : Algebra (A i) (A j)

@[simp]

instance AlgebraTower.toIsScalarTower {ι : Type u_1} [Preorder ι] {C : ι → Type u_4} [(i : ι) → CommSemiring (C i)] (a : AlgebraTower C) {i j k : ι} (h1 : i ≤ j) (h2 : j ≤ k) : IsScalarTower (C i) (C j) (C k)

structure AlgebraTowerEquiv {ι : Type u_1} [Preorder ι] (A : ι → Type u_5) [(i : ι) → CommSemiring (A i)] [a : AlgebraTower A] (B : ι → Type u_6) [(i : ι) → CommSemiring (B i)] [b : AlgebraTower B] : Type (max (max u_1 u_5) u_6)

• toRingEquiv (i : ι) : A i ≃+* B i
• commutesLeft' (i j : ι) (h : i ≤ j) (r : A i) : (AlgebraTower.algebraMap i j h) ((self.toRingEquiv i) r) = (self.toRingEquiv j) ((AlgebraTower.algebraMap i j h) r)

theorem AlgebraTowerEquiv.commutesRight' {ι : Type u_1} [Preorder ι] {A : ι → Type u_2} [(i : ι) → CommSemiring (A i)] [AlgebraTower A] {B : ι → Type u_3} [(i : ι) → CommSemiring (B i)] [AlgebraTower B] (e : AlgebraTowerEquiv A B) {i j : ι} (h : i ≤ j) (r : B i) : (AlgebraTower.algebraMap i j h) ((e.toRingEquiv i).symm r) = (e.toRingEquiv j).symm ((AlgebraTower.algebraMap i j h) r)

def AlgebraTowerEquiv.symm {ι : Type u_1} [Preorder ι] {A : ι → Type u_2} [(i : ι) → CommSemiring (A i)] [AlgebraTower A] {B : ι → Type u_3} [(i : ι) → CommSemiring (B i)] [AlgebraTower B] (e : AlgebraTowerEquiv A B) : AlgebraTowerEquiv B A

def AlgebraTowerEquiv.algebraMapRightUp {ι : Type u_1} [Preorder ι] {A : ι → Type u_2} [(i : ι) → CommSemiring (A i)] [AlgebraTower A] {B : ι → Type u_3} [(i : ι) → CommSemiring (B i)] [AlgebraTower B] (e : AlgebraTowerEquiv A B) (i j : ι) (h : i ≤ j) : A i →+* B j

def AlgebraTowerEquiv.algebraMapLeftUp {ι : Type u_1} [Preorder ι] {A : ι → Type u_2} [(i : ι) → CommSemiring (A i)] [AlgebraTower A] {B : ι → Type u_3} [(i : ι) → CommSemiring (B i)] [AlgebraTower B] (e : AlgebraTowerEquiv A B) (i j : ι) (h : i ≤ j) : B i →+* A j

@[reducible, inline]

abbrev AlgebraTowerEquiv.toAlgebraOverLeft {ι : Type u_1} [Preorder ι] {A : ι → Type u_2} [(i : ι) → CommSemiring (A i)] [AlgebraTower A] {B : ι → Type u_3} [(i : ι) → CommSemiring (B i)] [AlgebraTower B] (e : AlgebraTowerEquiv A B) (i j : ι) (h : i ≤ j) : Algebra (A i) (B j)

@[reducible, inline]

abbrev AlgebraTowerEquiv.toAlgebraOverRight {ι : Type u_1} [Preorder ι] {A : ι → Type u_2} [(i : ι) → CommSemiring (A i)] [AlgebraTower A] {B : ι → Type u_3} [(i : ι) → CommSemiring (B i)] [AlgebraTower B] (e : AlgebraTowerEquiv A B) (i j : ι) (h : i ≤ j) : Algebra (B i) (A j)

def AlgebraTowerEquiv.toAlgEquivOverLeft {ι : Type u_1} [Preorder ι] {A : ι → Type u_2} [(i : ι) → CommSemiring (A i)] [AlgebraTower A] {B : ι → Type u_3} [(i : ι) → CommSemiring (B i)] [AlgebraTower B] (e : AlgebraTowerEquiv A B) (i j : ι) (h : i ≤ j) : A j ≃ₐ[A i] B j

def AlgebraTowerEquiv.toAlgEquivOverRight {ι : Type u_1} [Preorder ι] {A : ι → Type u_2} [(i : ι) → CommSemiring (A i)] [AlgebraTower A] {B : ι → Type u_3} [(i : ι) → CommSemiring (B i)] [AlgebraTower B] (e : AlgebraTowerEquiv A B) (i j : ι) (h : i ≤ j) : B j ≃ₐ[B i] A j