MultibarSigns.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DerivedBar.SquareZero.sign_square line 11

def OAI.DerivedBar.SquareZero.signedProjection line 23

Source documentation

Projection to count r, rescaled by one minus sign per base/ideal inversion. For block lengths i₀,...,iᵣ the exponent is Σⱼ (r-j)iⱼ.

def signedProjection : (n r : ℕ) → Module.End k (term k (TrivSqZeroExt D X) N n)
  | 0, 0 => LinearMap.id
  | 0, _+1 => 0
  | n+1, 0 => TensorProduct.map (baseProjection k D X) (signedProjection n 0)
  | n+1, r+1 => (-1 : k)^(r+1) •
      TensorProduct.map (baseProjection k D X) (signedProjection n (r+1)) +
      TensorProduct.map (idealProjection k D X) (signedProjection n r)

Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.baseProjection, OAI.DerivedBar.SquareZero.idealProjection

theorem OAI.DerivedBar.SquareZero.signedProjection_base line 31
theorem OAI.DerivedBar.SquareZero.signedProjection_ideal_zero line 38
theorem OAI.DerivedBar.SquareZero.signedProjection_ideal_succ line 43
theorem OAI.DerivedBar.SquareZero.signedProjection_word_mem line 52
Source documentation
The rescaling stays inside the actual count subspace.
```
theorem signedProjection_word_mem {n r : ℕ} {v : term k (TrivSqZeroExt D X) N n}
    (hv : Word k D X N n r v) :
    signedProjection k D X N n r v ∈ weight k D X N n r := by
…
```
Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.Word, OAI.DerivedBar.SquareZero.signedProjection, OAI.DerivedBar.SquareZero.weight
theorem OAI.DerivedBar.SquareZero.signedProjection_sq_word line 65
Source documentation
The sign rescaling is its own inverse on homogeneous pure tensors.
```
theorem signedProjection_sq_word {n r : ℕ} {v : term k (TrivSqZeroExt D X) N n}
    (hv : Word k D X N n r v) :
    signedProjection k D X N n r (signedProjection k D X N n r v) = v := by
…
```
Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.Word, OAI.DerivedBar.SquareZero.signedProjection
theorem OAI.DerivedBar.SquareZero.signedProjection_mem line 76
theorem OAI.DerivedBar.SquareZero.signedProjection_sq line 85
Source documentation
Involutivity holds on the entire submodule, including sums of block tensors.
```
theorem signedProjection_sq {n r : ℕ} {v : term k (TrivSqZeroExt D X) N n}
    (hv : v ∈ weight k D X N n r) :
    signedProjection k D X N n r (signedProjection k D X N n r v) = v := by
…
```
Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.weight, OAI.DerivedBar.SquareZero.signedProjection
def OAI.DerivedBar.SquareZero.twoSidedSignedProjection line 100
Source documentation
The signed count operator preserves the exterior left D-action.
```
def twoSidedSignedProjection (n r : ℕ) :
    Module.End D (D ⊗[k] term k (TrivSqZeroExt D X) N n) :=
…
```
Mentions: OAI.DerivedBar.term
theorem OAI.DerivedBar.SquareZero.twoSidedSignedProjection_mem line 106
theorem OAI.DerivedBar.SquareZero.twoSidedSignedProjection_sq line 117
def OAI.DerivedBar.SquareZero.signEquiv line 135
Source documentation
Actual D-linear involution giving the manuscript's component rescaling. This alone is not the chain comparison or the derived tensor identification.
```
def signEquiv (n r : ℕ) : twoSidedWeight k D X N n r ≃ₗ[D]
    twoSidedWeight k D X N n r where
…
```
Mentions: OAI.DerivedBar.SquareZero.twoSidedWeight