OAI/Topology/CoarseAssembly/RelativeUnitary.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Unitaries equal to one modulo a nonunital subalgebra

The scalar part is kept explicit, so no faithfulness assumption on a unitization representation is needed to obtain its K₁ class.

  1. theorem OAI.CoarseAssembly.OperatorKTheory.relativePart_mul_star line 19
  2. theorem OAI.CoarseAssembly.OperatorKTheory.relativePart_star_mul line 30
  3. theorem OAI.CoarseAssembly.OperatorKTheory.relativeUnitary_val line 41
  4. theorem OAI.CoarseAssembly.OperatorKTheory.relativeUnitary_scalar line 45
  5. theorem OAI.CoarseAssembly.OperatorKTheory.relativeMatrix_scalar line 49
  6. theorem OAI.CoarseAssembly.OperatorKTheory.relativeClass_one line 59
  7. theorem OAI.CoarseAssembly.OperatorKTheory.relativeClass_eq_zero line 74