OAI/Analysis/CharacterCriterion/Definitions.lean

GitHub source file

145 declarations, 0 contain sorry, 0 declared as axioms

Character criterion for Jiang–Su absorption

The main statement is Theorem 1.1 of the Kirchberg–Rørdam character-criterion paper. The constructions below specify the norm central-sequence algebra and Jiang–Su absorption.

  1. def OAI.KirchbergRordam.QuotientNormSupport.normedRing line 23

    Also declared: ComparatorChallenges/CharacterCriterion.lean:23 (same declaration text).

  2. abbrev OAI.KirchbergRordam.NormUltrapower.BoundedSeq line 88

    Also declared: ComparatorChallenges/CharacterCriterion.lean:88 (same declaration text).

  3. def OAI.KirchbergRordam.NormUltrapower.normLimit line 90

    Also declared: ComparatorChallenges/CharacterCriterion.lean:90 (same declaration text).

  4. def OAI.KirchbergRordam.NormUltrapower.nullIdeal line 102

    Also declared: ComparatorChallenges/CharacterCriterion.lean:102 (same declaration text).

  5. instance OAI.KirchbergRordam.NormUltrapower.nullIdeal_twoSided line 145

    Also declared: ComparatorChallenges/CharacterCriterion.lean:145 (same declaration text).

  6. instance OAI.KirchbergRordam.NormUltrapower.nullIdeal_closed line 173

    Also declared: ComparatorChallenges/CharacterCriterion.lean:173 (same declaration text).

  7. abbrev OAI.KirchbergRordam.NormUltrapower.Algebra line 210

    Also declared: ComparatorChallenges/CharacterCriterion.lean:210 (same declaration text).

  8. instance OAI.KirchbergRordam.NormUltrapower.quotientNormedRing line 213

    Also declared: ComparatorChallenges/CharacterCriterion.lean:213 (same declaration text).

  9. instance OAI.KirchbergRordam.NormUltrapower.quotientNormedAlgebra line 217

    Also declared: ComparatorChallenges/CharacterCriterion.lean:217 (same declaration text).

  10. instance OAI.KirchbergRordam.NormUltrapower.quotientStar line 220

    Also declared: ComparatorChallenges/CharacterCriterion.lean:220 (same declaration text).

  11. instance OAI.KirchbergRordam.NormUltrapower.quotientStarRing line 244

    Also declared: ComparatorChallenges/CharacterCriterion.lean:244 (same declaration text).

  12. instance OAI.KirchbergRordam.NormUltrapower.quotientStarModule line 258

    Also declared: ComparatorChallenges/CharacterCriterion.lean:258 (same declaration text).

  13. def OAI.KirchbergRordam.NormUltrapower.cutRepresentative line 265

    Also declared: ComparatorChallenges/CharacterCriterion.lean:265 (same declaration text).

  14. instance OAI.KirchbergRordam.NormUltrapower.quotientCStarRing line 272

    Also declared: ComparatorChallenges/CharacterCriterion.lean:272 (same declaration text).

  15. instance OAI.KirchbergRordam.NormUltrapower.quotientCStarAlgebra line 370

    Also declared: ComparatorChallenges/CharacterCriterion.lean:370 (same declaration text).

  16. def OAI.KirchbergRordam.NormUltrapower.quotientMap line 372

    Also declared: ComparatorChallenges/CharacterCriterion.lean:372 (same declaration text).

  17. def OAI.KirchbergRordam.NormUltrapower.constantSeq line 376

    Also declared: ComparatorChallenges/CharacterCriterion.lean:376 (same declaration text).

  18. def OAI.KirchbergRordam.NormUltrapower.diagonal line 385

    Also declared: ComparatorChallenges/CharacterCriterion.lean:385 (same declaration text).

  19. def OAI.KirchbergRordam.NormUltrapower.centralSubalgebra line 388

    Also declared: ComparatorChallenges/CharacterCriterion.lean:388 (same declaration text).

  20. instance OAI.KirchbergRordam.NormUltrapower.centralSubalgebra_closed line 391

    Also declared: ComparatorChallenges/CharacterCriterion.lean:391 (same declaration text).

  21. abbrev OAI.KirchbergRordam.NormUltrapower.CentralAlgebra line 395

    Also declared: ComparatorChallenges/CharacterCriterion.lean:395 (same declaration text).

  22. instance OAI.KirchbergRordam.NormUltrapower.centralSubringClass line 398

    Also declared: ComparatorChallenges/CharacterCriterion.lean:398 (same declaration text).

  23. instance OAI.KirchbergRordam.NormUltrapower.centralCStarAlgebra line 402

    Also declared: ComparatorChallenges/CharacterCriterion.lean:402 (same declaration text).

  24. instance OAI.KirchbergRordam.StarCompletion.completionStar line 413

    Also declared: ComparatorChallenges/CharacterCriterion.lean:413 (same declaration text).

  25. instance OAI.KirchbergRordam.StarCompletion.completionContinuousStar line 415

    Also declared: ComparatorChallenges/CharacterCriterion.lean:415 (same declaration text).

  26. instance OAI.KirchbergRordam.StarCompletion.completionStarRing line 418

    Also declared: ComparatorChallenges/CharacterCriterion.lean:418 (same declaration text).

  27. instance OAI.KirchbergRordam.StarCompletion.completionNormedAlgebra line 439

    Also declared: ComparatorChallenges/CharacterCriterion.lean:439 (same declaration text).

  28. instance OAI.KirchbergRordam.StarCompletion.completionStarModule line 442

    Also declared: ComparatorChallenges/CharacterCriterion.lean:442 (same declaration text).

  29. structure OAI.KirchbergRordam.CStarInductiveLimit.System line 464

    Also declared: ComparatorChallenges/CharacterCriterion.lean:464 (same declaration text).

  30. instance OAI.KirchbergRordam.CStarInductiveLimit.(instance at line 475) line 475
  31. def OAI.KirchbergRordam.CStarInductiveLimit.Raw line 479

    Also declared: ComparatorChallenges/CharacterCriterion.lean:479 (same declaration text).

  32. instance OAI.KirchbergRordam.CStarInductiveLimit.(instance at line 481) line 481
  33. instance OAI.KirchbergRordam.CStarInductiveLimit.(instance at line 483) line 483
  34. instance OAI.KirchbergRordam.CStarInductiveLimit.(instance at line 485) line 485
  35. instance OAI.KirchbergRordam.CStarInductiveLimit.(instance at line 487) line 487
  36. def OAI.KirchbergRordam.CStarInductiveLimit.rawOf line 489

    Also declared: ComparatorChallenges/CharacterCriterion.lean:489 (same declaration text).

  37. def OAI.KirchbergRordam.CStarInductiveLimit.normLift line 493

    Also declared: ComparatorChallenges/CharacterCriterion.lean:493 (same declaration text).

  38. def OAI.KirchbergRordam.CStarInductiveLimit.ringNorm line 496

    Also declared: ComparatorChallenges/CharacterCriterion.lean:496 (same declaration text).

  39. instance OAI.KirchbergRordam.CStarInductiveLimit.(instance at line 538) line 538
  40. instance OAI.KirchbergRordam.CStarInductiveLimit.(instance at line 540) line 540
  41. instance OAI.KirchbergRordam.CStarInductiveLimit.(instance at line 556) line 556
  42. instance OAI.KirchbergRordam.CStarInductiveLimit.(instance at line 571) line 571
  43. abbrev OAI.KirchbergRordam.CStarInductiveLimit.Algebra line 587

    Also declared: ComparatorChallenges/CharacterCriterion.lean:587 (same declaration text).

  44. instance OAI.KirchbergRordam.CStarInductiveLimit.(instance at line 589) line 589
  45. instance OAI.KirchbergRordam.CStarInductiveLimit.(instance at line 601) line 601
  46. structure OAI.KirchbergRordam.CStarInductiveLimit.Chain line 609

    Also declared: ComparatorChallenges/CharacterCriterion.lean:609 (same declaration text).

  47. def OAI.KirchbergRordam.CStarInductiveLimit.Chain.map line 617

    Also declared: ComparatorChallenges/CharacterCriterion.lean:617 (same declaration text).

  48. def OAI.KirchbergRordam.CStarInductiveLimit.Chain.system line 621

    Also declared: ComparatorChallenges/CharacterCriterion.lean:621 (same declaration text).

  49. structure OAI.KirchbergRordam.MaxTensor.CrossSeminorm line 656

    Also declared: ComparatorChallenges/CharacterCriterion.lean:656 (same declaration text).

  50. instance OAI.KirchbergRordam.MaxTensor.(instance at line 662) line 662
  51. def OAI.KirchbergRordam.MaxTensor.Raw line 671

    Also declared: ComparatorChallenges/CharacterCriterion.lean:671 (same declaration text).

  52. instance OAI.KirchbergRordam.MaxTensor.(instance at line 673) line 673
  53. instance OAI.KirchbergRordam.MaxTensor.(instance at line 675) line 675
  54. instance OAI.KirchbergRordam.MaxTensor.(instance at line 677) line 677
  55. def OAI.KirchbergRordam.MaxTensor.rawEquiv line 679

    Also declared: ComparatorChallenges/CharacterCriterion.lean:679 (same declaration text).

  56. def OAI.KirchbergRordam.MaxTensor.liftRaw line 684

    Also declared: ComparatorChallenges/CharacterCriterion.lean:684 (same declaration text).

  57. def OAI.KirchbergRordam.MaxTensor.representationSeminorm line 697

    Also declared: ComparatorChallenges/CharacterCriterion.lean:697 (same declaration text).

  58. abbrev OAI.KirchbergRordam.Spatial.Hilbert line 734

    Also declared: ComparatorChallenges/CharacterCriterion.lean:734 (same declaration text).

  59. def OAI.KirchbergRordam.Spatial.map line 737

    Also declared: ComparatorChallenges/CharacterCriterion.lean:737 (same declaration text).

  60. def OAI.KirchbergRordam.Spatial.left line 742

    Also declared: ComparatorChallenges/CharacterCriterion.lean:742 (same declaration text).

  61. def OAI.KirchbergRordam.Spatial.right line 812

    Also declared: ComparatorChallenges/CharacterCriterion.lean:812 (same declaration text).

  62. structure OAI.KirchbergRordam.MinTensor.RepresentationPair line 889

    Also declared: ComparatorChallenges/CharacterCriterion.lean:889 (same declaration text).

  63. def OAI.KirchbergRordam.MinTensor.RepresentationPair.left line 905

    Also declared: ComparatorChallenges/CharacterCriterion.lean:905 (same declaration text).

  64. def OAI.KirchbergRordam.MinTensor.RepresentationPair.right line 909

    Also declared: ComparatorChallenges/CharacterCriterion.lean:909 (same declaration text).

  65. def OAI.KirchbergRordam.MinTensor.RepresentationPair.crossSeminorm line 913

    Also declared: ComparatorChallenges/CharacterCriterion.lean:913 (same declaration text).

  66. def OAI.KirchbergRordam.MinTensor.spatialIndex line 944

    Also declared: ComparatorChallenges/CharacterCriterion.lean:944 (same declaration text).

  67. def OAI.KirchbergRordam.MinTensor.seminorm line 948

    Also declared: ComparatorChallenges/CharacterCriterion.lean:948 (same declaration text).

  68. def OAI.KirchbergRordam.MinTensor.Raw line 966

    Also declared: ComparatorChallenges/CharacterCriterion.lean:966 (same declaration text).

  69. instance OAI.KirchbergRordam.MinTensor.(instance at line 969) line 969
  70. instance OAI.KirchbergRordam.MinTensor.(instance at line 972) line 972
  71. instance OAI.KirchbergRordam.MinTensor.instStarRingRaw line 974

    Also declared: ComparatorChallenges/CharacterCriterion.lean:974 (same declaration text).

  72. def OAI.KirchbergRordam.MinTensor.rawRingSeminorm line 977

    Also declared: ComparatorChallenges/CharacterCriterion.lean:977 (same declaration text).

  73. instance OAI.KirchbergRordam.MinTensor.(instance at line 1022) line 1022
  74. abbrev OAI.KirchbergRordam.MinTensor.Algebra line 1024

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1024 (same declaration text).

  75. abbrev OAI.KirchbergRordam.MatrixTensor.Mat line 1032

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1032 (same declaration text).

  76. def OAI.KirchbergRordam.MatrixTensor.leftMatrixAlgebra line 1034

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1034 (same declaration text).

  77. def OAI.KirchbergRordam.MatrixTensor.rightMatrixAlgebra line 1050

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1050 (same declaration text).

  78. def OAI.KirchbergRordam.MatrixTensor.leftMatrix line 1066

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1066 (same declaration text).

  79. def OAI.KirchbergRordam.MatrixTensor.rightMatrix line 1070

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1070 (same declaration text).

  80. abbrev OAI.KirchbergRordam.PrimeDimensionDrop.Fiber line 1080

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1080 (same declaration text).

  81. def OAI.KirchbergRordam.PrimeDimensionDrop.eval line 1082

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1082 (same declaration text).

  82. def OAI.KirchbergRordam.PrimeDimensionDrop.subalgebra line 1092

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1092 (same declaration text).

  83. instance OAI.KirchbergRordam.PrimeDimensionDrop.(instance at line 1096) line 1096
  84. instance OAI.KirchbergRordam.PrimeDimensionDrop.(instance at line 1099) line 1099
  85. abbrev OAI.KirchbergRordam.PrimeDimensionDrop.Algebra line 1109

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1109 (same declaration text).

  86. instance OAI.KirchbergRordam.PrimeDimensionDrop.(instance at line 1111) line 1111
  87. instance OAI.KirchbergRordam.PrimeDimensionDrop.(instance at line 1115) line 1115
  88. def OAI.KirchbergRordam.UnitaryPaths.phase line 1123

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1123 (same declaration text).

  89. def OAI.KirchbergRordam.UnitaryPaths.involutionValue line 1125

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1125 (same declaration text).

  90. def OAI.KirchbergRordam.UnitaryPaths.involutionPath line 1128

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1128 (same declaration text).

  91. abbrev OAI.KirchbergRordam.MatrixPermutationPath.Mat line 1190

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1190 (same declaration text).

  92. def OAI.KirchbergRordam.MatrixPermutationPath.perm line 1192

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1192 (same declaration text).

  93. def OAI.KirchbergRordam.MatrixPermutationPath.path line 1202

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1202 (same declaration text).

  94. abbrev OAI.KirchbergRordam.MatrixDiagonalPath.Mat line 1233

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1233 (same declaration text).

  95. def OAI.KirchbergRordam.MatrixDiagonalPath.block line 1235

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1235 (same declaration text).

  96. def OAI.KirchbergRordam.MatrixDiagonalPath.evaluationBlock line 1249

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1249 (same declaration text).

  97. def OAI.KirchbergRordam.MatrixDiagonalPath.diagonal line 1259

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1259 (same declaration text).

  98. def OAI.KirchbergRordam.MatrixDiagonalPath.interpolate line 1275

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1275 (same declaration text).

  99. def OAI.KirchbergRordam.MatrixBlockReindex.sumBlock line 1291

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1291 (same declaration text).

  100. def OAI.KirchbergRordam.BalancedDropSystem.cardEquiv line 1326

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1326 (same declaration text).

  101. def OAI.KirchbergRordam.BalancedDropSystem.half line 1330

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1330 (same declaration text).

  102. def OAI.KirchbergRordam.BalancedDropSystem.lowerPath line 1338

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1338 (same declaration text).

  103. def OAI.KirchbergRordam.BalancedDropSystem.upperPath line 1347

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1347 (same declaration text).

  104. def OAI.KirchbergRordam.GeneralBlockReindex.repackLeft line 1367

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1367 (same declaration text).

  105. def OAI.KirchbergRordam.GeneralBlockReindex.repackRight line 1378

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1378 (same declaration text).

  106. structure OAI.KirchbergRordam.GeneralDropSystem.Data line 1449

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1449 (same declaration text).

  107. abbrev OAI.KirchbergRordam.GeneralDropSystem.Low line 1467

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1467 (same declaration text).

  108. abbrev OAI.KirchbergRordam.GeneralDropSystem.High line 1469

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1469 (same declaration text).

  109. abbrev OAI.KirchbergRordam.GeneralDropSystem.Mid line 1471

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1471 (same declaration text).

  110. abbrev OAI.KirchbergRordam.GeneralDropSystem.Slot line 1473

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1473 (same declaration text).

  111. abbrev OAI.KirchbergRordam.GeneralDropSystem.Index line 1475

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1475 (same declaration text).

  112. abbrev OAI.KirchbergRordam.GeneralDropSystem.ZeroSpace line 1477

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1477 (same declaration text).

  113. abbrev OAI.KirchbergRordam.GeneralDropSystem.OneSpace line 1479

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1479 (same declaration text).

  114. def OAI.KirchbergRordam.GeneralDropSystem.zeroLow line 1481

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1481 (same declaration text).

  115. def OAI.KirchbergRordam.GeneralDropSystem.zeroMid line 1484

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1484 (same declaration text).

  116. def OAI.KirchbergRordam.GeneralDropSystem.zeroOuter line 1487

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1487 (same declaration text).

  117. def OAI.KirchbergRordam.GeneralDropSystem.oneLow line 1490

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1490 (same declaration text).

  118. def OAI.KirchbergRordam.GeneralDropSystem.oneMid line 1493

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1493 (same declaration text).

  119. def OAI.KirchbergRordam.GeneralDropSystem.oneOuter line 1496

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1496 (same declaration text).

  120. def OAI.KirchbergRordam.GeneralDropSystem.slotSwap line 1499

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1499 (same declaration text).

  121. def OAI.KirchbergRordam.GeneralDropSystem.zeroReindex line 1505

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1505 (same declaration text).

  122. def OAI.KirchbergRordam.GeneralDropSystem.oneReindex line 1509

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1509 (same declaration text).

  123. def OAI.KirchbergRordam.GeneralDropSystem.eigenpath line 1514

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1514 (same declaration text).

  124. def OAI.KirchbergRordam.GeneralDropSystem.interpolatedEvaluation line 1519

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1519 (same declaration text).

  125. def OAI.KirchbergRordam.GeneralDropSystem.fiberMap line 1537

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1537 (same declaration text).

  126. def OAI.KirchbergRordam.GeneralDropSystem.continuousFamily line 1545

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1545 (same declaration text).

  127. def OAI.KirchbergRordam.GeneralDropSystem.rawStep line 1557

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1557 (same declaration text).

  128. def OAI.KirchbergRordam.GeneralDropSystem.restrictToSubalgebras line 1595

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1595 (same declaration text).

  129. def OAI.KirchbergRordam.GeneralDropSystem.step line 1601

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1601 (same declaration text).

  130. structure OAI.KirchbergRordam.PrimeDropPresentation line 1928

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1928 (same declaration text).

  131. def OAI.KirchbergRordam.PrimeDropPresentation.Stage line 1939

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1939 (same declaration text).

  132. instance OAI.KirchbergRordam.PrimeDropPresentation.(instance at line 1941) line 1941
  133. def OAI.KirchbergRordam.PrimeDropPresentation.chain line 1944

    Also declared: ComparatorChallenges/CharacterCriterion.lean:1944 (same declaration text).

  134. abbrev OAI.KirchbergRordam.PrimeDropPresentation.system line 2000

    Also declared: ComparatorChallenges/CharacterCriterion.lean:2000 (same declaration text).

  135. def OAI.KirchbergRordam.StandardPrimeMultiplicity.copies line 2007

    Also declared: ComparatorChallenges/CharacterCriterion.lean:2007 (same declaration text).

  136. def OAI.KirchbergRordam.StandardPrimeMultiplicity.lower line 2009

    Also declared: ComparatorChallenges/CharacterCriterion.lean:2009 (same declaration text).

  137. def OAI.KirchbergRordam.StandardPrimeMultiplicity.upper line 2011

    Also declared: ComparatorChallenges/CharacterCriterion.lean:2011 (same declaration text).

  138. def OAI.KirchbergRordam.StandardPrimeMultiplicity.middle line 2013

    Also declared: ComparatorChallenges/CharacterCriterion.lean:2013 (same declaration text).

  139. def OAI.KirchbergRordam.StandardPrimeMultiplicity.next line 2015

    Also declared: ComparatorChallenges/CharacterCriterion.lean:2015 (same declaration text).

  140. def OAI.KirchbergRordam.StandardPrimeMultiplicity.data line 2017

    Also declared: ComparatorChallenges/CharacterCriterion.lean:2017 (same declaration text).

  141. def OAI.KirchbergRordam.StandardPrimeMultiplicity.size line 2070

    Also declared: ComparatorChallenges/CharacterCriterion.lean:2070 (same declaration text).

  142. def OAI.KirchbergRordam.StandardPrimeModel.presentation line 2078

    Also declared: ComparatorChallenges/CharacterCriterion.lean:2078 (same declaration text).

  143. def OAI.KirchbergRordam.JiangSu.Algebra line 2116

    Also declared: ComparatorChallenges/CharacterCriterion.lean:2116 (same declaration text).

  144. instance OAI.KirchbergRordam.JiangSu.(instance at line 2118) line 2118
  145. def OAI.KirchbergRordam.HasNoCharacters line 2125

    Also declared: ComparatorChallenges/CharacterCriterion.lean:2125 (same declaration text).