OAI/GroupTheory/Kervaire/IncidenceSpaces.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.KervaireIncidenceCurrent.Mat line 33
2. abbrev OAI.KervaireIncidenceCurrent.Alg line 34
3. abbrev OAI.KervaireIncidenceCurrent.Horizontal line 35
4. def OAI.KervaireIncidenceCurrent.in11 line 39

   Source documentation

   Diagonal corner inclusions, as continuous real linear maps.

   def in11 : Mat K →L[ℝ] Mat (K ⊕ R) :=
   …

   Mentions: OAI.KervaireIncidenceCurrent.Mat

5. def OAI.KervaireIncidenceCurrent.in22 line 44
6. def OAI.KervaireIncidenceCurrent.diag line 50
7. def OAI.KervaireIncidenceCurrent.off line 52
8. lemma OAI.KervaireIncidenceCurrent.off_skew line 55
9. lemma OAI.KervaireIncidenceCurrent.off_bracket line 59
10. lemma OAI.KervaireIncidenceCurrent.diag_star line 67
11. lemma OAI.KervaireIncidenceCurrent.diag_mul line 72
12. lemma OAI.KervaireIncidenceCurrent.diag_sub line 76
13. def OAI.KervaireIncidenceCurrent.incidence line 81

    Source documentation

    The incidence map is polynomial in the redundant compact-group coordinates.

    def incidence (f : ℝ × Mat K → Mat (K ⊕ R)) (p : ℝ × Alg K R) : Mat (K ⊕ R) :=
    …

    Mentions: OAI.KervaireIncidenceCurrent.Mat, OAI.KervaireIncidenceCurrent.Alg

14. lemma OAI.KervaireIncidenceCurrent.diag_eq_corner line 85
15. lemma OAI.KervaireIncidenceCurrent.diag_one line 93
16. lemma OAI.KervaireIncidenceCurrent.diag_unitary line 97
17. lemma OAI.KervaireIncidenceCurrent.unitary_alg_parts line 102
18. lemma OAI.KervaireIncidenceCurrent.incidence_unitary line 110
19. lemma OAI.KervaireIncidenceCurrent.frame_diagonal_commutator line 118

    Source documentation

    A diagonal change of the frame is absorbed by a fiber-unitary direction.

    lemma frame_diagonal_commutator (T : unitary (Mat R)) (U : Mat K) (V : Mat R) :
        diag U V * diag 1 (star (T : Mat R)) - diag 1 (star (T : Mat R)) * diag U V =
          in22 (V * star (T : Mat R) - star (T : Mat R) * V) := by
    …

    Mentions: OAI.KervaireIncidenceCurrent.Mat, OAI.KervaireIncidenceCurrent.diag, OAI.KervaireIncidenceCurrent.in22

20. def OAI.KervaireIncidenceCurrent.compensated line 125
21. lemma OAI.KervaireIncidenceCurrent.compensated_star_mul line 132
22. def OAI.KervaireSkewTrace.pairing line 149

    Source documentation

    The positive invariant trace pairing on skew-Hermitian matrices.

    def pairing : LinearMap.BilinForm ℝ S where
    …

23. lemma OAI.KervaireSkewTrace.pairing_apply line 167
24. lemma OAI.KervaireSkewTrace.pairing_symm line 169
25. lemma OAI.KervaireSkewTrace.pairing_self line 174
26. lemma OAI.KervaireSkewTrace.pairing_self_eq_zero_iff line 178
27. def OAI.KervaireSkewTrace.bracket line 190
28. lemma OAI.KervaireSkewTrace.bracket_pair_left line 197
29. lemma OAI.KervaireSkewTrace.bracket_pair_right line 202
30. lemma OAI.KervaireSkewTrace.exists_orthogonal_basis line 208

    Source documentation

    Orthogonal bases exist without selecting an orientation or changing matrix norms.

    lemma exists_orthogonal_basis : ∃ b : Basis (Fin (Module.finrank ℝ S)) ℝ S,
        (pairing (I := I)).IsOrthoᵢ b :=
    …

    Mentions: OAI.KervaireSkewTrace.pairing

31. lemma OAI.KervaireSkewTrace.pairing_eq_repr_mul line 212
32. lemma OAI.KervaireSkewTrace.bracket_repr_left line 223
33. lemma OAI.KervaireSkewTrace.bracket_repr_right line 230
34. def OAI.KervaireIncidenceCurrent.direction line 242

    Source documentation

    The redundant compact group has a canonically chosen horizontal frame.

    def direction : Horizontal K R →ₗ[ℝ] skewAdjoint.submodule ℝ (Alg K R) where
    …

    Mentions: OAI.KervaireIncidenceCurrent.Horizontal, OAI.KervaireIncidenceCurrent.Alg

35. def OAI.KervaireIncidenceCurrent.rectBracket line 260

    Source documentation

    Lower block of the bracket of two off-diagonal skew matrices.

    def rectBracket (Z Y : Matrix R K ℂ) : skewAdjoint.submodule ℝ (Mat R) :=
    …

    Mentions: OAI.KervaireIncidenceCurrent.Mat

36. lemma OAI.KervaireIncidenceCurrent.rectBracket_zero_left line 269
37. lemma OAI.KervaireIncidenceCurrent.rectBracket_zero_right line 273
38. lemma OAI.KervaireIncidenceCurrent.compensated_zero line 276
39. lemma OAI.KervaireIncidenceCurrent.skewBracket_zero_left line 279
40. lemma OAI.KervaireIncidenceCurrent.skewBracket_zero_right line 283
41. def OAI.KervaireIncidenceCurrent.effectiveBracket line 289

    Source documentation

    The defect of horizontal integrability is vertical and is absorbed by T.

    def effectiveBracket (T : unitary (Mat R)) (h g : Horizontal K R) : Horizontal K R :=
    …

    Mentions: OAI.KervaireIncidenceCurrent.Mat, OAI.KervaireIncidenceCurrent.Horizontal

42. def OAI.KervaireIncidenceCurrent.horizontalBasis line 298
43. lemma OAI.KervaireIncidenceCurrent.effectiveBracket_repr_left line 301
44. lemma OAI.KervaireIncidenceCurrent.effectiveBracket_repr_right line 311