OAI/GroupTheory/PolycyclicRecognition/Finiteness/ControlledCochainHomotopy.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Close coarse maps give homotopic controlled pullbacks

  1. def OAI.PolycyclicRecognition.controlledPrismHom line 12
  2. theorem OAI.PolycyclicRecognition.controlledPrismHom_succ line 21
  3. def OAI.PolycyclicRecognition.controlledCochainHomotopy line 30

    Source documentation

    The controlled-support estimate promotes the simplicial prism to an actual homotopy between the two cochain maps.

    def controlledCochainHomotopy (e e' : GroupCoarseEquivalence G H)
    (hc : (Set.range fun x => (e.toFun x)⁻¹ * e'.toFun x).Finite) :
    Homotopy (controlledCochainMap (R := R) e) (controlledCochainMap e') where
…

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