OAI/Analysis/KadisonSimilarity/Representation/ConullRepresentationExtension.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Extend the original algebra's conull fiber representations by zero. The maps remain nonunital star homomorphisms at every base point, so their unit projections give genuine representations on every projection fiber.

  1. def OAI.KadisonSimilarity.zeroExtendNonunitalRepresentation line 18
  2. theorem OAI.KadisonSimilarity.zeroExtendNonunitalRepresentation_apply line 26