OAI/Algebra/Finitistic/Ordinary/OrdinaryCochain.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.OrdinarySimulation.intervalTerms line 13

   Source documentation

   The genuine cochain differential on the selected finite interval.

   abbrev intervalTerms (P : CochainComplex (ModuleCat.{u} k) ℤ) (a : ℤ) (l : ℕ)
       (i : Fin (l+1)) : Type u := P.X (a + (i.val : ℤ))

2. def OAI.LittleFinitistic.OrdinarySimulation.intervalDifferential line 16
3. theorem OAI.LittleFinitistic.OrdinarySimulation.intervalDifferential_square line 20
4. def OAI.LittleFinitistic.OrdinarySimulation.cochainModule line 28

   Source documentation

   The ordinary C-module O formed from the actual terms and differential of P.

   def cochainModule (P : CochainComplex (ModuleCat.{u} k) ℤ) (a : ℤ) (l : ℕ) :
       Module (ChainAlgebra k l) (OrdinaryTerms (intervalTerms P a l)) :=
   …

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.OrdinarySimulation.OrdinaryTerms, OAI.LittleFinitistic.OrdinarySimulation.intervalTerms