OAI/Analysis/BoundedHochschild/InfiniteCentralReduction.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The remaining properly infinite input

The finite case is proved. The maximal finite central cut reduces the classical vanishing input to algebras with no nonzero finite central summand, the properly infinite case of Christensen--Effros--Sinclair (1987), as recorded in Christensen--Pop--Sinclair--Smith (2003), p. 636, equation (1.1).

  1. def OAI.BoundedHochschild.KadisonRingrose.NoFiniteCentralSummand line 24
  2. lemma OAI.BoundedHochschild.KadisonRingrose.noTypeII1_centralCorner line 32
  3. theorem OAI.BoundedHochschild.KadisonRingrose.exists_finite_central_cut_noFiniteSummand line 44