SignedBlockModel.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DerivedBar.Multibar.Indexed.toList_injective line 13
Source documentation
The degree-indexed shapes faithfully record their D/X words.
```
theorem toList_injective {n r : ℕ} : Function.Injective (@toList n r) := by
…
```
Mentions: OAI.DerivedBar.Multibar.Indexed.toList
instance OAI.DerivedBar.Multibar.Indexed.shape_finite line 29
Source documentation
The block direct sum is finite in every degree, without any completion.
```
instance shape_finite (n r : ℕ) : Finite (Shape n r) :=
…
```
Mentions: OAI.DerivedBar.Multibar.Indexed.Shape
theorem OAI.DerivedBar.Multibar.Indexed.tensor_toList line 41
Source documentation
The indexed tensor is exactly the earlier literal D/X pattern tensor.
```
theorem tensor_toList {n r : ℕ} (p : Shape n r) :
    tensor k D X N p = patternTerm k D X N (toList p) := by
…
```
Mentions: OAI.DerivedBar.Multibar.Indexed.Shape, OAI.DerivedBar.Multibar.Indexed.tensor, OAI.DerivedBar.Multibar.patternTerm, OAI.DerivedBar.Multibar.Indexed.toList
theorem OAI.DerivedBar.Multibar.Indexed.inclusion_sign line 49
Source documentation
The sign involution acts by the prescribed inversion count on each tensor summand.
```
theorem inclusion_sign {n r : ℕ} (p : Shape n r) (v : tensor k D X N p) :
    SquareZero.signedProjection k D X N n r (inclusion k D X N p v) =
      (-1 : k)^(inversions (toList p)) • inclusion k D X N p v := by
…
```
Mentions: OAI.DerivedBar.Multibar.Indexed.Shape, OAI.DerivedBar.Multibar.Indexed.tensor, OAI.DerivedBar.SquareZero.signedProjection, OAI.DerivedBar.Multibar.Indexed.inclusion, OAI.DerivedBar.Multibar.inversions, OAI.DerivedBar.Multibar.Indexed.toList
theorem OAI.DerivedBar.Multibar.Indexed.outerInclusion_sign line 74
def OAI.DerivedBar.Multibar.Indexed.signedAssembly line 85
Source documentation
Summation of genuine tensor blocks followed by the source's sign rescaling.
```
def signedAssembly (n r : ℕ) : (⨁ p : Shape n r, outerTensor k D X N p) ≃ₗ[D]
    SquareZero.twoSidedWeight k D X N n r :=
…
```
Mentions: OAI.DerivedBar.Multibar.Indexed.Shape, OAI.DerivedBar.Multibar.Indexed.outerTensor, OAI.DerivedBar.SquareZero.twoSidedWeight
def OAI.DerivedBar.Multibar.Indexed.blockDifferential line 93
Source documentation
Transport of the actual count differential to signed tensor blocks.
```
def blockDifferential (n r : ℕ) :
    (⨁ p : Shape (n+1) r, outerTensor k D X N p) →ₗ[D]
      (⨁ p : Shape n r, outerTensor k D X N p) :=
…
```
Mentions: OAI.DerivedBar.Multibar.Indexed.Shape, OAI.DerivedBar.Multibar.Indexed.outerTensor
theorem OAI.DerivedBar.Multibar.Indexed.blockDifferential_sq line 100
def OAI.DerivedBar.Multibar.Indexed.signedBlockComplex line 122
Source documentation
Signed block chain model, still indexed by the full homological degree r+Σiⱼ.
```
def signedBlockComplex (r : ℕ) : ChainComplex (ModuleCat D) ℕ :=
…
```
def OAI.DerivedBar.Multibar.Indexed.signedBlockIso line 128
Source documentation
Chain isomorphism between the signed block model and the preserved count subcomplex.
```
def signedBlockIso (r : ℕ) : signedBlockComplex k D X N hN r ≅
    SquareZero.twoSidedWeightComplex k D X N hN r :=
…
```
Mentions: OAI.DerivedBar.Multibar.Indexed.signedBlockComplex, OAI.DerivedBar.SquareZero.twoSidedWeightComplex