OAI/Algebra/Finitistic/Ordinary/OrdinaryFiniteConeTriangular.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.FiniteColumnComplex.coneSource line 15
2. abbrev OAI.LittleFinitistic.FiniteColumnComplex.coneTarget line 17
3. theorem OAI.LittleFinitistic.FiniteColumnComplex.coneEquiv_symm_pair line 20
4. theorem OAI.LittleFinitistic.FiniteColumnComplex.coneDifferential_coordinate line 30

   Source documentation

   The conjugated genuine cone differential has the expected finite-column formula.

   theorem coneDifferential_coordinate (n : ℤ) (z : term (coneColumn K L f) n) (i : Fin l) :
       ConeCoordinates.coordinateEquiv (f i) (n+1) (coneDifferential K L δ ε f hc n z i) =
         (-(δ.d (n+1) (coneSource K L f n z)) i,
          ((f i).f (n+1)).hom (coneSource K L f n z i) + (ε.d n (coneTarget K L f n z)) i) := by
   …

   Mentions: OAI.LittleFinitistic.FiniteColumnComplex.term, OAI.LittleFinitistic.FiniteColumnComplex.coneColumn, OAI.LittleFinitistic.ConeCoordinates.coordinateEquiv, OAI.LittleFinitistic.FiniteColumnComplex.coneDifferential, OAI.LittleFinitistic.FiniteColumnComplex.coneSource, OAI.LittleFinitistic.FiniteColumnComplex.coneTarget

5. def OAI.LittleFinitistic.FiniteColumnComplex.coneTriangular line 43

   Source documentation

   The cone of a componentwise total map is triangular with the actual column cones on its diagonal.

   def coneTriangular : Differential (coneColumn K L f) where
   …

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

6. def OAI.LittleFinitistic.FiniteColumnComplex.coneIso line 61

   Source documentation

   The triangular cone model is isomorphic to the native cone, not an assumed cone replacement.

   def coneIso : totalCone K L δ ε f hc ≅ complex (coneColumn K L f) (coneTriangular K L δ ε f hc) :=
   …

   Mentions: OAI.LittleFinitistic.FiniteColumnComplex.totalCone, OAI.LittleFinitistic.FiniteColumnComplex.complex, OAI.LittleFinitistic.FiniteColumnComplex.coneColumn, OAI.LittleFinitistic.FiniteColumnComplex.coneTriangular

7. theorem OAI.LittleFinitistic.FiniteColumnComplex.complexMap_quasiIso line 77

   Source documentation

   Quasi-isomorphisms in every column induce a quasi-isomorphism of the actual finite totals.

   theorem complexMap_quasiIso [∀ i, QuasiIso (f i)] : QuasiIso (complexMap K L δ ε f hc) := by
   …

   Mentions: OAI.LittleFinitistic.FiniteColumnComplex.complexMap