TwoSidedWeight.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DerivedBar.SquareZero.twoSidedWeight line 16
Source documentation
Count-r submodule of the two-sided bar term, with the leading D coefficient uncounted.
```
def twoSidedWeight (n r : ℕ) : Submodule D (D ⊗[k] term k (TrivSqZeroExt D X) N n) :=
…
```
Mentions: OAI.DerivedBar.term
theorem OAI.DerivedBar.SquareZero.word_count_le line 22
theorem OAI.DerivedBar.SquareZero.weight_eq_bot_of_lt line 29
theorem OAI.DerivedBar.SquareZero.twoSidedWeight_eq_bot_of_lt line 35
Source documentation
A count-r two-sided bar term is zero below degree r.
```
theorem twoSidedWeight_eq_bot_of_lt {n r : ℕ} (h : n < r) :
    twoSidedWeight k D X N n r = ⊥ := by
…
```
Mentions: OAI.DerivedBar.SquareZero.twoSidedWeight
theorem OAI.DerivedBar.SquareZero.tensor_weight_mem line 41
theorem OAI.DerivedBar.SquareZero.coefficient_weight_mem line 52
Source documentation
Projection of the leading square-zero coefficient kills an ideal letter and retains a base letter.
```
theorem coefficient_weight_mem {n r : ℕ}
    {v : term k (TrivSqZeroExt D X) N (n+1)} (hv : v ∈ weight k D X N (n+1) r) :
    FreeBaseChange.coefficient (fstHom k D X) (term k (TrivSqZeroExt D X) N n) v ∈
      twoSidedWeight k D X N n r := by
…
```
Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.weight, OAI.DerivedBar.FreeBaseChange.coefficient, OAI.DerivedBar.SquareZero.twoSidedWeight

theorem OAI.DerivedBar.SquareZero.twoSidedDifferential_mem line 73

Source documentation

The actual D-linear two-sided differential preserves X-count; no flatness enters the proof.

theorem twoSidedDifferential_mem
    (hN : ∀ (x : X) (v : N), (inr x : TrivSqZeroExt D X) • v = 0)
    (n r : ℕ) {v : D ⊗[k] term k (TrivSqZeroExt D X) N (n+1)}
    (hv : v ∈ twoSidedWeight k D X N (n+1) r) :
    twoSidedDifferential k (TrivSqZeroExt D X) D N (fstHom k D X) n v ∈
      twoSidedWeight k D X N n r := by
…

Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.twoSidedWeight, OAI.DerivedBar.twoSidedDifferential

def OAI.DerivedBar.SquareZero.twoSidedWeightComplex line 95
Source documentation
A genuine D-module chain complex for each fixed number of square-zero entries.
```
def twoSidedWeightComplex
    (hN : ∀ (x : X) (v : N), (inr x : TrivSqZeroExt D X) • v = 0) (r : ℕ) :
    ChainComplex (ModuleCat D) ℕ :=
…
```