OAI/Algebra/Finitistic/Rectification/VertexProjectives.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.VertexProjectives.ideal line 11

   Source documentation

   eB, represented in the opposite regular module to encode right linearity.

   def ideal (e : B) : Submodule Bᵐᵒᵖ Bᵐᵒᵖ :=
   …

2. theorem OAI.LittleFinitistic.VertexProjectives.fixed line 14
3. instance OAI.LittleFinitistic.VertexProjectives.finite line 20
4. theorem OAI.LittleFinitistic.VertexProjectives.projective line 23
5. def OAI.LittleFinitistic.VertexProjectives.object line 30

   Source documentation

   The actual finitely generated projective right module eB.

   def object (e : B) (he : e * e = e) : ProjectiveComplexes.Proj B :=
   …

   Mentions: OAI.LittleFinitistic.ProjectiveComplexes.Proj

6. def OAI.LittleFinitistic.VertexProjectives.arrow line 34

   Source documentation

   Left multiplication by an arrow a with target idempotent e'.

   def arrow {e e' : B} (he : e * e = e) (he' : e' * e' = e')
       (a : B) (ha : e' * a = a) : object e he ⟶ object e' he' :=
   …

   Mentions: OAI.LittleFinitistic.VertexProjectives.object

7. theorem OAI.LittleFinitistic.VertexProjectives.arrow_apply line 42
8. theorem OAI.LittleFinitistic.VertexProjectives.arrow_comp line 46