Splitting.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.DerivedBar.SquareZero.internal_of_projections line 12
theorem OAI.DerivedBar.SquareZero.weight_internal line 35
Source documentation
The homogeneous absolute bar term is an internal direct sum.
```
theorem weight_internal (n : ℕ) : DirectSum.IsInternal (weight k D X N n) :=
…
```
Mentions: OAI.DerivedBar.SquareZero.weight
def OAI.DerivedBar.SquareZero.twoSidedProjection line 41
Source documentation
Actual D-linear count projection on the two-sided bar term.
```
def twoSidedProjection (n r : ℕ) : Module.End D (D ⊗[k] term k (TrivSqZeroExt D X) N n) :=
…
```
Mentions: OAI.DerivedBar.term
theorem OAI.DerivedBar.SquareZero.twoSidedProjection_tmul line 44
theorem OAI.DerivedBar.SquareZero.twoSidedProjection_self line 50
theorem OAI.DerivedBar.SquareZero.twoSidedProjection_other line 63
theorem OAI.DerivedBar.SquareZero.twoSidedWeight_iSup line 76
Source documentation
Expansion of internal A entries as D ⊕ X spans the two-sided bar term as a D-module.
```
theorem twoSidedWeight_iSup (n : ℕ) : (⨆ r, twoSidedWeight k D X N n r) = ⊤ := by
…
```
Mentions: OAI.DerivedBar.SquareZero.twoSidedWeight
theorem OAI.DerivedBar.SquareZero.twoSidedWeight_internal line 96
Source documentation
The genuine D-module decomposition of each two-sided bar term by X-count.
```
theorem twoSidedWeight_internal (n : ℕ) : DirectSum.IsInternal (twoSidedWeight k D X N n) :=
…
```
Mentions: OAI.DerivedBar.SquareZero.twoSidedWeight
def OAI.DerivedBar.SquareZero.twoSidedWeightEquiv line 103
Source documentation
Canonical sum of homogeneous tensors, as a linear equivalence.
```
def twoSidedWeightEquiv (n : ℕ) :
    (⨁ r : ℕ, twoSidedWeight k D X N n r) ≃ₗ[D]
      D ⊗[k] term k (TrivSqZeroExt D X) N n :=
…
```
Mentions: OAI.DerivedBar.SquareZero.twoSidedWeight, OAI.DerivedBar.term