ControlledPrism.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Closeness bounds all mixed pairs of vertices. Properness of the first vertex then gives finite fibers at each controlled scale.

theorem OAI.PolycyclicRecognition.controlled_tuplePrism line 16
def OAI.PolycyclicRecognition.controlledPrismTerm line 33
Source documentation
Each prism summand is defined on the controlled cochains themselves.
```
def controlledPrismTerm (e e' : GroupCoarseEquivalence G H)
    (hc : (Set.range fun x => (e.toFun x)⁻¹ * e'.toFun x).Finite)
    (i : Fin (n + 1)) :
    controlledCochains R H (n + 1) →ₗ[R] controlledCochains R G n where
…
```
Mentions: OAI.PolycyclicRecognition.GroupCoarseEquivalence, OAI.PolycyclicRecognition.controlledCochains
theorem OAI.PolycyclicRecognition.controlledPrismTerm_apply line 52
def OAI.PolycyclicRecognition.controlledPrism line 60
Source documentation
The negative alternating prism, with the sign convention of Mathlib's chain homotopy, lowers cochain degree by one.
```
def controlledPrism (e e' : GroupCoarseEquivalence G H)
    (hc : (Set.range fun x => (e.toFun x)⁻¹ * e'.toFun x).Finite) :
    controlledCochains R H (n + 1) →ₗ[R] controlledCochains R G n :=
…
```
Mentions: OAI.PolycyclicRecognition.GroupCoarseEquivalence, OAI.PolycyclicRecognition.controlledCochains
theorem OAI.PolycyclicRecognition.controlledPrism_apply line 65