OAI/Topology/CoarseAssembly/CharacterExtension.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Completing a represented subspace using a character

For a unital coefficient algebra with a character, the complement of the represented subspace can carry that character. The cut-down operator acts as the identity there, so this completion preserves the Fredholm defects.

  1. def OAI.CoarseAssembly.Analytic.characterProjectionRepresentation line 20
  2. theorem OAI.CoarseAssembly.Analytic.representation_unit_projection line 31
  3. theorem OAI.CoarseAssembly.Analytic.representation_complement_right line 35
  4. theorem OAI.CoarseAssembly.Analytic.representation_complement_left line 39
  5. theorem OAI.CoarseAssembly.Analytic.completedRepresentation_apply line 43
  6. theorem OAI.CoarseAssembly.Analytic.completedRepresentation_one line 46
  7. def OAI.CoarseAssembly.Analytic.identityOperatorCycle line 52

    Source documentation

    Any representation with the identity operator is degenerate.

    def identityOperatorCycle (ρ : A →⋆ₙₐ[ℂ] End H) : OddCycle A where
…

    Mentions: OAI.CoarseAssembly.Analytic.End, OAI.CoarseAssembly.Analytic.OddCycle

  8. theorem OAI.CoarseAssembly.Analytic.identityOperatorCycle_degenerate line 60
  9. theorem OAI.CoarseAssembly.Analytic.characterExtension_unital line 68