OAI/Algebra/Finitistic/Selection/SelectionEncoding.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.LittleFinitistic.SelectionEncoding.Encoding line 10

   Source documentation

   Concrete finite coefficient data, with an exact presentation equivalence.

   structure Encoding (k R : Type*) [Field k] [Ring R] [Algebra k R] where
   …

2. def OAI.LittleFinitistic.SelectionEncoding.generator line 19
3. theorem OAI.LittleFinitistic.SelectionEncoding.generator_relations line 24

   Source documentation

   These concrete elements of R satisfy every coefficient equation.

   theorem generator_relations (j : Fin E.equations) :
       (∑ h, ∑ l, E.relations.quadratic j h l • (generator E h * generator E l)) +
       (∑ h, E.relations.linear j h • generator E h) + E.relations.constant j • (1 : R) = 0 := by
   …

   Mentions: OAI.LittleFinitistic.SelectionEncoding.generator

4. abbrev OAI.LittleFinitistic.SelectionEncoding.directedAlgebra line 32
5. instance OAI.LittleFinitistic.SelectionEncoding.(instance at line 34) line 34
6. theorem OAI.LittleFinitistic.SelectionEncoding.directedAlgebra_finiteDimensional line 37
7. theorem OAI.LittleFinitistic.SelectionEncoding.directedAlgebra_globalDimension_le_two line 41
8. def OAI.LittleFinitistic.SelectionEncoding.auxiliaryEncoding line 47

   Source documentation

   The actual Section 2 selecting algebra has one fixed concrete finite encoding.

   noncomputable def auxiliaryEncoding : Encoding ℂ SelectionRing :=
   …

   Mentions: OAI.LittleFinitistic.SelectionEncoding.Encoding, OAI.LittleFinitistic.SelectionRing