OAI/Analysis/BoundedHochschild/TypeIResolution.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Orthogonal homogeneous resolutions of finite type-I algebras

A maximal orthogonal family of homogeneous central blocks separates points: a nonzero central complement would contain another block by the type-I hypothesis.

  1. lemma OAI.HochschildTypeILocal.exists_maximal_homogeneous_family line 33
  2. theorem OAI.HochschildTypeILocal.exists_homogeneous_resolution line 72