TupleChains.lean`

36 declarations, 0 contain sorry, 0 declared as axioms

Tuple chains, subdivision, chain maps, and support control.

def OAI.Kaplansky.tupleSSet line 19
Source documentation
Ordered tuples, with deletion and repetition of vertices.
```
def tupleSSet (E : Type) : SSet.{0} where
…
```
abbrev OAI.Kaplansky.tupleChains line 23
abbrev OAI.Kaplansky.tupleGen line 24
theorem OAI.Kaplansky.tupleChains_hom_ext line 28
Source documentation
Maps from tuple chains are determined by their values on tuple generators.
```
theorem tupleChains_hom_ext {E : Type} {n : ℕ} {T : ModuleCat.{0} ℤ}
    {f g : (tupleChains E).X n ⟶ T}
    (h : ∀ v : Fin (n+1) → E, tupleGen v ≫ f = tupleGen v ≫ g) : f = g :=
…
```
Mentions: OAI.Kaplansky.tupleChains, OAI.Kaplansky.tupleGen
theorem OAI.Kaplansky.tupleGen_d line 34
def OAI.Kaplansky.tupleCone line 40
Source documentation
Prepending a fixed vertex, extended linearly on actual free chains.
```
def tupleCone {E : Type} (p : E) (n : ℕ) :
    (tupleChains E).X n ⟶ (tupleChains E).X (n+1) :=
…
```
Mentions: OAI.Kaplansky.tupleChains
theorem OAI.Kaplansky.tupleGen_cone line 45
def OAI.Kaplansky.tupleAugmentation line 50
Source documentation
Augmentation of zero-chains.
```
def tupleAugmentation (E : Type) : (tupleChains E).X 0 ⟶ ModuleCat.of ℤ ℤ :=
…
```
Mentions: OAI.Kaplansky.tupleChains
theorem OAI.Kaplansky.tupleGen_augmentation line 54
theorem OAI.Kaplansky.tuple_d_augmentation line 59
theorem OAI.Kaplansky.tupleCone_d_zero line 67

theorem OAI.Kaplansky.tupleCone_d line 85

Source documentation

The cone boundary identity in positive degree.

theorem tupleCone_d {E : Type} (p : E) (n : ℕ) :
    tupleCone p (n+1) ≫ (tupleChains E).d (n+2) (n+1) =
      𝟙 _ - (tupleChains E).d (n+1) n ≫ tupleCone p n := by
…

Mentions: OAI.Kaplansky.tupleCone, OAI.Kaplansky.tupleChains

def OAI.Kaplansky.tupleSubdivisionMap line 109
Source documentation
A center is chosen for each positive-dimensional tuple. The chain identity does not require a metric; barycenters will supply mesh control.
```
def tupleSubdivisionMap (b : ∀ n : ℕ, (Fin (n+2) → E) → E) :
    ∀ n, (tupleChains E).X n ⟶ (tupleChains E).X n := fun n => match n with
…
```
Mentions: OAI.Kaplansky.tupleChains
theorem OAI.Kaplansky.tupleSubdivisionMap_zero line 116
theorem OAI.Kaplansky.tupleGen_subdivision_succ line 120

theorem OAI.Kaplansky.tupleSubdivisionMap_d line 129

Source documentation

Subdivision commutes with the actual alternating boundary.

theorem tupleSubdivisionMap_d (b : ∀ n : ℕ, (Fin (n+2) → E) → E) (n : ℕ) :
    tupleSubdivisionMap b (n+1) ≫ (tupleChains E).d (n+1) n =
      (tupleChains E).d (n+1) n ≫ tupleSubdivisionMap b n := by
…

Mentions: OAI.Kaplansky.tupleSubdivisionMap, OAI.Kaplansky.tupleChains

def OAI.Kaplansky.tupleSubdivision line 149
Source documentation
A constructed chain endomorphism, for any supplied centers.
```
def tupleSubdivision (b : ∀ n : ℕ, (Fin (n+2) → E) → E) :
    tupleChains E ⟶ tupleChains E :=
…
```
Mentions: OAI.Kaplansky.tupleChains
def OAI.Kaplansky.tupleSubdivisionPrism line 155
Source documentation
The prism is filled by a cone after subtracting its prescribed boundary. This recursion constructs the homotopy; it is not a homotopy premise.
```
def tupleSubdivisionPrism (b : ∀ n : ℕ, (Fin (n+2) → E) → E) :
    ∀ n, (tupleChains E).X n ⟶ (tupleChains E).X (n+1) := fun n => match n with
…
```
Mentions: OAI.Kaplansky.tupleChains
theorem OAI.Kaplansky.tupleSubdivisionPrism_zero line 164
theorem OAI.Kaplansky.tupleGen_prism_succ line 168

theorem OAI.Kaplansky.tupleCone_cycle line 177

Source documentation

A cone fills every positive-dimensional cycle in tuple chains.

theorem tupleCone_cycle (p : E) (n : ℕ) {A : ModuleCat.{0} ℤ}
    (z : A ⟶ (tupleChains E).X (n+1))
    (hz : z ≫ (tupleChains E).d (n+1) n = 0) :
    z ≫ tupleCone p (n+1) ≫ (tupleChains E).d (n+2) (n+1) = z := by
…

Mentions: OAI.Kaplansky.tupleChains, OAI.Kaplansky.tupleCone

theorem OAI.Kaplansky.tupleSubdivisionPrism_equation line 185

Source documentation

The full positive-degree chain-homotopy equation.

theorem tupleSubdivisionPrism_equation (b : ∀ n : ℕ, (Fin (n+2) → E) → E) (n : ℕ) :
    tupleSubdivisionPrism b (n+1) ≫ (tupleChains E).d (n+2) (n+1) =
      𝟙 _ - tupleSubdivisionMap b (n+1) -
      (tupleChains E).d (n+1) n ≫ tupleSubdivisionPrism b n := by
…

Mentions: OAI.Kaplansky.tupleSubdivisionPrism, OAI.Kaplansky.tupleChains, OAI.Kaplansky.tupleSubdivisionMap

def OAI.Kaplansky.chainHomotopyOfComponents line 227
def OAI.Kaplansky.tupleSubdivisionHomotopy line 244
Source documentation
Subdivision is chain homotopic to the identity.
```
def tupleSubdivisionHomotopy (b : ∀ n : ℕ, (Fin (n+2) → E) → E) :
    Homotopy (𝟙 (tupleChains E)) (tupleSubdivision b) :=
…
```
Mentions: OAI.Kaplansky.tupleChains, OAI.Kaplansky.tupleSubdivision
def OAI.Kaplansky.tupleSSetMap line 257
Source documentation
Applying a function to each vertex defines a simplicial map.
```
def tupleSSetMap (f : E → F) : tupleSSet E ⟶ tupleSSet F where
…
```
Mentions: OAI.Kaplansky.tupleSSet
abbrev OAI.Kaplansky.tupleChainMap line 260
theorem OAI.Kaplansky.tupleGen_map line 264
theorem OAI.Kaplansky.tupleCone_map line 270

theorem OAI.Kaplansky.tupleSubdivisionMap_naturality line 279

Source documentation

Naturality of subdivision for center-preserving vertex maps.

theorem tupleSubdivisionMap_naturality
    (b : ∀ n : ℕ, (Fin (n+2) → E) → E)
    (c : ∀ n : ℕ, (Fin (n+2) → F) → F)
    (f : E → F) (hb : ∀ n v, f (b n v) = c n (f ∘ v)) (n : ℕ) :
    tupleSubdivisionMap b n ≫ (tupleChainMap f).f n =
      (tupleChainMap f).f n ≫ tupleSubdivisionMap c n := by
…

Mentions: OAI.Kaplansky.tupleSubdivisionMap, OAI.Kaplansky.tupleChainMap

theorem OAI.Kaplansky.tupleSubdivisionPrism_naturality line 298

Source documentation

The explicit subdivision homotopy has the same naturality.

theorem tupleSubdivisionPrism_naturality
    (b : ∀ n : ℕ, (Fin (n+2) → E) → E)
    (c : ∀ n : ℕ, (Fin (n+2) → F) → F)
    (f : E → F) (hb : ∀ n v, f (b n v) = c n (f ∘ v)) (n : ℕ) :
    tupleSubdivisionPrism b n ≫ (tupleChainMap f).f (n+1) =
      (tupleChainMap f).f n ≫ tupleSubdivisionPrism c n := by
…

Mentions: OAI.Kaplansky.tupleSubdivisionPrism, OAI.Kaplansky.tupleChainMap

def OAI.Kaplansky.tupleChainSpan line 324
Source documentation
Integral chains spanned by tuples satisfying a specified support condition.
```
def tupleChainSpan {n : ℕ} (P : (Fin (n+1) → E) → Prop) :
    Submodule ℤ ((tupleChains E).X n) :=
…
```
Mentions: OAI.Kaplansky.tupleChains
theorem OAI.Kaplansky.tupleGen_mem_span line 328

theorem OAI.Kaplansky.tupleChainSpan_map line 334

Source documentation

To control a linear operator on supported chains, it suffices to control each supported generator.

theorem tupleChainSpan_map {n m : ℕ} {P : (Fin (n+1) → E) → Prop}
    {Q : (Fin (m+1) → F) → Prop}
    (L : (tupleChains E).X n ⟶ (tupleChains F).X m)
    (hL : ∀ v, P v → L (tupleGen v (1 : ℤ)) ∈ tupleChainSpan Q)
    {c : (tupleChains E).X n} (hc : c ∈ tupleChainSpan P) : L c ∈ tupleChainSpan Q := by
…

Mentions: OAI.Kaplansky.tupleChains, OAI.Kaplansky.tupleGen, OAI.Kaplansky.tupleChainSpan

theorem OAI.Kaplansky.tupleChainSpan_mono line 345

theorem OAI.Kaplansky.tupleCone_mem_span line 353

Source documentation

Coning preserves the support condition exactly when prepending its vertex preserves the generator condition.

theorem tupleCone_mem_span {n : ℕ} (p : E)
    {P : (Fin (n+1) → E) → Prop} {Q : (Fin (n+2) → E) → Prop}
    (h : ∀ v, P v → Q (Fin.cons p v))
    {c : (tupleChains E).X n} (hc : c ∈ tupleChainSpan P) :
    tupleCone p n c ∈ tupleChainSpan Q := by
…

Mentions: OAI.Kaplansky.tupleChains, OAI.Kaplansky.tupleChainSpan, OAI.Kaplansky.tupleCone

theorem OAI.Kaplansky.tupleSubdivision_gen_value line 364

Source documentation

The recursive subdivision formula evaluated as an actual chain.

theorem tupleSubdivision_gen_value (b : ∀ n : ℕ, (Fin (n+2) → E) → E)
    {n : ℕ} (v : Fin (n+2) → E) :
    tupleSubdivisionMap b (n+1) (tupleGen v (1 : ℤ)) =
      ∑ i : Fin (n+2), (-1 : ℤ)^i.val •
        tupleCone (b n v) n (tupleSubdivisionMap b n (tupleGen (v ∘ i.succAbove) (1 : ℤ))) := by
…

Mentions: OAI.Kaplansky.tupleSubdivisionMap, OAI.Kaplansky.tupleGen, OAI.Kaplansky.tupleCone