OrdinaryComplexAction.lean`

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.coefficient line 14
Source documentation
The coefficient of the unique possible arrow from j to i.
```
def coefficient (x : ChainAlgebra k l) (i j : Fin (l+1)) : k :=
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra
theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.coefficient_mul line 17
theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.coefficient_one line 31
theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.coefficient_zero line 37
theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.coefficient_add line 42
theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.coefficient_vertex line 48
theorem OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.coefficient_arrow line 53
abbrev OAI.LittleFinitistic.OrdinarySimulation.OrdinaryTerms line 63
Source documentation
Actual finite direct sum of terms; the finite product is canonically that sum.
```
abbrev OrdinaryTerms (V : Fin (l+1) → Type v) := ∀ i, V i
…
```
def OAI.LittleFinitistic.OrdinarySimulation.OrdinaryTerms.action line 70
Source documentation
Coordinate action induced by the genuine differential, not an assumed representation.
```
def action (x : ChainAlgebra k l) (v : OrdinaryTerms V) (i : Fin (l+1)) : V i :=
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.OrdinarySimulation.OrdinaryTerms
theorem OAI.LittleFinitistic.OrdinarySimulation.OrdinaryTerms.action_add line 73
theorem OAI.LittleFinitistic.OrdinarySimulation.OrdinaryTerms.action_smul line 79
theorem OAI.LittleFinitistic.OrdinarySimulation.OrdinaryTerms.action_mul line 88
Source documentation
The complex equation d²=0 implies associativity of the ordinary action.
```
theorem action_mul (dd : ∀ i j h, (d j h).comp (d i j) = 0)
    (x y : ChainAlgebra k l) (v : OrdinaryTerms V) :
    action V d (x*y) v = action V d x (action V d y v) := by
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.OrdinarySimulation.OrdinaryTerms, OAI.LittleFinitistic.OrdinarySimulation.OrdinaryTerms.action
def OAI.LittleFinitistic.OrdinarySimulation.OrdinaryTerms.actionLinear line 101
theorem OAI.LittleFinitistic.OrdinarySimulation.OrdinaryTerms.action_vertex line 107
Source documentation
Each ordinary vertex projects onto the corresponding genuine term.
```
theorem action_vertex (h : Fin (l+1)) (v : OrdinaryTerms V) :
    action V d (ChainAlgebra.vertex k l h) v = Pi.single h (v h) := by
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.OrdinaryTerms, OAI.LittleFinitistic.OrdinarySimulation.OrdinaryTerms.action, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.vertex
theorem OAI.LittleFinitistic.OrdinarySimulation.OrdinaryTerms.action_arrow line 119
Source documentation
Each ordinary arrow acts by the actual differential on its source term.
```
theorem action_arrow (h : Fin l) (v : OrdinaryTerms V) :
    action V d (ChainAlgebra.arrow k l h) v =
      Pi.single h.succ (d h.castSucc h.succ (v h.castSucc)) := by
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.OrdinaryTerms, OAI.LittleFinitistic.OrdinarySimulation.OrdinaryTerms.action, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.arrow
theorem OAI.LittleFinitistic.OrdinarySimulation.OrdinaryTerms.action_one line 130
theorem OAI.LittleFinitistic.OrdinarySimulation.OrdinaryTerms.action_zero line 135
theorem OAI.LittleFinitistic.OrdinarySimulation.OrdinaryTerms.add_action line 140
def OAI.LittleFinitistic.OrdinarySimulation.OrdinaryTerms.module line 149
Source documentation
The ordinary C-module constructed from the complex equation.
```
def module (dd : ∀ i j h, (d j h).comp (d i j) = 0) :
    Module (ChainAlgebra k l) (OrdinaryTerms V) where
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.OrdinarySimulation.OrdinaryTerms
theorem OAI.LittleFinitistic.OrdinarySimulation.OrdinaryTerms.scalarTower line 165
Source documentation
The constructed action retains the given k-vector-space structure.
```
theorem scalarTower : letI := module V d dd; IsScalarTower k (ChainAlgebra k l) (OrdinaryTerms V) := by
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.OrdinaryTerms.module, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.OrdinarySimulation.OrdinaryTerms
theorem OAI.LittleFinitistic.OrdinarySimulation.OrdinaryTerms.action_commutes line 180
Source documentation
Any additional scalar action commuting with k and with d commutes with C. Applied to B and Bᵐᵒᵖ this proves both bimodule actions, without postulating them.
```
theorem action_commutes (R : Type*) [Monoid R] [∀ i, DistribMulAction R (V i)]
    [∀ i, SMulCommClass k R (V i)]
    (hd : ∀ i j (r : R) (v : V i), d i j (r • v) = r • d i j v)
    (x : ChainAlgebra k l) (r : R) (v : OrdinaryTerms V) :
    action V d x (r • v) = r • action V d x v := by
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.OrdinarySimulation.OrdinaryTerms, OAI.LittleFinitistic.OrdinarySimulation.OrdinaryTerms.action
instance OAI.LittleFinitistic.OrdinarySimulation.OrdinaryTerms.finiteDimensional line 191