OAI/Algebra/Finitistic/Bar/PatternTensorCoherence.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.DerivedBar.Multibar.patternModule line 16

   Source documentation

   The exterior D action on a literal pattern is the action on its first slot.

   @[reducible] instance patternModule : (p : List Bool) → Module D (patternTerm k D X N p)
     | [] => inferInstanceAs (Module D N)
     | false :: p => inferInstanceAs (Module D (D ⊗[k] patternTerm k D X N p))
     | true :: p => inferInstanceAs (Module D (X ⊗[k] patternTerm k D X N p))

   Mentions: OAI.DerivedBar.Multibar.patternTerm

2. instance OAI.DerivedBar.Multibar.patternTower line 21
3. theorem OAI.DerivedBar.Multibar.term_pattern line 29

   Source documentation

   Prefixing i D slots is literally the i-fold free bar term.

   theorem term_pattern (i : ℕ) (p : List Bool) :
       DerivedBar.term k D (patternTerm k D X N p) i =
         patternTerm k D X N (List.replicate i false ++ p) := by
   …

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

4. def OAI.DerivedBar.Multibar.termPatternIso line 39

   Source documentation

   Exterior actions agree as well as the underlying field-tensor modules.

   def termPatternIso (i : ℕ) (p : List Bool) :
       ModuleCat.of D (DerivedBar.term k D (patternTerm k D X N p) i) ≅
         ModuleCat.of D (patternTerm k D X N (List.replicate i false ++ p)) := by
   …

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

5. def OAI.DerivedBar.Multibar.freeBarObjIso line 49

   Source documentation

   Coherence between canonical categorical scalars and supplied compatible scalars.

   def freeBarObjIso (V : Type u) [AddCommGroup V] [Module k V]
       [Module D V] [IsScalarTower k D V] (i : ℕ) :
       ((DerivedBar.barFunctor k D).obj (ModuleCat.of D V)).X i ≅
         ModuleCat.of D (DerivedBar.term k D V (i+1)) := by
   …

   Mentions: OAI.DerivedBar.barFunctor, OAI.DerivedBar.term

6. def OAI.DerivedBar.Multibar.twoSidedBarObjIso line 58

   Source documentation

   The same coherence for arbitrary X bimodule coefficients.

   def twoSidedBarObjIso (V : Type u) [AddCommGroup V] [Module k V]
       [Module D V] [IsScalarTower k D V] (i : ℕ) :
       ((BimoduleTensor.twoSidedBarFunctor k D X).obj (ModuleCat.of D V)).X i ≅
         ModuleCat.of D (X ⊗[k] DerivedBar.term k D V i) := by
   …

   Mentions: OAI.DerivedBar.BimoduleTensor.twoSidedBarFunctor, OAI.DerivedBar.term

7. def OAI.DerivedBar.Multibar.freeBarPatternIso line 67

   Source documentation

   Coherence of a free bar term with a literal leading block.

   def freeBarPatternIso (i : ℕ) (p : List Bool) :
       ((DerivedBar.barFunctor k D).obj (ModuleCat.of D (patternTerm k D X N p))).X i ≅
         ModuleCat.of D (patternTerm k D X N (List.replicate (i+1) false ++ p)) :=
   …

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

8. def OAI.DerivedBar.Multibar.twoSidedBarPatternIso line 73

   Source documentation

   Coherence of a two-sided bar term with its literal X and D slots.

   def twoSidedBarPatternIso (i : ℕ) (p : List Bool) :
       ((BimoduleTensor.twoSidedBarFunctor k D X).obj
         (ModuleCat.of D (patternTerm k D X N p))).X i ≅
         ModuleCat.of D (patternTerm k D X N (true :: (List.replicate i false ++ p))) :=
   …

   Mentions: OAI.DerivedBar.BimoduleTensor.twoSidedBarFunctor, OAI.DerivedBar.Multibar.patternTerm