OAI/Algebra/Finitistic/Selected/SelectedOrdinaryResolution.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.SelectedOrdinaryResolution.complex line 11

   Source documentation

   The one fixed genuine D-bimodule resolution Q_X used by the source.

   abbrev complex := OrdinarySimulation.XResolution.complex SelectedRectification.bimodule a length

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.XResolution.complex, OAI.LittleFinitistic.SelectedRectification.bimodule

2. abbrev OAI.LittleFinitistic.SelectedOrdinaryResolution.target line 12
3. abbrev OAI.LittleFinitistic.SelectedOrdinaryResolution.augmentation line 13
4. theorem OAI.LittleFinitistic.SelectedOrdinaryResolution.augmentation_quasiIso line 16
5. theorem OAI.LittleFinitistic.SelectedOrdinaryResolution.right_projective line 19
6. theorem OAI.LittleFinitistic.SelectedOrdinaryResolution.bounded line 23
7. abbrev OAI.LittleFinitistic.SelectedOrdinaryResolution.derived line 30

   Source documentation

   Tensor via the actual bounded right-projective Q_X, with the left D-action retained.

   abbrev derived := OrdinarySimulation.XResolution.derivedTensor SelectedRectification.bimodule a length

   Mentions: OAI.LittleFinitistic.OrdinarySimulation.XResolution.derivedTensor, OAI.LittleFinitistic.SelectedRectification.bimodule

8. abbrev OAI.LittleFinitistic.SelectedOrdinaryResolution.comparison line 31