Projection.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DerivedBar.SquareZero.baseProjection line 16
def OAI.DerivedBar.SquareZero.idealProjection line 19
theorem OAI.DerivedBar.SquareZero.baseProjection_inl line 22
theorem OAI.DerivedBar.SquareZero.baseProjection_inr line 24
theorem OAI.DerivedBar.SquareZero.idealProjection_inl line 26
theorem OAI.DerivedBar.SquareZero.idealProjection_inr line 28

def OAI.DerivedBar.SquareZero.projection line 32

Source documentation

The actual linear projection onto words with a prescribed X-count.

def projection : (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) (projection n 0)
  | n+1, r+1 => TensorProduct.map (baseProjection k D X) (projection n (r+1)) +
      TensorProduct.map (idealProjection k D X) (projection n r)

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

theorem OAI.DerivedBar.SquareZero.projection_base line 39
theorem OAI.DerivedBar.SquareZero.projection_ideal_zero line 45
theorem OAI.DerivedBar.SquareZero.projection_ideal_succ line 50
theorem OAI.DerivedBar.SquareZero.projection_word line 59
Source documentation
The projections separate homogeneous bar words exactly.
```
theorem projection_word {n s : ℕ} {v : term k (TrivSqZeroExt D X) N n}
    (hv : Word k D X N n s v) (r : ℕ) :
    projection k D X N n r v = if r = s then v else 0 := by
…
```
Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.Word, OAI.DerivedBar.SquareZero.projection
theorem OAI.DerivedBar.SquareZero.projection_self line 77
Source documentation
Identity on the whole homogeneous subspace, not merely on individual words.
```
theorem projection_self {n r : ℕ} {v : term k (TrivSqZeroExt D X) N n}
    (hv : v ∈ weight k D X N n r) : projection k D X N n r v = v := by
…
```
Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.weight, OAI.DerivedBar.SquareZero.projection
theorem OAI.DerivedBar.SquareZero.projection_other line 90
Source documentation
Distinct counts are annihilated by the projection.
```
theorem projection_other {n r s : ℕ} (hrs : r ≠ s)
    {v : term k (TrivSqZeroExt D X) N n} (hv : v ∈ weight k D X N n s) :
    projection k D X N n r v = 0 := by
…
```
Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.weight, OAI.DerivedBar.SquareZero.projection
theorem OAI.DerivedBar.SquareZero.weight_disjoint line 101
Source documentation
Homogeneous bar subspaces with distinct counts have zero intersection.
```
theorem weight_disjoint (n : ℕ) {r s : ℕ} (hrs : r ≠ s) :
    Disjoint (weight k D X N n r) (weight k D X N n s) := by
…
```
Mentions: OAI.DerivedBar.SquareZero.weight
theorem OAI.DerivedBar.SquareZero.all_words_span line 111
Source documentation
Expanding each actual algebra entry as D ⊕ X spans every absolute bar term.
```
theorem all_words_span (n : ℕ) :
    Submodule.span k {v : term k (TrivSqZeroExt D X) N n |
      ∃ r, Word k D X N n r v} = ⊤ := by
…
```
Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.Word
theorem OAI.DerivedBar.SquareZero.projection_mem line 141
Source documentation
Every value of the count projection lies in the corresponding homogeneous subspace.
```
theorem projection_mem (n r : ℕ) (v : term k (TrivSqZeroExt D X) N n) :
    projection k D X N n r v ∈ weight k D X N n r := by
…
```
Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.projection, OAI.DerivedBar.SquareZero.weight
theorem OAI.DerivedBar.SquareZero.weight_iSup line 158
Source documentation
The count subspaces span the entire bar term.
```
theorem weight_iSup (n : ℕ) : (⨆ r, weight k D X N n r) = ⊤ := by
…
```
Mentions: OAI.DerivedBar.SquareZero.weight