OAI/Algebra/Finitistic/Selection/MatrixModel.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LittleFinitistic.internalIndex line 12
  2. theorem OAI.LittleFinitistic.internalIndex_ne_zero line 14
  3. theorem OAI.LittleFinitistic.internalIndex_ne_four line 19
  4. theorem OAI.LittleFinitistic.internalIndex_inj line 24
  5. def OAI.LittleFinitistic.matrixU line 39
  6. def OAI.LittleFinitistic.matrixV line 42
  7. def OAI.LittleFinitistic.matrixW line 45
  8. def OAI.LittleFinitistic.matrixT line 49
  9. theorem OAI.LittleFinitistic.matrixU_square line 52
  10. theorem OAI.LittleFinitistic.matrix_UU_commute line 59
  11. theorem OAI.LittleFinitistic.matrix_VV_commute line 64
  12. theorem OAI.LittleFinitistic.matrix_UV_commute line 69
  13. theorem OAI.LittleFinitistic.matrix_WU_commute line 73
  14. theorem OAI.LittleFinitistic.matrix_WV_commute line 81
  15. theorem OAI.LittleFinitistic.matrix_UW_commutator line 89
  16. theorem OAI.LittleFinitistic.matrix_WV_commutator line 98
  17. theorem OAI.LittleFinitistic.matrix_TT_commute line 107
  18. theorem OAI.LittleFinitistic.matrix_W_diagonal line 110
  19. theorem OAI.LittleFinitistic.matrix_TU_conjugation line 113
  20. theorem OAI.LittleFinitistic.matrix_TV_conjugation line 125
  21. theorem OAI.LittleFinitistic.matrix_TW_conjugation line 137
  22. def OAI.LittleFinitistic.matrixData line 157
  23. def OAI.LittleFinitistic.matrixRepresentation line 176
  24. theorem OAI.LittleFinitistic.matrixRepresentation_z line 179
  25. instance OAI.LittleFinitistic.cyclicRing_nontrivial line 192
  26. instance OAI.LittleFinitistic.cyclicRing_finiteInst line 196
  27. instance OAI.LittleFinitistic.cyclicRing_charTwo line 199
  28. def OAI.LittleFinitistic.cyclicUnit line 202
  29. theorem OAI.LittleFinitistic.cyclicUnit_val line 205
  30. def OAI.LittleFinitistic.cyclicRepresentation line 209
  31. theorem OAI.LittleFinitistic.cyclicRepresentation_z line 212
  32. theorem OAI.LittleFinitistic.centralEmbedding_basis line 219
  33. abbrev OAI.LittleFinitistic.FiniteQuotientGroup line 228
  34. instance OAI.LittleFinitistic.finiteQuotientGroup_finite line 230
  35. def OAI.LittleFinitistic.finiteQuotientMap line 233
  36. theorem OAI.LittleFinitistic.finiteQuotientMap_surjective line 236
  37. theorem OAI.LittleFinitistic.centralEmbedding_mem_center_map line 239
  38. theorem OAI.LittleFinitistic.centralEmbedding_mem_range line 259
  39. def OAI.LittleFinitistic.quotientCentralEmbedding line 265
  40. theorem OAI.LittleFinitistic.quotientCentralEmbedding_injective line 271
  41. theorem OAI.LittleFinitistic.quotientCentralEmbedding_basis line 276
  42. theorem OAI.LittleFinitistic.quotientCentralEmbedding_central line 281
  43. theorem OAI.LittleFinitistic.finite_central_quotient line 296

    Source documentation

    The actual finite quotient in the manuscript, including the embedded elementary abelian central subgroup and the prescribed images of all its basis elements.

    theorem finite_central_quotient (m : ℕ) [NeZero m] :
    Function.Surjective (finiteQuotientMap m) ∧
    Function.Injective (quotientCentralEmbedding m) ∧
    (∀ c g, Commute (quotientCentralEmbedding m c) g) ∧
    (∀ i : Fin m, quotientCentralEmbedding m (Multiplicative.ofAdd (Pi.single i 1)) =
      finiteQuotientMap m (Presentation.z i.val)) :=
…

    Mentions: OAI.LittleFinitistic.finiteQuotientMap, OAI.LittleFinitistic.quotientCentralEmbedding, OAI.LittleFinitistic.Presentation.z