OAI/Algebra/Finitistic/Encoding/EncodingModuleAssembly.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.EncodingModuleAssembly.system line 15
2. def OAI.LittleFinitistic.EncodingModuleAssembly.equiv line 20

   Source documentation

   Reconstruct a full module isomorphism from the three actual vertex-space isomorphisms and the two finite arrow families. Its underlying vector-space map is precisely the direct-sum assembly of the supplied vertex isomorphisms.

   def equiv (E : ∀ i, Space (system P) M i ≃ₗ[k] Space (system P) N i)
       (h01 : ∀ a x, E 1 (arrow (system P) (i := 0) (j := 1) (arrow01 P a)
   …

   Mentions: OAI.LittleFinitistic.EncodingModuleAssembly.system