OAI/Algebra/Finitistic/Dimension/PDBarQuotient.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.PDBarQuotient.RightBase line 14

   Source documentation

   D with the actual right A action through f.

   def RightBase (_f : A →ₐ[k] D) := D

2. instance OAI.LittleFinitistic.PDBarQuotient.(instance at line 15) line 15
3. instance OAI.LittleFinitistic.PDBarQuotient.(instance at line 16) line 16
4. instance OAI.LittleFinitistic.PDBarQuotient.(instance at line 17) line 17
5. theorem OAI.LittleFinitistic.PDBarQuotient.right_smul line 19
6. def OAI.LittleFinitistic.PDBarQuotient.forward line 25

   Source documentation

   Quotient map from the detector tensor to the actual left D-linear bar quotient.

   def forward : BalancedTensor.Tensor k A (RightBase f) V →ₗ[k] DerivedBar.Balanced.tensor f V :=
   …

   Mentions: OAI.LittleFinitistic.BalancedTensor.Tensor, OAI.LittleFinitistic.PDBarQuotient.RightBase, OAI.DerivedBar.Balanced.tensor

7. theorem OAI.LittleFinitistic.PDBarQuotient.relations_kill line 34

   Source documentation

   Every D-linear balancing relation lies in the detector's k-linear relation space; the proof retains all left D multiples, rather than assuming the quotients equal.

   theorem relations_kill : (DerivedBar.Balanced.relations f V).restrictScalars k ≤
       (BalancedTensor.relations k A (RightBase f) V).mkQ.ker := by
   …

   Mentions: OAI.DerivedBar.Balanced.relations, OAI.LittleFinitistic.BalancedTensor.relations, OAI.LittleFinitistic.PDBarQuotient.RightBase

8. def OAI.LittleFinitistic.PDBarQuotient.inverse line 56
9. theorem OAI.LittleFinitistic.PDBarQuotient.forward_mk line 61
10. theorem OAI.LittleFinitistic.PDBarQuotient.inverse_quotient line 66
11. def OAI.LittleFinitistic.PDBarQuotient.equiv line 71

    Source documentation

    Canonical actual quotient equivalence, on representatives d tensor v.

    def equiv : BalancedTensor.Tensor k A (RightBase f) V ≃ₗ[k] DerivedBar.Balanced.tensor f V :=
    …

    Mentions: OAI.LittleFinitistic.BalancedTensor.Tensor, OAI.LittleFinitistic.PDBarQuotient.RightBase, OAI.DerivedBar.Balanced.tensor

12. theorem OAI.LittleFinitistic.PDBarQuotient.natural line 85
13. theorem OAI.LittleFinitistic.PDBarQuotient.left_action line 94

    Source documentation

    Exterior D multiplication agrees on every tensor generator.

    theorem left_action (d b : D) (v : V) :
        forward f V (BalancedTensor.mk k A (RightBase f) V (d*b) v) =
          d • forward f V (BalancedTensor.mk k A (RightBase f) V b v) := by
    …

    Mentions: OAI.LittleFinitistic.PDBarQuotient.forward, OAI.LittleFinitistic.BalancedTensor.mk, OAI.LittleFinitistic.PDBarQuotient.RightBase