OAI/GroupTheory/PolycyclicRecognition/Finiteness/SmallCoefficientRing.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

A small ring of bounded functions with finite-subgroup projectivity

For each finite subgroup choose its right-coset transversal. Take the Boolean algebra generated by every left translate of these transversals and of subgroup coset partitions inside finitely generated subgroups. When the group is countable, this uses countably many coordinates. Its step-function ring is projective over the integers and has a trace-one element for every finite subgroup.

  1. abbrev OAI.PolycyclicRecognition.finiteSubgroupIndex line 22
  2. def OAI.PolycyclicRecognition.finiteSubgroupElements line 24
  3. theorem OAI.PolycyclicRecognition.finiteSubgroupElements_coe line 29
  4. instance OAI.PolycyclicRecognition.finiteSubgroupIndex_countable line 33
  5. instance OAI.PolycyclicRecognition.finiteSubgroupIndex_nonempty line 40
  6. abbrev OAI.PolycyclicRecognition.finitelyGeneratedSubgroupIndex line 43
  7. def OAI.PolycyclicRecognition.finitelyGeneratedSubgroupGenerators line 45
  8. instance OAI.PolycyclicRecognition.finitelyGeneratedSubgroupIndex_countable line 48
  9. abbrev OAI.PolycyclicRecognition.smallCoefficientBase line 59
  10. abbrev OAI.PolycyclicRecognition.smallCoefficientIndex line 62
  11. def OAI.PolycyclicRecognition.smallCoefficientFeature line 64
  12. def OAI.PolycyclicRecognition.smallCoefficientTranslate line 70
  13. theorem OAI.PolycyclicRecognition.smallCoefficientFeature_translate line 73
  14. abbrev OAI.PolycyclicRecognition.SmallCoefficientRing line 79
  15. instance OAI.PolycyclicRecognition.smallCoefficientRing_mulSemiringAction line 81
  16. theorem OAI.PolycyclicRecognition.smallCoefficientRing_smul_apply line 86
  17. instance OAI.PolycyclicRecognition.smallCoefficientRing_integer_projective line 89
  18. def OAI.PolycyclicRecognition.smallCoefficientTransversal line 94

    Source documentation

    The indicator of the chosen transversal of a finite subgroup.

    def smallCoefficientTransversal (H : Subgroup G) [Finite H] : SmallCoefficientRing G :=
…

    Mentions: OAI.PolycyclicRecognition.SmallCoefficientRing

  19. theorem OAI.PolycyclicRecognition.smallCoefficientTransversal_apply line 99
  20. theorem OAI.PolycyclicRecognition.smallCoefficientTransversal_trace_one line 105
  21. abbrev OAI.PolycyclicRecognition.smallCoefficientRepresentation line 121

    Source documentation

    The coefficient ring with its actual translation representation.

    abbrev smallCoefficientRepresentation : Rep ℤ G :=
…
  22. theorem OAI.PolycyclicRecognition.smallCoefficient_finite_subgroup_projective line 124