OAI/Algebra/Finitistic/Dimension/PDResidueProjection.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.PDResidueProjection.InflatedResidue line 15
2. instance OAI.LittleFinitistic.PDResidueProjection.(instance at line 16) line 16
3. instance OAI.LittleFinitistic.PDResidueProjection.(instance at line 17) line 17
4. instance OAI.LittleFinitistic.PDResidueProjection.(instance at line 18) line 18
5. instance OAI.LittleFinitistic.PDResidueProjection.(instance at line 20) line 20
6. instance OAI.LittleFinitistic.PDResidueProjection.(instance at line 22) line 22
7. instance OAI.LittleFinitistic.PDResidueProjection.(instance at line 24) line 24
8. def OAI.LittleFinitistic.PDResidueProjection.map line 30
9. theorem OAI.LittleFinitistic.PDResidueProjection.map_mk line 40
10. def OAI.LittleFinitistic.PDResidueProjection.equiv line 44

    Source documentation

    The radical quotient-ring comparison also respects the actual k action.

    def equiv : PDTensor.Residue (A := A) ≃ₗ[k] InflatedResidue f :=
    …

    Mentions: OAI.LittleFinitistic.PDTensor.Residue, OAI.LittleFinitistic.PDResidueProjection.InflatedResidue

11. def OAI.LittleFinitistic.PDResidueProjection.rightEquiv line 56

    Source documentation

    Its right A action is precisely restriction through the canonical projection.

    def rightEquiv : PDTensor.Residue (A := A) ≃ₗ[Aᵐᵒᵖ] InflatedResidue f where
    …

    Mentions: OAI.LittleFinitistic.PDTensor.Residue, OAI.LittleFinitistic.PDResidueProjection.InflatedResidue

12. def OAI.LittleFinitistic.PDResidueProjection.tensorEquiv line 67
13. def OAI.LittleFinitistic.PDResidueProjection.tensorNatIso line 84

    Source documentation

    The residue projection comparison is natural on all actual left A-modules.

    def tensorNatIso : PDTensor.tensorFunctor k A (PDTensor.Residue (A := A)) ≅
    …

    Mentions: OAI.LittleFinitistic.PDTensor.tensorFunctor, OAI.LittleFinitistic.PDTensor.Residue

14. def OAI.LittleFinitistic.PDResidueProjection.resolutionIso line 95
15. def OAI.LittleFinitistic.PDResidueProjection.torIso line 102

    Source documentation

    Actual derived residue tensor is unchanged by the proved right-module identification.

    def torIso (n : ℕ) : PDTensor.Tor (k := k) (PDTensor.Residue (A := A)) M n ≅
    …

    Mentions: OAI.LittleFinitistic.PDTensor.Tor, OAI.LittleFinitistic.PDTensor.Residue