OAI/Algebra/Finitistic/Ordinary/OrdinaryFiniteConeReindex.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.FiniteColumnComplex.coneColumn line 16
2. abbrev OAI.LittleFinitistic.FiniteColumnComplex.totalCone line 17
3. def OAI.LittleFinitistic.FiniteColumnComplex.pairEquiv line 20

   Source documentation

   Distribution of a binary module product over the finite family of columns.

   def pairEquiv (n : ℤ) : (term K (n+1) × term L n) ≃ₗ[R] (∀ i, (K i).X (n+1) × (L i).X n) where
   …

   Mentions: OAI.LittleFinitistic.FiniteColumnComplex.term

4. def OAI.LittleFinitistic.FiniteColumnComplex.coneEquiv line 29

   Source documentation

   Reindex the actual cone of a total map into the actual cones of its column maps.

   def coneEquiv (n : ℤ) : (totalCone K L δ ε f hc).X n ≃ₗ[R] term (coneColumn K L f) n :=
   …

   Mentions: OAI.LittleFinitistic.FiniteColumnComplex.totalCone, OAI.LittleFinitistic.FiniteColumnComplex.term, OAI.LittleFinitistic.FiniteColumnComplex.coneColumn

5. theorem OAI.LittleFinitistic.FiniteColumnComplex.coneEquiv_coordinate line 34
6. theorem OAI.LittleFinitistic.FiniteColumnComplex.coneEquiv_symm_coordinate line 40
7. def OAI.LittleFinitistic.FiniteColumnComplex.coneDifferential line 49

   Source documentation

   Transport the genuine cone differential through this coordinate equivalence.

   def coneDifferential (n : ℤ) : term (coneColumn K L f) n →ₗ[R] term (coneColumn K L f) (n+1) :=
   …

   Mentions: OAI.LittleFinitistic.FiniteColumnComplex.term, OAI.LittleFinitistic.FiniteColumnComplex.coneColumn

8. theorem OAI.LittleFinitistic.FiniteColumnComplex.coneDifferential_square line 53