ControlledCochains.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Cochains with finite support on controlled tuples

These are the scalar homogeneous cochains used to compare group-ring cohomology under a coarse equivalence. Support is finite after restricting all pairwise differences to any finite set. The pullback below uses both bounded-difference control and finite fibers of the coarse map.

def OAI.PolycyclicRecognition.IsControlledTuple line 21
Source documentation
All pairwise differences of a tuple belong to the indicated finite scale.
```
def IsControlledTuple {n : ℕ} (S : Set G) (x : Fin (n + 1) → G) : Prop :=
…
```
def OAI.PolycyclicRecognition.controlledCochains line 25
Source documentation
Homogeneous scalar cochains, locally finite on every controlled set.
```
def controlledCochains (G : Type*) [Group G] (n : ℕ) :
    Submodule R ((Fin (n + 1) → G) → R) where
…
```
instance OAI.PolycyclicRecognition.(instance at line 46) line 46
theorem OAI.PolycyclicRecognition.GroupCoarseEquivalence.finite_preimage line 50
Source documentation
A coarse equivalence has finite inverse images of finite sets.
```
theorem GroupCoarseEquivalence.finite_preimage (e : GroupCoarseEquivalence G H)
    (S : Set H) (hS : S.Finite) : (e.toFun ⁻¹' S).Finite :=
…
```
Mentions: OAI.PolycyclicRecognition.GroupCoarseEquivalence
theorem OAI.PolycyclicRecognition.GroupCoarseEquivalence.finite_tuple_fiber line 55
Source documentation
Coordinatewise pullback retains properness on finite tuple spaces.
```
theorem GroupCoarseEquivalence.finite_tuple_fiber (e : GroupCoarseEquivalence G H)
    (n : ℕ) (y : Fin (n + 1) → H) :
    {x : Fin (n + 1) → G | e.toFun ∘ x = y}.Finite := by
…
```
Mentions: OAI.PolycyclicRecognition.GroupCoarseEquivalence
def OAI.PolycyclicRecognition.controlledCochainPullback line 72
Source documentation
Pullback is well-defined because controlled tuples map to controlled tuples and the map on tuples has finite fibers.
```
def controlledCochainPullback (e : GroupCoarseEquivalence G H) (n : ℕ) :
    controlledCochains R H n →ₗ[R] controlledCochains R G n where
…
```
Mentions: OAI.PolycyclicRecognition.GroupCoarseEquivalence, OAI.PolycyclicRecognition.controlledCochains
theorem OAI.PolycyclicRecognition.controlledCochainPullback_apply line 85

theorem OAI.PolycyclicRecognition.controlledCochainPullback_trans line 90

Source documentation

Cochain pullback reverses composition of coarse maps.

theorem controlledCochainPullback_trans {J : Type*} [Group J]
    (e : GroupCoarseEquivalence G H) (e' : GroupCoarseEquivalence H J) (n : ℕ)
    (c : controlledCochains R J n) :
    controlledCochainPullback (e.trans e') n c =
      controlledCochainPullback e n (controlledCochainPullback e' n c) := rfl
…

Mentions: OAI.PolycyclicRecognition.GroupCoarseEquivalence, OAI.PolycyclicRecognition.controlledCochains, OAI.PolycyclicRecognition.controlledCochainPullback