OAI/Algebra/Finitistic/Bar/LiteralMultibarCoordinates.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DerivedBar.RecursiveTotal.inputDegree line 14

   Source documentation

   The final input degree, separated from all bar lengths.

   def inputDegree : (r : ℕ) → {n : ℕ} → Index r n → ℕ
     | 0, n, _ => n
     | r+1, _, ⟨_,t⟩ => inputDegree r t
   
   /-- The literal slots from the X bars, ordered outside to inside. -/

   Mentions: OAI.DerivedBar.RecursiveTotal.Index

2. def OAI.DerivedBar.RecursiveTotal.innerPattern line 19

   Source documentation

   The literal slots from the X bars, ordered outside to inside.

   def innerPattern : (r : ℕ) → {n : ℕ} → Index r n → List Bool
     | 0, _, _ => []
     | r+1, _, ⟨p,t⟩ => true :: (List.replicate p.val.1 false ++ innerPattern r t)

   Mentions: OAI.DerivedBar.RecursiveTotal.Index

3. theorem OAI.DerivedBar.RecursiveTotal.count_innerPattern line 23
4. theorem OAI.DerivedBar.RecursiveTotal.length_innerPattern line 31
5. def OAI.DerivedBar.RecursiveTotal.leadingPattern line 43

   Source documentation

   Leading internal D slots; the exterior D coefficient is kept separate.

   def leadingPattern (r n : ℕ) (t : Index (r+1) n) : List Bool :=
   …

   Mentions: OAI.DerivedBar.RecursiveTotal.Index

6. theorem OAI.DerivedBar.RecursiveTotal.count_leadingPattern line 46
7. theorem OAI.DerivedBar.RecursiveTotal.length_leadingPattern line 50
8. def OAI.DerivedBar.RecursiveTotal.innerSummandIso line 68

   Source documentation

   Every inner summand is isomorphic, D-linearly, to its literal field tensor.

   def innerSummandIso : (r n : ℕ) → (t : Index r n) →
       summand (fun _ => XB) Z r n t ≅
         ModuleCat.of D (patternTerm k D X (Z.X (inputDegree r t)) (innerPattern r t))
     | 0, _, _ => Iso.refl _
     | r+1, _, ⟨p,t⟩ =>
       (XB ⋙ HomologicalComplex.eval _ c p.val.1).mapIso (innerSummandIso r p.val.2 t) ≪≫
         twoSidedBarPatternIso k D X (Z.X (inputDegree r t)) p.val.1 (innerPattern r t)
   
   /-- The prefix of the leading sequence is exactly the sequence of X bars,
   also at the literal summand level. -/

   Mentions: OAI.DerivedBar.RecursiveTotal.Index, OAI.DerivedBar.RecursiveTotal.summand, OAI.DerivedBar.RecursiveTotal.inputDegree, OAI.DerivedBar.RecursiveTotal.innerPattern

9. theorem OAI.DerivedBar.RecursiveTotal.leadingSummand_prefix line 78

   Source documentation

   The prefix of the leading sequence is exactly the sequence of X bars, also at the literal summand level.

   theorem leadingSummand_prefix (r m n : ℕ) (h : m≤r) (t : Index m n) :
       summand (leadingBarSequence k D X r) Z m n t = summand (fun _ => XB) Z m n t := by
   …

   Mentions: OAI.DerivedBar.RecursiveTotal.Index, OAI.DerivedBar.RecursiveTotal.summand, OAI.DerivedBar.leadingBarSequence

10. def OAI.DerivedBar.RecursiveTotal.leadingSummandIso line 90

    Source documentation

    The source tensor D ⊗ D^i₀ ⊗ X ⊗ ... ⊗ D^iᵣ ⊗ Z^q, with every field scalar action and every exterior D action checked.

    def leadingSummandIso (r n : ℕ) (t : Index (r+1) n) :
        summand (leadingBarSequence k D X r) Z (r+1) n t ≅
          ModuleCat.of D (D ⊗[k]
            patternTerm k D X (Z.X (inputDegree (r+1) t)) (leadingPattern r n t)) := by
    …

    Mentions: OAI.DerivedBar.RecursiveTotal.Index, OAI.DerivedBar.RecursiveTotal.summand, OAI.DerivedBar.leadingBarSequence, OAI.DerivedBar.RecursiveTotal.inputDegree, OAI.DerivedBar.RecursiveTotal.leadingPattern