OAI/Algebra/Finitistic/Ordinary/OrdinaryTensorIdeal.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.OrdinarySimulation.TensorIdeal.vertex line 12
2. theorem OAI.LittleFinitistic.OrdinarySimulation.TensorIdeal.vertex_idempotent line 15
3. def OAI.LittleFinitistic.OrdinarySimulation.TensorIdeal.project line 18
4. def OAI.LittleFinitistic.OrdinarySimulation.TensorIdeal.inclusion line 23
5. def OAI.LittleFinitistic.OrdinarySimulation.TensorIdeal.retraction line 26
6. theorem OAI.LittleFinitistic.OrdinarySimulation.TensorIdeal.inclusion_retraction line 29
7. theorem OAI.LittleFinitistic.OrdinarySimulation.TensorIdeal.retraction_inclusion line 38
8. theorem OAI.LittleFinitistic.OrdinarySimulation.TensorIdeal.inclusion_fixed line 48
9. def OAI.LittleFinitistic.OrdinarySimulation.TensorIdeal.equivalence line 53

   Source documentation

   The source term B tensor eC is the actual right ideal (1 tensor e)(B tensor C).

   def equivalence : B ⊗[k] IdempotentTensor.rightIdeal e ≃ₗ[k]
       IdempotentTensor.rightIdeal (vertex (k := k) (B := B) e) where
   …

   Mentions: OAI.LittleFinitistic.IdempotentTensor.rightIdeal, OAI.LittleFinitistic.OrdinarySimulation.TensorIdeal.vertex

10. theorem OAI.LittleFinitistic.OrdinarySimulation.TensorIdeal.equivalence_tmul line 62