OAI/Topology/CoarseAssembly/CayleyUnitization.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The rational boundary under a nonunital spatial homomorphism

The lift 1 + (F - 1) in a unitization makes the complementary summand explicit. This is the algebraic input to naturality under isometric spatial inclusions, which extend an operator by the identity off its image.

  1. def OAI.CoarseAssembly.Analytic.identityUnitization line 19
  2. theorem OAI.CoarseAssembly.Analytic.identityUnitization_selfAdjoint line 21
  3. def OAI.CoarseAssembly.Analytic.unitizationScalar line 26
  4. def OAI.CoarseAssembly.Analytic.unitizationEval line 30
  5. theorem OAI.CoarseAssembly.Analytic.unitizationEval_apply line 33
  6. theorem OAI.CoarseAssembly.Analytic.unitizationScalar_identity line 36
  7. theorem OAI.CoarseAssembly.Analytic.unitizationEval_identity line 42
  8. theorem OAI.CoarseAssembly.Analytic.rationalBoundaryUnitary_identity_scalar line 49
  9. theorem OAI.CoarseAssembly.Analytic.rationalBoundaryUnitary_identity_eval line 61
  10. theorem OAI.CoarseAssembly.Analytic.rationalBoundaryUnitary_identity line 69