OAI/Algebra/Finitistic/Selected/SelectedFirstBlockFamily.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.SelectedFirstBlockFamily.inflation line 19

   Source documentation

   The actual exact inflation functor from B-modules to the first D-block.

   abbrev inflation : ModuleCat.{0} (B P) ⥤ ModuleCat.{0} D := ModuleCat.restrictScalars SelectedOrdinaryModules.firstProjection

   Mentions: OAI.LittleFinitistic.SelectedOrdinaryModules.firstProjection

2. instance OAI.LittleFinitistic.SelectedFirstBlockFamily.inflation_preservesFiniteLimits line 20
3. instance OAI.LittleFinitistic.SelectedFirstBlockFamily.inflation_preservesFiniteColimits line 25
4. abbrev OAI.LittleFinitistic.SelectedFirstBlockFamily.derivedInflation line 30
5. instance OAI.LittleFinitistic.SelectedFirstBlockFamily.derivedInflation_additive line 32
6. def OAI.LittleFinitistic.SelectedFirstBlockFamily.moduleIso line 38

   Source documentation

   This is the original selected input, with precisely its constructed D-action.

   def moduleIso (Y : FiniteSelectionFamily.S.{0}) :
       inflation.obj (FiniteSelectionFamily.module Y) ≅ SelectedBaseIterates.input Y :=
   …

   Mentions: OAI.LittleFinitistic.FiniteSelectionFamily.module, OAI.LittleFinitistic.SelectedBaseIterates.input

7. abbrev OAI.LittleFinitistic.SelectedFirstBlockFamily.derived line 42
8. def OAI.LittleFinitistic.SelectedFirstBlockFamily.stalkIso line 46

   Source documentation

   Exact inflation on derived categories agrees with the selected first-block stalk.

   def stalkIso (Y : FiniteSelectionFamily.S.{0}) :
       derivedInflation.obj (FiniteSelectionFamily.derived Y) ≅ derived Y :=
   …

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

9. theorem OAI.LittleFinitistic.SelectedFirstBlockFamily.module_zero line 51
10. theorem OAI.LittleFinitistic.SelectedFirstBlockFamily.derived_zero line 57
11. def OAI.LittleFinitistic.SelectedFirstBlockFamily.inflated_realization line 69

    Source documentation

    The already proved Phi realization, transported by the actual first-block inflation, with no ordinary F² identity assumed or asserted.

    def inflated_realization (Y : FiniteSelectionFamily.S.{0}) :
        derivedInflation.obj (SelectedDerivedFunctor.Phi.obj (FiniteSelectionFamily.derived Y)) ≅
          derived (FiniteSelectionFamily.H Y) ⊞ (derived (FiniteSelectionFamily.H Y))⟦(3 : ℤ)⟧ :=
    …

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