OAI/Algebra/Finitistic/Selected/SelectedShiftedRealization.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.SelectedShiftedRealization.shifted line 14

   Source documentation

   The actual shifted selecting bimodule, with its full B actions.

   abbrev shifted := SelectedRectification.bimodule⟦b⟧

   Mentions: OAI.LittleFinitistic.SelectedRectification.bimodule

2. def OAI.LittleFinitistic.SelectedShiftedRealization.model line 16
3. abbrev OAI.LittleFinitistic.SelectedShiftedRealization.G line 23
4. def OAI.LittleFinitistic.SelectedShiftedRealization.comparison line 27

   Source documentation

   Tensoring a selected stalk by the shifted fixed bimodule shifts the already verified full B-linear tensor complex.

   def comparison (Y : FiniteSelectionFamily.S.{0}) :
       G.obj (FiniteSelectionFamily.derived Y) ≅
         (SelectedTensorSplitting.object (FiniteSelectionFamily.representation Y).Evaluation)⟦b⟧ :=
   …

   Mentions: OAI.LittleFinitistic.FiniteSelectionFamily.derived, OAI.LittleFinitistic.SelectedTensorSplitting.object, OAI.LittleFinitistic.FiniteSelectionFamily.representation

5. def OAI.LittleFinitistic.SelectedShiftedRealization.realizationNested line 38

   Source documentation

   The concrete two summands for one application of the actual shifted tensor.

   def realizationNested (Y : FiniteSelectionFamily.S.{0}) :
       G.obj (FiniteSelectionFamily.derived Y) ≅
         (FiniteSelectionFamily.derived (FiniteSelectionFamily.H Y))⟦b⟧ ⊞
           ((FiniteSelectionFamily.derived (FiniteSelectionFamily.H Y))⟦(3 : ℤ)⟧)⟦b⟧ :=
   …

   Mentions: OAI.LittleFinitistic.FiniteSelectionFamily.derived, OAI.LittleFinitistic.FiniteSelectionFamily.H

6. def OAI.LittleFinitistic.SelectedShiftedRealization.realization line 46

   Source documentation

   The source convention places the two summands in shifts b and b+3.

   def realization (Y : FiniteSelectionFamily.S.{0}) :
       G.obj (FiniteSelectionFamily.derived Y) ≅
         (FiniteSelectionFamily.derived (FiniteSelectionFamily.H Y))⟦b⟧ ⊞
           (FiniteSelectionFamily.derived (FiniteSelectionFamily.H Y))⟦b+3⟧ :=
   …

   Mentions: OAI.LittleFinitistic.FiniteSelectionFamily.derived, OAI.LittleFinitistic.FiniteSelectionFamily.H

7. def OAI.LittleFinitistic.SelectedShiftedRealization.iteration line 53
8. theorem OAI.LittleFinitistic.SelectedShiftedRealization.isZero_iff line 60
9. theorem OAI.LittleFinitistic.SelectedShiftedRealization.extinction line 68