OAI/GroupTheory/Kervaire/FixedSpaces.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KervaireFixed.fixedDim line 40
2. lemma OAI.KervaireFixed.mulVecLin_sub_one line 41
3. lemma OAI.KervaireFixed.fixedDim_reindex line 46
4. def OAI.KervaireFixed.reindexUnitary line 69
5. lemma OAI.KervaireFixed.exists_signed_fixed_pos line 85
6. lemma OAI.KervaireFixed.signedMatrix_neg line 106
7. lemma OAI.KervaireFixed.exists_signed_fixed line 113
8. abbrev OAI.KervaireFixed.fixedSpace line 130
9. lemma OAI.KervaireFixed.mem_fixedSpace line 132
10. lemma OAI.KervaireFixed.fixed_star line 136
11. def OAI.KervaireFixed.doubleFixedMap line 144

    Source documentation

    Both traversal blocks have the same fixed space dimension, without a spectral-theorem assumption or a nonzero complement assumption.

    def doubleFixedMap (D P : unitary (Matrix I I ℂ)) :
        (fixedSpace ((D : Matrix I I ℂ) * (P : Matrix I I ℂ)) × fixedSpace ((D : Matrix I I ℂ) * (P : Matrix I I ℂ))) →ₗ[ℂ]
          fixedSpace ((fromBlocks 0 (D : Matrix I I ℂ) (star D : Matrix I I ℂ) 0) *
            (fromBlocks 0 (star P : Matrix I I ℂ) (P : Matrix I I ℂ) 0)) where
    …

    Mentions: OAI.KervaireFixed.fixedSpace

12. lemma OAI.KervaireFixed.doubleFixedMap_injective line 174
13. lemma OAI.KervaireFixed.two_mul_fixedDim_le line 185
14. lemma OAI.KervaireMatrix.phase_scalar_le_codim line 199

    Source documentation

    Scalar phase bound from the literal complex fixed-space dimension.

    lemma phase_scalar_le_codim (M Q : Matrix D D ℂ)
        (hM : M ∈ unitary (Matrix D D ℂ)) (hQ : Q ∈ unitary (Matrix D D ℂ))
        (hc : Q * M * star Q = star M) :
        let _ := isStarNormal_of_mem_unitary (scalarTensor_mem_unitary (A := A) hM)
    …

    Mentions: OAI.KervaireMatrix.scalarTensor_mem_unitary