OAI/Algebra/Finitistic/Selection/FiniteQuotient.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Exact prerequisites for Section 2 of v5s9.15.

These are the variable-coefficient elementary-matrix calculations in the finite-quotient construction, over the actual rings F₂[t]/(t^m - 1). They do not establish the paper's main homological theorem.

  1. def OAI.LittleFinitistic.transvection line 26
  2. theorem OAI.LittleFinitistic.single_square_zero line 28
  3. theorem OAI.LittleFinitistic.transvection_mul_neg line 32
  4. def OAI.LittleFinitistic.transvectionUnit line 38
  5. theorem OAI.LittleFinitistic.transvection_same line 44
  6. theorem OAI.LittleFinitistic.nilpotent_commutator line 50
  7. theorem OAI.LittleFinitistic.transvection_commutator line 60
  8. theorem OAI.LittleFinitistic.transvection_commute line 72
  9. theorem OAI.LittleFinitistic.transvection_injective line 83
  10. def OAI.LittleFinitistic.diagonalUnit line 89
  11. theorem OAI.LittleFinitistic.diagonal_single_conjugation line 99
  12. theorem OAI.LittleFinitistic.diagonal_transvection_conjugation line 110
  13. theorem OAI.LittleFinitistic.diagonalUnit_commute line 116
  14. theorem OAI.LittleFinitistic.transvectionUnit_commute line 121
  15. theorem OAI.LittleFinitistic.transvectionUnit_commutator line 128
  16. theorem OAI.LittleFinitistic.transvectionUnit_conjugation line 135
  17. def OAI.LittleFinitistic.cyclicPolynomial line 143
  18. abbrev OAI.LittleFinitistic.CyclicRing line 144
  19. theorem OAI.LittleFinitistic.cyclicPolynomial_monic line 146
  20. theorem OAI.LittleFinitistic.cyclicPolynomial_degree line 149
  21. def OAI.LittleFinitistic.cyclicBasis line 152
  22. theorem OAI.LittleFinitistic.cyclicRing_finite line 157
  23. theorem OAI.LittleFinitistic.cyclic_root_pow line 160
  24. theorem OAI.LittleFinitistic.cyclic_root_isUnit line 167
  25. theorem OAI.LittleFinitistic.cyclicBasis_apply line 171
  26. theorem OAI.LittleFinitistic.cyclic_powers_independent line 177
  27. def OAI.LittleFinitistic.centralMatrix line 187

    Source documentation

    The central coefficient embedding in the displayed 5-by-5 matrix model.

    noncomputable def centralMatrix (m : ℕ) (c : Fin m → ZMod 2) :
    Matrix (Fin 5) (Fin 5) (CyclicRing m) :=
…

    Mentions: OAI.LittleFinitistic.CyclicRing

  28. theorem OAI.LittleFinitistic.centralMatrix_zero line 191
  29. theorem OAI.LittleFinitistic.centralMatrix_add line 194
  30. theorem OAI.LittleFinitistic.centralMatrix_injective line 201
  31. theorem OAI.LittleFinitistic.centralMatrix_involution line 213
  32. def OAI.LittleFinitistic.centralEmbedding line 224

    Source documentation

    This is the concrete copy of the elementary abelian 2-group used by the paper's finite matrix quotient. Its realization as a quotient of the presented group remains separate from the verified embedding below.

    noncomputable def centralEmbedding (m : ℕ) :
    Multiplicative (Fin m → ZMod 2) →* (Matrix (Fin 5) (Fin 5) (CyclicRing m))ˣ where
…

    Mentions: OAI.LittleFinitistic.CyclicRing

  33. theorem OAI.LittleFinitistic.centralEmbedding_injective line 238