OAI/Algebra/Finitistic/Selection/FiniteSelectionFamily.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LittleFinitistic.FiniteSelectionFamily.S line 11

    Source documentation

    Actual finite-dimensional modules over the fixed selecting algebra.

    def S := {M : ModuleCat SelectionRing // FiniteDimensional ℂ (complexObject M)}

    Mentions: OAI.LittleFinitistic.SelectionRing, OAI.LittleFinitistic.complexObject

  2. abbrev OAI.LittleFinitistic.FiniteSelectionFamily.vector line 12
  3. instance OAI.LittleFinitistic.FiniteSelectionFamily.(instance at line 13) line 13
  4. instance OAI.LittleFinitistic.FiniteSelectionFamily.ringModule line 14
  5. instance OAI.LittleFinitistic.FiniteSelectionFamily.tower line 16
  6. def OAI.LittleFinitistic.FiniteSelectionFamily.H line 20

    Source documentation

    H preserves this actual finite-dimensional family.

    def H (Y : S) : S := ⟨selectionStep Y.val, by
…

    Mentions: OAI.LittleFinitistic.FiniteSelectionFamily.S, OAI.LittleFinitistic.selectionStep

  7. abbrev OAI.LittleFinitistic.FiniteSelectionFamily.representation line 24
  8. abbrev OAI.LittleFinitistic.FiniteSelectionFamily.module line 25
  9. abbrev OAI.LittleFinitistic.FiniteSelectionFamily.derived line 26
  10. def OAI.LittleFinitistic.FiniteSelectionFamily.realization line 29

    Source documentation

    The proved one-step realization uses the actual endomap of the finite family.

    def realization (Y : S) :
    SelectedTensorSplitting.object (representation Y).Evaluation ≅
      derived (H Y) ⊞ (derived (H Y))⟦(3 : ℤ)⟧ :=
…

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

  11. theorem OAI.LittleFinitistic.FiniteSelectionFamily.module_zero line 35

    Source documentation

    Evaluation on three copies preserves and reflects the zero module.

    theorem module_zero (Y : S) : IsZero (module Y) ↔ Subsingleton Y.val := by
…

    Mentions: OAI.LittleFinitistic.FiniteSelectionFamily.S, OAI.LittleFinitistic.FiniteSelectionFamily.module

  12. theorem OAI.LittleFinitistic.FiniteSelectionFamily.derived_zero line 51

    Source documentation

    The same exact zero criterion after embedding in the actual derived category.

    theorem derived_zero (Y : S) : IsZero (derived Y) ↔ Subsingleton Y.val := by
…

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

  13. theorem OAI.LittleFinitistic.FiniteSelectionFamily.iterate_val line 60

    Source documentation

    Iteration is literally the Section 2 selection operation.

    theorem iterate_val (j : ℕ) (Y : S) : ((H^[j]) Y).val = selectionIterate Y.val j := by
…

    Mentions: OAI.LittleFinitistic.FiniteSelectionFamily.S, OAI.LittleFinitistic.FiniteSelectionFamily.H, OAI.LittleFinitistic.selectionIterate

  14. def OAI.LittleFinitistic.FiniteSelectionFamily.test line 68
  15. theorem OAI.LittleFinitistic.FiniteSelectionFamily.extinction line 71

    Source documentation

    Exact finite extinction is retained by the actual derived evaluation family.

    theorem extinction (m : ℕ) [NeZero m] :
    (∀ j < m, ¬ IsZero (derived ((H^[j]) (test m)))) ∧
      IsZero (derived ((H^[m]) (test m))) := by
…

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