OAI/Algebra/Finitistic/Ordinary/OrdinaryBalancedAssociativity.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LittleFinitistic.BalancedAssociativity.Left line 15
  2. abbrev OAI.LittleFinitistic.BalancedAssociativity.Right line 16
  3. def OAI.LittleFinitistic.BalancedAssociativity.forwardAt line 19

    Source documentation

    Reassociate a fixed last input through the actual A-balanced quotient.

    def forwardAt (z : Z) : RightTensor k A B M N →ₗ[k] Right k A B M N Z :=
…

    Mentions: OAI.LittleFinitistic.RightTensor, OAI.LittleFinitistic.BalancedAssociativity.Right

  4. theorem OAI.LittleFinitistic.BalancedAssociativity.forwardAt_mk line 26
  5. def OAI.LittleFinitistic.BalancedAssociativity.forwardBilinear line 30
  6. def OAI.LittleFinitistic.BalancedAssociativity.forward line 55

    Source documentation

    The actual forward associativity map of balanced tensors.

    def forward : Left k A B M N Z →ₗ[k] Right k A B M N Z :=
…

    Mentions: OAI.LittleFinitistic.BalancedAssociativity.Left, OAI.LittleFinitistic.BalancedAssociativity.Right

  7. theorem OAI.LittleFinitistic.BalancedAssociativity.forward_mk line 69
  8. def OAI.LittleFinitistic.BalancedAssociativity.inverseAt line 74

    Source documentation

    Reassociate a fixed first input through the actual B-balanced quotient.

    def inverseAt (m : M) : LeftTensor k B A N Z →ₗ[k] Left k A B M N Z :=
…

    Mentions: OAI.LittleFinitistic.LeftTensor, OAI.LittleFinitistic.BalancedAssociativity.Left

  9. theorem OAI.LittleFinitistic.BalancedAssociativity.inverseAt_mk line 81
  10. def OAI.LittleFinitistic.BalancedAssociativity.inverseBilinear line 85
  11. def OAI.LittleFinitistic.BalancedAssociativity.inverse line 102

    Source documentation

    The actual inverse associativity map of balanced tensors.

    def inverse : Right k A B M N Z →ₗ[k] Left k A B M N Z :=
…

    Mentions: OAI.LittleFinitistic.BalancedAssociativity.Right, OAI.LittleFinitistic.BalancedAssociativity.Left

  12. theorem OAI.LittleFinitistic.BalancedAssociativity.inverse_mk line 116
  13. def OAI.LittleFinitistic.BalancedAssociativity.equivalence line 121

    Source documentation

    Associativity of the actual noncommutative balanced tensor, with no flatness hypotheses.

    def equivalence : Left k A B M N Z ≃ₗ[k] Right k A B M N Z where
…

    Mentions: OAI.LittleFinitistic.BalancedAssociativity.Left, OAI.LittleFinitistic.BalancedAssociativity.Right