OAI/Topology/CoarseAssembly/OrthogonalSumBoundary.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CoarseAssembly.Analytic.orthogonal_maps_reverse line 18
2. def OAI.CoarseAssembly.Analytic.orthogonalSumHom line 22
3. theorem OAI.CoarseAssembly.Analytic.nonunitalUnitaryExtension_product line 36
4. theorem OAI.CoarseAssembly.Analytic.orthogonalSum_selfAdjoint line 44
5. theorem OAI.CoarseAssembly.Analytic.rationalBoundaryUnitary_orthogonalSum line 48
6. theorem OAI.CoarseAssembly.OperatorKTheory.relativeClass_orthogonalSum line 75

   Source documentation

   The exact orthogonal-sum formula gives addition in the existing K₁ group.

   theorem relativeClass_orthogonalSum (S : NonUnitalStarSubalgebra ℂ R)
       [hS : IsClosed (S : Set R)]
       (φ : A →⋆ₙₐ[ℂ] R) (ψ : B →⋆ₙₐ[ℂ] R)
       (horth : ∀ a b, φ a * ψ b = 0) (hone : φ 1 + ψ 1 = 1)
       (F : A) (G : B) (hF : IsSelfAdjoint F) (hG : IsSelfAdjoint G)
       (hsum : (rationalBoundaryUnitary (φ F + ψ G)
         (orthogonalSum_selfAdjoint φ ψ F G hF hG) : R) - 1 ∈ S)
       (hleft : (rationalBoundaryUnitary (nonunitalIdentityExtension φ F)
         (nonunitalIdentityExtension_selfAdjoint φ F hF) : R) - 1 ∈ S)
       (hright : (rationalBoundaryUnitary (nonunitalIdentityExtension ψ G)
         (nonunitalIdentityExtension_selfAdjoint ψ G hG) : R) - 1 ∈ S) :
       relativeClass S (rationalBoundaryUnitary (φ F + ψ G)
   …

   Mentions: OAI.CoarseAssembly.OperatorKTheory.relativeClass