OAI/Algebra/Finitistic/Ordinary/OrdinaryConeCoordinates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.ConeCoordinates.coordinateIso line 13

   Source documentation

   The native cone term in its actual two module coordinates.

   def coordinateIso (n : ℤ) : (CochainComplex.mappingCone f).X n ≅
       ModuleCat.of R (K.X (n+1) × L.X n) :=
   …

2. def OAI.LittleFinitistic.ConeCoordinates.coordinateEquiv line 18
3. theorem OAI.LittleFinitistic.ConeCoordinates.coordinate_fst line 21
4. theorem OAI.LittleFinitistic.ConeCoordinates.coordinate_snd line 28
5. theorem OAI.LittleFinitistic.ConeCoordinates.differential_fst line 40

   Source documentation

   The first coordinate of the native cone differential carries its negative sign.

   theorem differential_fst (n : ℤ) (z : (CochainComplex.mappingCone f).X n) :
       (coordinateEquiv f (n+1) (((CochainComplex.mappingCone f).d n (n+1)).hom z)).1 =
         -((K.d (n+1) ((n+1)+1)).hom (coordinateEquiv f n z).1) := by
   …

   Mentions: OAI.LittleFinitistic.ConeCoordinates.coordinateEquiv

6. theorem OAI.LittleFinitistic.ConeCoordinates.differential_snd line 48

   Source documentation

   The second coordinate contains the input map and the target differential.

   theorem differential_snd (n : ℤ) (z : (CochainComplex.mappingCone f).X n) :
       (coordinateEquiv f (n+1) (((CochainComplex.mappingCone f).d n (n+1)).hom z)).2 =
         (f.f (n+1)).hom (coordinateEquiv f n z).1 +
         (L.d n (n+1)).hom (coordinateEquiv f n z).2 := by
   …

   Mentions: OAI.LittleFinitistic.ConeCoordinates.coordinateEquiv