OAI/Algebra/Finitistic/Dimension/PDBarQuotientAction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.LittleFinitistic.PDBarQuotient.leftModule line 15

   Source documentation

   The actual exterior D-action transferred through the proved quotient equivalence.

   instance leftModule : Module D (BalancedTensor.Tensor k A (RightBase f) V) :=
   …

   Mentions: OAI.LittleFinitistic.BalancedTensor.Tensor, OAI.LittleFinitistic.PDBarQuotient.RightBase

2. instance OAI.LittleFinitistic.PDBarQuotient.leftTower line 18
3. def OAI.LittleFinitistic.PDBarQuotient.linearEquiv line 21
4. theorem OAI.LittleFinitistic.PDBarQuotient.smul_mk line 26

   Source documentation

   The transferred action is the original left regular multiplication.

   @[simp] theorem smul_mk (d b : D) (v : V) :
       d • BalancedTensor.mk k A (RightBase f) V b v =
         BalancedTensor.mk k A (RightBase f) V (d*b) v := by
   …

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

5. theorem OAI.LittleFinitistic.PDBarQuotient.equiv_smul line 34

   Source documentation

   Compatibility with every exterior scalar, on arbitrary balanced tensors.

   theorem equiv_smul (d : D) (z : BalancedTensor.Tensor k A (RightBase f) V) :
       equiv f V (d • z) = d • equiv f V z := (linearEquiv f V).map_smul d z
   …

   Mentions: OAI.LittleFinitistic.BalancedTensor.Tensor, OAI.LittleFinitistic.PDBarQuotient.RightBase, OAI.LittleFinitistic.PDBarQuotient.equiv, OAI.LittleFinitistic.PDBarQuotient.linearEquiv

6. def OAI.LittleFinitistic.PDBarQuotient.map line 38
7. theorem OAI.LittleFinitistic.PDBarQuotient.map_eq line 43