OAI/Algebra/Finitistic/Bar/MultibarDecomposition.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.DerivedBar.Multibar.Indexed.Shape line 12

   Source documentation

   A D/X pattern with length and X-count in its type, avoiding any degree casts.

   inductive Shape : ℕ → ℕ → Type
     | nil : Shape 0 0
     | base {n r : ℕ} : Shape n r → Shape (n+1) r
     | ideal {n r : ℕ} : Shape n r → Shape (n+1) (r+1)
   
   local instance (n r : ℕ) : DecidableEq (Shape n r) := Classical.decEq _

2. def OAI.DerivedBar.Multibar.Indexed.toList line 19
3. theorem OAI.DerivedBar.Multibar.Indexed.length_toList line 24
4. theorem OAI.DerivedBar.Multibar.Indexed.count_toList line 27
5. def OAI.DerivedBar.Multibar.Indexed.tensor line 35
6. def OAI.DerivedBar.Multibar.Indexed.inclusion line 40
7. def OAI.DerivedBar.Multibar.Indexed.retraction line 46
8. theorem OAI.DerivedBar.Multibar.Indexed.retraction_inclusion line 52
9. theorem OAI.DerivedBar.Multibar.Indexed.retraction_other line 70

   Source documentation

   Distinct patterns are separated by slotwise projections, including non-flat bimodules.

   theorem retraction_other {n r : ℕ} (p q : Shape n r) (hpq : p ≠ q)
       (v : tensor k D X N q) : retraction k D X N p (inclusion k D X N q v) = 0 := by
   …

   Mentions: OAI.DerivedBar.Multibar.Indexed.Shape, OAI.DerivedBar.Multibar.Indexed.tensor, OAI.DerivedBar.Multibar.Indexed.retraction, OAI.DerivedBar.Multibar.Indexed.inclusion

10. theorem OAI.DerivedBar.Multibar.Indexed.inclusion_mem line 101
11. theorem OAI.DerivedBar.Multibar.Indexed.word_inclusion line 115

    Source documentation

    Every homogeneous word is an actual tensor in one of the prescribed blocks.

    theorem word_inclusion {n r : ℕ} {z : DerivedBar.term k (TrivSqZeroExt D X) N n}
        (hz : SquareZero.Word k D X N n r z) :
        ∃ (p : Shape n r) (v : tensor k D X N p), inclusion k D X N p v = z := by
    …

    Mentions: OAI.DerivedBar.term, OAI.DerivedBar.SquareZero.Word, OAI.DerivedBar.Multibar.Indexed.Shape, OAI.DerivedBar.Multibar.Indexed.tensor, OAI.DerivedBar.Multibar.Indexed.inclusion

12. abbrev OAI.DerivedBar.Multibar.Indexed.outerTensor line 127
13. def OAI.DerivedBar.Multibar.Indexed.outerInclusion line 129
14. def OAI.DerivedBar.Multibar.Indexed.outerRetraction line 133
15. theorem OAI.DerivedBar.Multibar.Indexed.outerRetraction_inclusion line 137
16. theorem OAI.DerivedBar.Multibar.Indexed.outerRetraction_other line 145
17. theorem OAI.DerivedBar.Multibar.Indexed.outerInclusion_mem line 154
18. def OAI.DerivedBar.Multibar.Indexed.assemble line 161

    Source documentation

    The actual sum of all tensor-block inclusions in count r and degree n.

    def assemble (n r : ℕ) : (⨁ p : Shape n r, outerTensor k D X N p) →ₗ[D]
        SquareZero.twoSidedWeight k D X N n r :=
    …

    Mentions: OAI.DerivedBar.Multibar.Indexed.Shape, OAI.DerivedBar.Multibar.Indexed.outerTensor, OAI.DerivedBar.SquareZero.twoSidedWeight

19. theorem OAI.DerivedBar.Multibar.Indexed.assemble_surjective line 167

    Source documentation

    Surjectivity is proved from the original homogeneous-word spanning definition.

    theorem assemble_surjective (n r : ℕ) : Function.Surjective (assemble k D X N n r) := by
    …

    Mentions: OAI.DerivedBar.Multibar.Indexed.assemble

20. theorem OAI.DerivedBar.Multibar.Indexed.outerRetraction_assemble line 187

    Source documentation

    Projection onto an actual block after summation recovers the direct-sum component.

    theorem outerRetraction_assemble (n r : ℕ) (p : Shape n r)
        (z : ⨁ p : Shape n r, outerTensor k D X N p) :
        outerRetraction k D X N p (assemble k D X N n r z) = z p := by
    …

    Mentions: OAI.DerivedBar.Multibar.Indexed.Shape, OAI.DerivedBar.Multibar.Indexed.outerTensor, OAI.DerivedBar.Multibar.Indexed.outerRetraction, OAI.DerivedBar.Multibar.Indexed.assemble

21. def OAI.DerivedBar.Multibar.Indexed.decomposition line 210

    Source documentation

    The block direct sum is linearly isomorphic to the entire actual count submodule.

    def decomposition (n r : ℕ) : (⨁ p : Shape n r, outerTensor k D X N p) ≃ₗ[D]
        SquareZero.twoSidedWeight k D X N n r :=
    …

    Mentions: OAI.DerivedBar.Multibar.Indexed.Shape, OAI.DerivedBar.Multibar.Indexed.outerTensor, OAI.DerivedBar.SquareZero.twoSidedWeight