OAI/GroupTheory/PolycyclicRecognition/Finiteness/SplitProjectiveColimit.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Projectivity of a sequential colimit with split transition maps

This is used for countable algebras of integer-valued step functions. Finite partition refinements give split inclusions of free modules; their actual colimit is projective. The splitting is constructed by compatible lifts.

  1. def OAI.PolycyclicRecognition.SequentialRepresentationDiagram.compatibleProjectiveLift line 22

    Source documentation

    Correct arbitrary lifts by the retraction so that successive lifts agree.

    def compatibleProjectiveLift [∀ i, Projective (D.obj i)]
    {E X : Rep.{0} ℤ G} (e : E ⟶ X) [Epi e] (f : ∀ i, D.obj i ⟶ X) :
    ∀ i, D.obj i ⟶ E
  | 0 => Projective.factorThru (f 0) e
  | i + 1 => r i ≫ compatibleProjectiveLift e f i +
      (𝟙 _ - r i ≫ D.map i (i + 1) (Nat.le_succ i)) ≫
        Projective.factorThru (f (i + 1)) e
  2. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.compatibleProjectiveLift_comp line 30
  3. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.compatibleProjectiveLift_step line 43
  4. theorem OAI.PolycyclicRecognition.SequentialRepresentationDiagram.split_colimit_projective line 52