OAI/Algebra/Finitistic/Selected/SelectedImageComparison.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.SelectedImageComparison.equiv line 14

   Source documentation

   The evaluator's range is canonically the primary's actual H(Y), as a complex vector space.

   def equiv : imageSpace (k := ℂ) (Y := Y) (selectionIdempotent 0) ≃ₗ[ℂ]
   …

   Mentions: OAI.LittleFinitistic.selectionIdempotent

2. abbrev OAI.LittleFinitistic.SelectedImageComparison.moduleAction line 32
3. theorem OAI.LittleFinitistic.SelectedImageComparison.equiv_action line 36

   Source documentation

   The evaluator's compressed alpha action is precisely the action on the primary's H(Y).

   theorem equiv_action (r : SelectionRing)
       (x : imageSpace (k := ℂ) (Y := Y) (selectionIdempotent 0)) :
   …

   Mentions: OAI.LittleFinitistic.SelectionRing, OAI.LittleFinitistic.selectionIdempotent

4. theorem OAI.LittleFinitistic.SelectedImageComparison.image_nontrivial_of line 47
5. theorem OAI.LittleFinitistic.SelectedImageComparison.image_subsingleton_of line 53