OAI/Algebra/Finitistic/Selection/SelectionIteration.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.selectedSubmodule line 9

   Source documentation

   The image of the central idempotent, expressed by its fixed vectors.

   noncomputable def selectedSubmodule (M : ModuleCat SelectionRing) : Submodule SelectionRing M where
   …

   Mentions: OAI.LittleFinitistic.SelectionRing

2. theorem OAI.LittleFinitistic.selectedSubmodule_eq_image line 23
3. def OAI.LittleFinitistic.selectionStep line 32

   Source documentation

   Exactly H(Y) = restriction along alpha of eY from the manuscript.

   noncomputable def selectionStep (M : ModuleCat SelectionRing) : ModuleCat SelectionRing :=
   …

   Mentions: OAI.LittleFinitistic.SelectionRing

4. def OAI.LittleFinitistic.selectionIterate line 36
5. def OAI.LittleFinitistic.IdentityAt line 40
6. def OAI.LittleFinitistic.ZeroAt line 43
7. theorem OAI.LittleFinitistic.identityAt_step line 46
8. theorem OAI.LittleFinitistic.zeroAt_step line 54
9. theorem OAI.LittleFinitistic.selectionStep_nontrivial line 62
10. theorem OAI.LittleFinitistic.selectionStep_subsingleton line 67
11. theorem OAI.LittleFinitistic.identityAt_iterate line 74
12. theorem OAI.LittleFinitistic.zeroAt_iterate line 83
13. def OAI.LittleFinitistic.testObject line 92
14. theorem OAI.LittleFinitistic.testObject_identityAt line 95
15. theorem OAI.LittleFinitistic.testObject_zeroAt line 106
16. theorem OAI.LittleFinitistic.selectionIterate_test_nontrivial line 110
17. theorem OAI.LittleFinitistic.selectionIterate_test_subsingleton line 120
18. theorem OAI.LittleFinitistic.selection_extinction line 131

    Source documentation

    Exact extinction under the manuscript's actual selection operation H: every earlier iterate is nonzero and the m-th iterate is zero.

    theorem selection_extinction (m : ℕ) [NeZero m] :
        (∀ n < m, Nontrivial (selectionIterate (testObject m) n)) ∧
        Subsingleton (selectionIterate (testObject m) m) :=
    …

    Mentions: OAI.LittleFinitistic.selectionIterate, OAI.LittleFinitistic.testObject

19. def OAI.LittleFinitistic.complexObject line 136
20. def OAI.LittleFinitistic.selectionStep_inclusion line 139
21. theorem OAI.LittleFinitistic.selectionStep_finiteDimensional line 148
22. theorem OAI.LittleFinitistic.testObject_finiteDimensional line 153
23. theorem OAI.LittleFinitistic.selectionIterate_test_finiteDimensional line 164