SignedBlockExplicit.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DerivedBar.SquareZero.multibarTwoSided_eq_conjugate line 21
Source documentation
The explicit faces equal the conjugated ordinary faces; this is a theorem, not the definition of the independent differential.
```
theorem multibarTwoSided_eq_conjugate (n r : ℕ)
    {z : D ⊗[k] term k A N (n+1)} (hz : z ∈ twoSidedWeight k D X N (n+1) r) :
    multibarTwoSidedDifferential k D X N n z =
      (-1 : k)^r • twoSidedSignedProjection k D X N n r
        (twoSidedDifferential k A D N (fstHom k D X) n
          (twoSidedSignedProjection k D X N (n+1) r z)) := by
…
```
Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.twoSidedWeight, OAI.DerivedBar.SquareZero.multibarTwoSidedDifferential, OAI.DerivedBar.SquareZero.twoSidedSignedProjection, OAI.DerivedBar.twoSidedDifferential
theorem OAI.DerivedBar.SquareZero.multibarTwoSided_mem line 32
theorem OAI.DerivedBar.SquareZero.multibarTwoSided_shifted line 41
def OAI.DerivedBar.SquareZero.multibarCountDifferential line 51
Source documentation
Restriction of the independently defined literal faces to count r.
```
def multibarCountDifferential (n r : ℕ) :
    twoSidedWeight k D X N (n+1) r →ₗ[D] twoSidedWeight k D X N n r :=
…
```
Mentions: OAI.DerivedBar.SquareZero.twoSidedWeight
theorem OAI.DerivedBar.SquareZero.multibarCountDifferential_zero_of_lt line 58
Source documentation
There is no outgoing differential from an all-X word, or below its count. The ordinary r=0 degree-zero boundary is supplied by the chain shape.
```
theorem multibarCountDifferential_zero_of_lt (n r : ℕ) (hn : n < r) :
    multibarCountDifferential k D X N hN n r = 0 := by
…
```
Mentions: OAI.DerivedBar.SquareZero.multibarCountDifferential
def OAI.DerivedBar.Multibar.Indexed.explicitBlockDifferential line 79
Source documentation
Literal multibar faces on the direct sum of actual tensor blocks, with the [r] sign. Only the degreewise tensor decomposition is used for coordinates.
```
def explicitBlockDifferential (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_eq_explicit line 88
Source documentation
The previously transported signed differential is identified with independent literal faces, including the endpoint and square-zero empty-block cases.
```
theorem blockDifferential_eq_explicit (n r : ℕ) :
    blockDifferential k D X N hN n r = explicitBlockDifferential k D X N hN n r := by
…
```
Mentions: OAI.DerivedBar.Multibar.Indexed.blockDifferential, OAI.DerivedBar.Multibar.Indexed.explicitBlockDifferential
theorem OAI.DerivedBar.Multibar.Indexed.explicitBlockDifferential_sq line 109
Source documentation
Square-zero follows after identifying the independent differential with the verified chain differential; no transported differential was used to define it.
```
theorem explicitBlockDifferential_sq (n r : ℕ) :
    (explicitBlockDifferential k D X N hN n r).comp
      (explicitBlockDifferential k D X N hN (n+1) r) = 0 := by
…
```
Mentions: OAI.DerivedBar.Multibar.Indexed.explicitBlockDifferential
theorem OAI.DerivedBar.Multibar.Indexed.explicitBlockDifferential_zero_of_lt line 115