Tower of Algebras and Tower of Algebra Equivalences

This file contains definitions, theorems, instances that are used in defining tower of algebras and their equivalences.

Main definitions

• AlgebraTower : a tower of algebras
• AlgebraTowerEquiv : an equivalence of towers of algebras

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

A tower of algebras is a sequence of algebras AT i indexed over a preorder ι with the following data:

• algebraMap : AT i →+* AT j is a ring homomorphism from AT i to AT j for all i ≤ j
• commutes' is a proof that the ring homomorphism commutes with the multiplication
• coherence': A tower of algebras is coherent if the algebra maps satisfy the coherence condition: the direct map from i to k equals the composition of maps i → j → k.

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

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

• 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

  Commutativity of multiplication with respect to the ring homomorphism.

• 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)

@[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