OrdinaryTensorAugmentation.lean`

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

instance OAI.LittleFinitistic.OrdinarySimulation.TerminalSimple.tower line 12
def OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.simpleCoordinates line 21
def OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.terminalEquiv line 29
def OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.augmentation line 33
Source documentation
The augmentation retains the actual right BC-action.
```
def augmentation : term k B l l →ₗ[(B ⊗[k] ChainAlgebra k l)ᵐᵒᵖ] TerminalTensor B where
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.term, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.OrdinarySimulation.TerminalTensor
theorem OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.augmentation_tensor line 39
Source documentation
The ordinary augmentation is exactly B tensor the terminal C-augmentation.
```
theorem augmentation_tensor (z : B ⊗[k] resolutionIdeal k l l) :
    augmentation k B l (termEquiv k B l l z) =
      terminalEquiv k B (((resolutionAugmentation k l).hom.restrictScalars k).lTensor B z) := by
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.augmentation, OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.termEquiv, OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.terminalEquiv
theorem OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.augmentation_left line 49
Source documentation
The augmentation preserves the regular left B-action as well.
```
theorem augmentation_left (b : B) (x : term k B l l) :
    augmentation k B l (b • x) = b • augmentation k B l x := by
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.term, OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.augmentation
theorem OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.augmentation_comp line 58
theorem OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.augmentation_exact line 69
theorem OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.augmentation_surjective line 94
Source documentation
Surjectivity is explicit: the terminal vertex lifts every coefficient b.
```
theorem augmentation_surjective : Function.Surjective (augmentation k B l) := by
…
```
Mentions: OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.augmentation
theorem OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.initial_injective line 105
theorem OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.augmentation_zero_injective line 114