OAI/Topology/CoarseAssembly/RelativeTwoConjugation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Relative two-by-two conjugation by idealizing operators

  1. def OAI.CoarseAssembly.OperatorKTheory.matrixTwoUnitalStarHom line 13
  2. theorem OAI.CoarseAssembly.OperatorKTheory.matrixTwoUnitalStarHom_apply line 25
  3. theorem OAI.CoarseAssembly.OperatorKTheory.matrixTwoUnitalStarHom_continuous line 29
  4. def OAI.CoarseAssembly.OperatorKTheory.mapTwoUnitary line 33
  5. theorem OAI.CoarseAssembly.OperatorKTheory.mapTwoUnitary_diagonal line 38
  6. def OAI.CoarseAssembly.OperatorKTheory.conjugatedTwoUnitary line 46
  7. theorem OAI.CoarseAssembly.OperatorKTheory.conjugatedTwoUnitary_defect line 49
  8. theorem OAI.CoarseAssembly.OperatorKTheory.mapTwoUnitary_one line 60
  9. theorem OAI.CoarseAssembly.OperatorKTheory.mapTwoUnitary_conjugate line 64
  10. theorem OAI.CoarseAssembly.OperatorKTheory.conjugatedTwoUnitary_relative line 77

    Source documentation

    The entries of the conjugation defect remain in the idealized algebra.

    theorem conjugatedTwoUnitary_relative (φ : A →⋆ₐ[ℂ] R)
    (hφ : ∀ a b, b ∈ S → φ a * b ∈ S ∧ b * φ a ∈ S)
    (w : unitary (Matrix (Fin 2) (Fin 2) A))
    (u : unitary (Matrix (Fin 2) (Fin 2) R))
    (hu : ∀ i j, ((u : Matrix (Fin 2) (Fin 2) R) - 1) i j ∈ S) :
    ∀ i j, ((conjugatedTwoUnitary (mapTwoUnitary φ w) u :
      Matrix (Fin 2) (Fin 2) R) - 1) i j ∈ S := by
…

    Mentions: OAI.CoarseAssembly.OperatorKTheory.conjugatedTwoUnitary, OAI.CoarseAssembly.OperatorKTheory.mapTwoUnitary

  11. theorem OAI.CoarseAssembly.OperatorKTheory.relativeTwoClass_conjugationPath line 99