OAI/Algebra/Finitistic/Dimension/PDResidueTensor.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.PDTensor.radicalProduct line 12
2. abbrev OAI.LittleFinitistic.PDTensor.Top line 13
3. def OAI.LittleFinitistic.PDTensor.residuePair line 15
4. theorem OAI.LittleFinitistic.PDTensor.residuePair_mk line 29
5. def OAI.LittleFinitistic.PDTensor.residueEval line 33
6. def OAI.LittleFinitistic.PDTensor.residueInverse line 39
7. theorem OAI.LittleFinitistic.PDTensor.residueEval_mk line 45
8. theorem OAI.LittleFinitistic.PDTensor.residueInverse_mk line 49
9. def OAI.LittleFinitistic.PDTensor.residueTensorEquiv line 54

   Source documentation

   The actual noncommutative tensor/quotient identification in cor:pd-detection.

   def residueTensorEquiv : BalancedTensor.Tensor k A (Residue (A := A)) N ≃ₗ[k] Top (A := A) N where
   …

   Mentions: OAI.LittleFinitistic.BalancedTensor.Tensor, OAI.LittleFinitistic.PDTensor.Residue, OAI.LittleFinitistic.PDTensor.Top

10. theorem OAI.LittleFinitistic.PDTensor.residueTensor_nontrivial line 77

    Source documentation

    Nakayama proves tensor detection for every finitely generated nonzero module.

    theorem residueTensor_nontrivial [Module.Finite A N] [Nontrivial N] :
        Nontrivial (BalancedTensor.Tensor k A (Residue (A := A)) N) := by
    …

    Mentions: OAI.LittleFinitistic.BalancedTensor.Tensor, OAI.LittleFinitistic.PDTensor.Residue