ControlledFaceSupport.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Controlled support under face maps

Deleting a vertex has finite fibers once the pairwise differences of the original tuple are bounded. This supplies the local finiteness needed by the homogeneous cochain differential.

theorem OAI.PolycyclicRecognition.IsControlledTuple.face line 20
Source documentation
Faces of a controlled tuple retain the same scale.
```
theorem IsControlledTuple.face {S : Set G} {x : Fin (n + 2) → G}
    (hx : IsControlledTuple S x) (i : Fin (n + 2)) :
    IsControlledTuple S (x ∘ i.succAbove) :=
…
```
Mentions: OAI.PolycyclicRecognition.IsControlledTuple
theorem OAI.PolycyclicRecognition.finite_controlled_face_fiber line 27
Source documentation
On controlled tuples a fixed face has only finitely many possible missing vertices.
```
theorem finite_controlled_face_fiber (S : Set G) (hS : S.Finite)
    (i : Fin (n + 2)) (y : Fin (n + 1) → G) :
    {x : Fin (n + 2) → G | IsControlledTuple S x ∧ x ∘ i.succAbove = y}.Finite := by
…
```
Mentions: OAI.PolycyclicRecognition.IsControlledTuple
def OAI.PolycyclicRecognition.controlledFace line 48
Source documentation
Face pullback preserves locally finite support.
```
def controlledFace (i : Fin (n + 2)) :
    controlledCochains R G n →ₗ[R] controlledCochains R G (n + 1) where
…
```
Mentions: OAI.PolycyclicRecognition.controlledCochains
theorem OAI.PolycyclicRecognition.controlledFace_apply line 64
def OAI.PolycyclicRecognition.controlledCoboundary line 69
Source documentation
The homogeneous coboundary, as an actual map on controlled cochains.
```
def controlledCoboundary :
    controlledCochains R G n →ₗ[R] controlledCochains R G (n + 1) :=
…
```
Mentions: OAI.PolycyclicRecognition.controlledCochains
theorem OAI.PolycyclicRecognition.controlledCoboundary_apply line 73
theorem OAI.PolycyclicRecognition.controlledCoboundary_pullback line 79
Source documentation
Coordinatewise coarse pullback commutes with the homogeneous coboundary.
```
theorem controlledCoboundary_pullback {H : Type*} [Group H]
    (e : GroupCoarseEquivalence G H) (c : controlledCochains R H n) :
    controlledCoboundary (controlledCochainPullback e n c) =
      controlledCochainPullback e (n + 1) (controlledCoboundary c) := by
…
```
Mentions: OAI.PolycyclicRecognition.GroupCoarseEquivalence, OAI.PolycyclicRecognition.controlledCochains, OAI.PolycyclicRecognition.controlledCoboundary, OAI.PolycyclicRecognition.controlledCochainPullback