OAI/Algebra/Finitistic/Ordinary/OrdinaryBimoduleTensorTerms.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.BimoduleComplexTensor.rightComplex line 16
2. abbrev OAI.LittleFinitistic.BimoduleComplexTensor.term line 20
3. def OAI.LittleFinitistic.BimoduleComplexTensor.map line 23

   Source documentation

   Both actual term maps with the outside left action retained.

   def map {p p' q q' : ℤ} (f : Q.X p ⟶ Q.X p') (g : Z.X q ⟶ Z.X q') :
       term k S A Q Z p q →ₗ[S] term k S A Q Z p' q' :=
   …

   Mentions: OAI.LittleFinitistic.BimoduleComplexTensor.term

4. def OAI.LittleFinitistic.BimoduleComplexTensor.forgetEquiv line 28

   Source documentation

   Forgetting the outside action gives exactly the previous balanced tensor term.

   def forgetEquiv (p q : ℤ) : term k S A Q Z p q ≃ₗ[k]
       ComplexTensor.term k A (rightComplex k S A Q) Z p q := by
   …

   Mentions: OAI.LittleFinitistic.BimoduleComplexTensor.term, OAI.LittleFinitistic.ComplexTensor.term, OAI.LittleFinitistic.BimoduleComplexTensor.rightComplex

5. theorem OAI.LittleFinitistic.BimoduleComplexTensor.forget_map line 35

   Source documentation

   The retained-action map has precisely the same underlying balanced map.

   theorem forget_map {p p' q q' : ℤ} (f : Q.X p ⟶ Q.X p') (g : Z.X q ⟶ Z.X q') :
       (forgetEquiv k S A Q Z p' q').toLinearMap.comp ((map k S A Q Z f g).restrictScalars k) =
         (ComplexTensor.map k A (rightComplex k S A Q) Z
           ((ModuleCat.restrictScalars (Algebra.TensorProduct.includeRight (R := k) (A := S) (B := Aᵐᵒᵖ)).toRingHom).map f) g).comp
   …

   Mentions: OAI.LittleFinitistic.BimoduleComplexTensor.forgetEquiv, OAI.LittleFinitistic.BimoduleComplexTensor.map, OAI.LittleFinitistic.ComplexTensor.map, OAI.LittleFinitistic.BimoduleComplexTensor.rightComplex