OAI/Algebra/Finitistic/Ordinary/OrdinaryTerminal.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.OrdinarySimulation.terminalAugmentation line 12

   Source documentation

   The terminal character extended along the B-factor.

   def terminalAugmentation : (B ⊗[k] ChainAlgebra k l) →ₐ[k] B :=
   …

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra

2. def OAI.LittleFinitistic.OrdinarySimulation.TerminalTensor line 21

   Source documentation

   Coordinate model for B tensor_k W, with its specified terminal right action.

   def TerminalTensor := B
   …

3. instance OAI.LittleFinitistic.OrdinarySimulation.TerminalTensor.(instance at line 23) line 23
4. instance OAI.LittleFinitistic.OrdinarySimulation.TerminalTensor.(instance at line 24) line 24
5. instance OAI.LittleFinitistic.OrdinarySimulation.TerminalTensor.(instance at line 25) line 25
6. instance OAI.LittleFinitistic.OrdinarySimulation.TerminalTensor.(instance at line 26) line 26
7. def OAI.LittleFinitistic.OrdinarySimulation.TerminalTensor.value line 29
8. theorem OAI.LittleFinitistic.OrdinarySimulation.TerminalTensor.right_action line 31
9. instance OAI.LittleFinitistic.OrdinarySimulation.TerminalTensor.towerLeft line 34
10. instance OAI.LittleFinitistic.OrdinarySimulation.TerminalTensor.towerRight line 36
11. instance OAI.LittleFinitistic.OrdinarySimulation.TerminalTensor.commuteActions line 41
12. def OAI.LittleFinitistic.OrdinarySimulation.TerminalTensor.tensorModel line 48

    Source documentation

    Explicit identification of this coordinate model with the source tensor product.

    def tensorModel : (B ⊗[k] k) ≃ₗ[k] TerminalTensor B := TensorProduct.rid k B

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.TerminalTensor

13. theorem OAI.LittleFinitistic.OrdinarySimulation.TerminalTensor.tensorModel_tmul line 50
14. theorem OAI.LittleFinitistic.OrdinarySimulation.TerminalTensor.tensor_right_formula line 54

    Source documentation

    The coordinate right action has exactly the regular-B/terminal-W tensor formula.

    theorem tensor_right_formula (b b' : B) (w : k) (c : ChainAlgebra k l) :
        MulOpposite.op (b' ⊗ₜ[k] c) • tensorModel k B (b ⊗ₜ[k] w) =
          tensorModel k B ((b*b') ⊗ₜ[k] (w * ChainAlgebra.terminalCharacter k l c)) := by
    …

    Mentions: OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.OrdinarySimulation.TerminalTensor.tensorModel, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra.terminalCharacter

15. instance OAI.LittleFinitistic.OrdinarySimulation.TerminalTensor.finiteDimensional line 65