Weight.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

inductive OAI.DerivedBar.SquareZero.Word line 18

Source documentation

(TrivSqZeroExt D X) pure bar word with precisely r factors in the square-zero ideal.

inductive Word : (n r : ℕ) → term k (TrivSqZeroExt D X) N n → Prop
  | nil (v : N) : Word 0 0 v
  | base {n r : ℕ} {v : term k (TrivSqZeroExt D X) N n} (d : D) (h : Word n r v) :
      Word (n+1) r ((inl d : (TrivSqZeroExt D X)) ⊗ₜ[k] v)
  | ideal {n r : ℕ} {v : term k (TrivSqZeroExt D X) N n} (x : X) (h : Word n r v) :
      Word (n+1) (r+1) ((inr x : (TrivSqZeroExt D X)) ⊗ₜ[k] v)

/-- The homogeneous subspace, defined by actual tensors rather than formal signs. -/

Mentions: OAI.DerivedBar.term

def OAI.DerivedBar.SquareZero.weight line 26
Source documentation
The homogeneous subspace, defined by actual tensors rather than formal signs.
```
def weight (n r : ℕ) : Submodule k (term k (TrivSqZeroExt D X) N n) :=
…
```
Mentions: OAI.DerivedBar.term
theorem OAI.DerivedBar.SquareZero.map_span_mem line 29
theorem OAI.DerivedBar.SquareZero.base_tmul_mem line 37
theorem OAI.DerivedBar.SquareZero.ideal_tmul_mem line 43
theorem OAI.DerivedBar.SquareZero.base_smul_mem line 52
Source documentation
Degree-zero multiplication preserves the number of ideal factors.
```
theorem base_smul_mem {n r : ℕ} (d : D) {v : term k (TrivSqZeroExt D X) N n}
    (hv : v ∈ weight k D X N n r) :
    (inl d : (TrivSqZeroExt D X)) • v ∈ weight k D X N n r := by
…
```
Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.weight

theorem OAI.DerivedBar.SquareZero.ideal_smul_mem line 69

Source documentation

Degree-one multiplication raises the count, with square-zero products vanishing.

theorem ideal_smul_mem (hN : ∀ (x : X) (v : N), (inr x : (TrivSqZeroExt D X)) • v = 0)
    {n r : ℕ} (x : X) {v : term k (TrivSqZeroExt D X) N n}
    (hv : v ∈ weight k D X N n r) :
    (inr x : (TrivSqZeroExt D X)) • v ∈ weight k D X N n (r+1) := by
…

Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.weight

theorem OAI.DerivedBar.SquareZero.differential_mem line 90

Source documentation

Every face of the augmented algebra bar differential preserves the X-count.

theorem differential_mem (hN : ∀ (x : X) (v : N), (inr x : (TrivSqZeroExt D X)) • v = 0)
    (n r : ℕ) {v : term k (TrivSqZeroExt D X) N (n+1)} (hv : v ∈ weight k D X N (n+1) r) :
    differential k (TrivSqZeroExt D X) N n v ∈ weight k D X N n r := by
…

Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.weight, OAI.DerivedBar.differential

def OAI.DerivedBar.SquareZero.weightComplex line 124
Source documentation
The actual complex formed by the fixed-count homogeneous bar subspaces.
```
def weightComplex (hN : ∀ (x : X) (v : N), (inr x : (TrivSqZeroExt D X)) • v = 0) (r : ℕ) :
    ChainComplex (ModuleCat k) ℕ :=
…
```