OAI/GroupTheory/PolycyclicRecognition/Finiteness/BooleanStepProjective.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Countable Boolean step rings are projective over the integers

Enumerating the Boolean coordinates gives a sequence of finite partitions. Their modules are free, the refinement maps split, and their colimit is the step ring itself. No freeness theorem about all bounded functions is needed.

  1. def OAI.PolycyclicRecognition.booleanPrefix line 17
  2. theorem OAI.PolycyclicRecognition.booleanPrefix_mono line 21
  3. theorem OAI.PolycyclicRecognition.exists_booleanPrefix_contains line 25
  4. def OAI.PolycyclicRecognition.booleanPartitionDiagram line 38
  5. def OAI.PolycyclicRecognition.booleanStepColimit line 56
  6. theorem OAI.PolycyclicRecognition.booleanStepRepresentation_projective line 73
  7. theorem OAI.PolycyclicRecognition.booleanStepRing_integer_projective line 84

    Source documentation

    The small step-function algebra required in the countable group application.

    theorem booleanStepRing_integer_projective [Countable I] [Nonempty I] :
    Module.Projective ℤ (booleanStepRing a) := by
…

    Mentions: OAI.PolycyclicRecognition.booleanStepRing