OAI/GroupTheory/Kervaire/Traversal.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.KervaireTraversal.Slots line 42
2. def OAI.KervaireTraversal.coordinates line 44
3. def OAI.KervaireTraversal.mixer line 54
4. def OAI.KervaireTraversal.exchange line 57
5. lemma OAI.KervaireTraversal.exchange_star line 61
6. lemma OAI.KervaireTraversal.exchange_sq line 64
7. lemma OAI.KervaireTraversal.exchange_unitary line 70
8. lemma OAI.KervaireTraversal.mixer_coordinates line 76
9. lemma OAI.KervaireTraversal.signedMatrix_unitary line 86
10. lemma OAI.KervaireTraversal.exists_mixer_fixed line 99
11. lemma OAI.KervaireTraversal.offDiagonal_representation line 138

    Source documentation

    Every unitary selfadjoint exchange has a unitary off-diagonal block.

    lemma offDiagonal_representation (N : Matrix (E ⊕ E) (E ⊕ E) ℂ)
        (hNs : star N = N) (hNu : N ∈ unitary (Matrix (E ⊕ E) (E ⊕ E) ℂ))
        (h₀ : ∀ i j, N (.inl i) (.inl j) = 0)
        (h₁ : ∀ i j, N (.inr i) (.inr j) = 0) :
        ∃ P : unitary (Matrix E E ℂ), N = fromBlocks 0 (star (P : Matrix E E ℂ)) P 0 := by
    …

12. lemma OAI.KervaireTraversal.exists_mixer_for_exchange line 171

    Source documentation

    The exact mixing step for an arbitrary scalar band involution exchanging positive and negative traversal slots. No monomial restriction is imposed on X.

    lemma exists_mixer_for_exchange (s : I → ℤ)
        (hs : ∀ i, s i = 1 ∨ s i = -1) (hsum : (∑ i, s i) = 1 ∨ (∑ i, s i) = -1)
        (T : Matrix (Slots I K) (Slots I K) ℂ)
        (hTs : star T = T) (hTu : T ∈ unitary (Matrix (Slots I K) (Slots I K) ℂ))
        (h₀ : ∀ i j, T (coordinates s (.inl i)) (coordinates s (.inl j)) = 0)
        (h₁ : ∀ i j, T (coordinates s (.inr i)) (coordinates s (.inr j)) = 0) :
        ∃ X : unitary (Matrix K K ℂ), 2 * Fintype.card K ≤ fixedDim (mixer (X : Matrix K K ℂ) * T) := by
    …

    Mentions: OAI.KervaireTraversal.Slots, OAI.KervaireTraversal.coordinates, OAI.KervaireTraversal.mixer

13. def OAI.KervaireMatrix.monomial line 203

    Source documentation

    The exact scalar weighted permutation attached to the oriented bands.

    def monomial (θ : Equiv.Perm D) (u : D → ℂ) : Matrix D D ℂ :=
    …

14. lemma OAI.KervaireMatrix.monomial_mul line 206
15. lemma OAI.KervaireMatrix.monomial_one line 220
16. lemma OAI.KervaireMatrix.monomial_star line 225
17. lemma OAI.KervaireMatrix.monomial_unitary line 239
18. lemma OAI.KervaireMatrix.monomial_selfadjoint line 251
19. lemma OAI.KervaireMatrix.scalarTensor_monomial line 261
20. lemma OAI.KervaireMixing.phase_upper_of_fixed line 279