OAI/Algebra/Finitistic/Bar/MultibarBlocks.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DerivedBar.Multibar.count line 12

   Source documentation

   false records a D slot, true an X slot. The leading D is separate.

   def count : List Bool → ℕ
     | [] => 0
     | false :: p => count p
     | true :: p => count p + 1
   
   /-- Number of ordered pairs consisting of a D slot followed by an X slot. -/

2. def OAI.DerivedBar.Multibar.inversions line 18

   Source documentation

   Number of ordered pairs consisting of a D slot followed by an X slot.

   def inversions : List Bool → ℕ
     | [] => 0
     | false :: p => count p + inversions p
     | true :: p => inversions p
   
   /-- The r+1 block lengths, with no empty-list ambiguity at r=0. -/

   Mentions: OAI.DerivedBar.Multibar.count

3. def OAI.DerivedBar.Multibar.Blocks line 24

   Source documentation

   The r+1 block lengths, with no empty-list ambiguity at r=0.

   def Blocks : ℕ → Type
     | 0 => ℕ
     | r+1 => ℕ × Blocks r

4. def OAI.DerivedBar.Multibar.total line 28
5. def OAI.DerivedBar.Multibar.exponent line 33

   Source documentation

   This recursive sum is exactly Σⱼ (r-j)iⱼ.

   def exponent : (r : ℕ) → Blocks r → ℕ
     | 0, _ => 0
     | r+1, (i, tail) => (r+1)*i + exponent r tail

   Mentions: OAI.DerivedBar.Multibar.Blocks

6. def OAI.DerivedBar.Multibar.pattern line 37
7. theorem OAI.DerivedBar.Multibar.count_bases line 41
8. theorem OAI.DerivedBar.Multibar.inversions_bases line 47
9. theorem OAI.DerivedBar.Multibar.count_pattern line 56
10. theorem OAI.DerivedBar.Multibar.length_pattern line 64

    Source documentation

    The actual word length agrees with source cohomological degree -r-Σiⱼ.

    @[simp] theorem length_pattern (r : ℕ) (b : Blocks r) :
        (pattern r b).length = r + total r b := by
    …

    Mentions: OAI.DerivedBar.Multibar.Blocks, OAI.DerivedBar.Multibar.pattern, OAI.DerivedBar.Multibar.total

11. theorem OAI.DerivedBar.Multibar.inversions_pattern line 76

    Source documentation

    The combinatorial rescaling is exactly the component factor in prop:bar-splitting.

    @[simp] theorem inversions_pattern (r : ℕ) (b : Blocks r) :
        inversions (pattern r b) = exponent r b := by
    …

    Mentions: OAI.DerivedBar.Multibar.Blocks, OAI.DerivedBar.Multibar.inversions, OAI.DerivedBar.Multibar.pattern, OAI.DerivedBar.Multibar.exponent

12. def OAI.DerivedBar.Multibar.patternTerm line 93

    Source documentation

    Genuine iterated tensors over k for a prescribed D/X pattern, ending in N. No ordinary tensor over D is used in these bar terms.

    @[reducible] def patternTerm : List Bool → ModuleCat k
      | [] => ModuleCat.of k N
      | false :: p => ModuleCat.of k (D ⊗[k] patternTerm p)
      | true :: p => ModuleCat.of k (X ⊗[k] patternTerm p)
    
    /-- Inclusion of each D/X tensor into the actual A bar term. -/

13. def OAI.DerivedBar.Multibar.embed line 99

    Source documentation

    Inclusion of each D/X tensor into the actual A bar term.

    def embed : (p : List Bool) → patternTerm k D X N p →ₗ[k]
        DerivedBar.term k (TrivSqZeroExt D X) N p.length
      | [] => LinearMap.id
      | false :: p => TensorProduct.map (inlAlgHom k D X).toLinearMap (embed p)
      | true :: p => TensorProduct.map ((inrHom D X).restrictScalars k) (embed p)
    
    /-- Slotwise projection back to the prescribed tensor; this proves no tensor relations were lost. -/

    Mentions: OAI.DerivedBar.Multibar.patternTerm, OAI.DerivedBar.term

14. def OAI.DerivedBar.Multibar.extract line 106

    Source documentation

    Slotwise projection back to the prescribed tensor; this proves no tensor relations were lost.

    def extract : (p : List Bool) → DerivedBar.term k (TrivSqZeroExt D X) N p.length →ₗ[k]
        patternTerm k D X N p
      | [] => LinearMap.id
      | false :: p => TensorProduct.map (fstHom k D X).toLinearMap (extract p)
      | true :: p => TensorProduct.map ((sndHom D X).restrictScalars k) (extract p)
    
    /-- Every block inclusion has an actual linear left inverse. -/

    Mentions: OAI.DerivedBar.term, OAI.DerivedBar.Multibar.patternTerm

15. theorem OAI.DerivedBar.Multibar.extract_embed line 113

    Source documentation

    Every block inclusion has an actual linear left inverse.

    theorem extract_embed (p : List Bool) (v : patternTerm k D X N p) :
        extract k D X N p (embed k D X N p v) = v := by
    …

    Mentions: OAI.DerivedBar.Multibar.patternTerm, OAI.DerivedBar.Multibar.extract, OAI.DerivedBar.Multibar.embed

16. theorem OAI.DerivedBar.Multibar.embed_mem line 127

    Source documentation

    Each tensor embeds into its correct count subspace.

    theorem embed_mem (p : List Bool) (v : patternTerm k D X N p) :
        embed k D X N p v ∈ SquareZero.weight k D X N p.length (count p) := by
    …

    Mentions: OAI.DerivedBar.Multibar.patternTerm, OAI.DerivedBar.Multibar.embed, OAI.DerivedBar.SquareZero.weight, OAI.DerivedBar.Multibar.count

17. theorem OAI.DerivedBar.Multibar.signedProjection_embed line 143

    Source documentation

    Evaluation of the constructed sign operator on genuine pattern tensors.

    theorem signedProjection_embed (p : List Bool) (v : patternTerm k D X N p) :
        SquareZero.signedProjection k D X N p.length (count p) (embed k D X N p v) =
          (-1 : k)^(inversions p) • embed k D X N p v := by
    …

    Mentions: OAI.DerivedBar.Multibar.patternTerm, OAI.DerivedBar.SquareZero.signedProjection, OAI.DerivedBar.Multibar.count, OAI.DerivedBar.Multibar.embed, OAI.DerivedBar.Multibar.inversions

18. abbrev OAI.DerivedBar.Multibar.blockTerm line 166

    Source documentation

    The source block tensor, including the exterior D coefficient.

    abbrev blockTerm (r : ℕ) (b : Blocks r) := D ⊗[k] patternTerm k D X N (pattern r b)

    Mentions: OAI.DerivedBar.Multibar.Blocks, OAI.DerivedBar.Multibar.patternTerm, OAI.DerivedBar.Multibar.pattern

19. def OAI.DerivedBar.Multibar.blockEmbed line 168
20. def OAI.DerivedBar.Multibar.blockExtract line 172
21. theorem OAI.DerivedBar.Multibar.blockExtract_embed line 177
22. theorem OAI.DerivedBar.Multibar.blockEmbed_injective line 186

    Source documentation

    Actual block tensors inject, with no D-flatness hypothesis.

    theorem blockEmbed_injective (r : ℕ) (b : Blocks r) :
        Function.Injective (blockEmbed k D X N r b) :=
    …

    Mentions: OAI.DerivedBar.Multibar.Blocks, OAI.DerivedBar.Multibar.blockEmbed

23. theorem OAI.DerivedBar.Multibar.blockEmbed_mem line 190
24. theorem OAI.DerivedBar.Multibar.sign_on_block line 200

    Source documentation

    The D-linear rescaling on each source block is exactly (-1)^(Σⱼ(r-j)iⱼ).

    theorem sign_on_block (r : ℕ) (b : Blocks r) (v : blockTerm k D X N r b) :
        SquareZero.twoSidedSignedProjection k D X N (pattern r b).length r
          (blockEmbed k D X N r b v) =
            (-1 : k)^(exponent r b) • blockEmbed k D X N r b v := by
    …

    Mentions: OAI.DerivedBar.Multibar.Blocks, OAI.DerivedBar.Multibar.blockTerm, OAI.DerivedBar.SquareZero.twoSidedSignedProjection, OAI.DerivedBar.Multibar.pattern, OAI.DerivedBar.Multibar.blockEmbed, OAI.DerivedBar.Multibar.exponent