OAI/GroupTheory/PolycyclicRecognition/Finiteness/ControlledCochainMap.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Coarse pullback as a map of controlled cochain complexes

  1. def OAI.PolycyclicRecognition.controlledCochainMap line 13

    Source documentation

    Coarse pullback commutes with the actual homogeneous differential.

    def controlledCochainMap (e : GroupCoarseEquivalence G H) :
    controlledCochainComplex R H ⟶ controlledCochainComplex R G :=
…

    Mentions: OAI.PolycyclicRecognition.GroupCoarseEquivalence, OAI.PolycyclicRecognition.controlledCochainComplex

  2. theorem OAI.PolycyclicRecognition.controlledCochainMap_apply line 25
  3. theorem OAI.PolycyclicRecognition.controlledCochainMap_trans line 31

    Source documentation

    Pullback on complexes reverses composition.

    theorem controlledCochainMap_trans (e : GroupCoarseEquivalence G H)
    (e' : GroupCoarseEquivalence H J) :
    controlledCochainMap (R := R) (e.trans e') =
…

    Mentions: OAI.PolycyclicRecognition.GroupCoarseEquivalence, OAI.PolycyclicRecognition.controlledCochainMap